Executing and verifying higher-order functional-imperative programs in Maude
Executing and verifying higher-order functional-imperative programs in Maude
复制标题
DOI：
10.1016/j.jlamp.2017.09.002
复制
发表时间：
2017-12
期刊：
影响因子：
--
通讯作者：
Vlad Rusu;Andrei Arusoaie
中科院分区：
文献类型：
--
作者：
Vlad Rusu;Andrei Arusoaie
我们在Maude中加入了高阶函数和状态单数，从而在Maude框架中嵌入了一种具有命令性功能的高阶函数式语言。我们通过结果语言中的简单程序来说明：程序的具体和符号执行；它们关于以可达性逻辑表示的性质的验证，这是Hoare逻辑的语言参数推广；以及程序等价性质的验证。我们的方法被证明是可靠的，并通过充分利用其反射特性和模块系统在Maude中实现。
We incorporate higher-order functions and state monads in Maude, thereby embedding a higher-order functional language with imperative features in the Maude framework. We illustrate, via simple programs in the resulting language: the concrete and symbolic execution of programs; their verification with respect to properties expressed in Reachability Logic, a language-parametric generalisation of Hoare Logic; and the verification of program-equivalence properties. Our approach is proved sound and is implemented in Full Maude by taking advantage of its reflective features and module system.