Dijkstra Monads for All
Dijkstra Monads for All
摘要：
本文提出了一个通用的语义框架，用于验证程序的任意单子的副作用使用Dijkstra单子，我们定义为单子的结构索引的规范单子。我们证明了计算单子和规范单子之间的任何单子态射都会产生一个Dijkstra单子，这为获得适合手头验证任务的Dijkstra单子提供了很大的灵活性。此外，我们表明，各种规格的单子可以通过应用单子变换到各种基础规格的单子，包括谓词Transformers和霍尔式的前置和后置条件。为了定义正确的单子Transformers，我们提出了一种语言的启发Moggi的单子元语言，参数化的依赖类型论。我们还开发了一个概念的代数运算的Dijkstra单子，并开始调查两种方式也容纳效果处理程序。我们实现我们的框架在Coq和F*，并说明它支持各种各样的验证风格的影响，如异常，非确定性，状态，输入输出，和一般递归。
英文摘要：
This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed by a specification monad. We prove that any monad morphism between a computational monad and a specification monad gives rise to a Dijkstra monad, which provides great flexibility for obtaining Dijkstra monads tailored to the verification task at hand. We moreover show that a large variety of specification monads can be obtained by applying monad transformers to various base specification monads, including predicate transformers and Hoare-style pre- and postconditions. For defining correct monad transformers, we propose a language inspired by Moggi's monadic metalanguage that is parameterized by a dependent type theory. We also develop a notion of algebraic operations for Dijkstra monads, and start to investigate two ways of also accommodating effect handlers. We implement our framework in both Coq and F*, and illustrate that it supports a wide variety of verification styles for effects such as exceptions, nondeterminism, state, input-output, and general recursion.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
