Monad-Independent Hoare Logic in HASCASL
Monad-Independent Hoare Logic in HASCASL
复制标题
HACASL 中独立于 Monad 的霍尔逻辑
DOI：
10.1007/3-540-36578-8_19
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Till Mossakowski
中科院分区：
文献类型：
--
作者：
Lutz Schröder;Till Mossakowski
monad已经被Moggi认可为在函数式编程语言中处理有状态计算的优雅设备。因此，开发霍尔演算来对计算单元进行推理是很自然的。虽然以前只对状态单子做过这样的工作，但我们在这里提供了一种通用的、独立于单子的方法，它也适用于进一步的计算单子，如异常、输入/输出和非确定性。所有这些都在HASCASL的逻辑中形式化，HASCASL是一种用于功能规范和编程的高级语言。单元特征的组合可以通过组合它们的松散规范来获得。作为一个应用，我们证明了欧几里得算法的Dijkstra的不确定版本在一个不确定动态引用的单节点上的部分正确性。
Monads have been recognized by Moggi as an elegant device for dealing with stateful computation in functional programming languages. It is thus natural to develop a Hoare calculus for reasoning about computational monads. While this has previously been done only for the state monad, we here provide a generic, monad-independent approach, which applies also to further computational monads such as exceptions, input/output, and non-determinism. All this is formalized within the logic of HASCASL, a higher-order language for functional specification and programming. Combination of monadic features can be obtained by combining their loose specifications. As an application, we prove partial correctness of Dijkstra's nondeterministic version of Euclid's algorithm in a monad with nondeterministic dynamic references.