Formal specifications of debuggers
Formal specifications of debuggers
复制标题
调试器的正式规范
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Ming
中科院分区：
文献类型：
--
作者：
Ming
构造型理论中的程序设计对应于数学中的定理证明：规格说明扮演着要证明的命题的角色，程序是从证明中获得的。在本文中，我们提出了一种方法，使用建设性类型理论推导出一个调试程序的给定的编程语言从其指称语义定义。该开发由一个名为PowerEpperity的验证开发系统支持。
Programming in constructive type theory corresponds to theorem proving in mathematics: the specification plays the role of the proposition to be proved and the program is obtained from the proof. In this paper, we present an approach of using constructive type theory to derive a debugger of a given programming language from its denotational semantic definition. The development is supported by a proof development system called PowerEpsilon.