Verifying the reflective visitor pattern
Verifying the reflective visitor pattern
复制标题
DOI：
10.1145/2318202.2318208
复制
发表时间：
2012-06
期刊：
影响因子：
--
通讯作者：
B. Horsfall;Nathaniel Charlton;Bernhard Reus
中科院分区：
文献类型：
--
作者：
B. Horsfall;Nathaniel Charlton;Bernhard Reus
计算反射允许程序在运行时检查和操纵自身的结构或行为。这通常意味着可以以优雅的方式创建更通用或适应性更强的程序。然而，很少有支持反射程序的规范和自动验证。我们解决这个问题，通过实现，指定和验证一个反射库使用霍尔逻辑存储过程的简单语言。后者很重要，因为反射元数据是在堆上建模的，因此方法对象将被实现为存储过程。我们验证内存安全以及反射访问者模式的实例，包括反射库的功能正确性。整个验证在我们的（半）自动验证工具Crowfoot中进行。
Computational reflection allows a program to inspect and manipulate the structure or behaviour of itself at runtime. Often this means that it is possible to create more generic or adaptable programs in an elegant way. However, there is little support for specification and automatic verification of reflective programs. We address this problem by implementing, specifying, and verifying a reflective library using a Hoare-logic for a simple language with stored procedures. The latter is important since reflective metadata is modelled on the heap, thus method objects will be realised as stored procedures. We verify memory safety as well as functional correctness of an instance of the reflective visitor pattern, including the reflective library. The entire verification is carried out in our (semi-)automatic verification tool Crowfoot.