The Typed Logic of Partial Functions and the Vienna Development Method
The Typed Logic of Partial Functions and the Vienna Development Method
复制标题
偏函数的类型化逻辑和维也纳展开法
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
J. Fitzgerald
中科院分区：
文献类型：
--
作者：
J. Fitzgerald
关于支撑形式化规范语言的逻辑的决定对形式化的效用有重要的影响。本章描述了部分函数的类型化逻辑（LPF）的主要特性，因为它是为了支持维也纳开发方法的规范语言VDM-SL而实现的。它比较了在不同环境中实现逻辑的尝试：以用户为中心的证明支持工具，规范解释器和自动证明工具。提出了该语言集成证明支持的未来发展方向。
Decisions about the logic underpinning a formal specification language have important consequences for the utility of the formalism. This chapter describes the major features of the typed Logic of Partial Functions (LPF) as it has been implemented in support of the Vienna Development Method’s Specification Language, VDM-SL. It compares attempts to realise the logic in different environments: a usercentred proof support tool, a specification interpreter and an automated proof tool. Future directions in integrated proof support for the language are suggested.