Abstract State Machines, Alloy, B, VDM, and Z
Abstract State Machines, Alloy, B, VDM, and Z
复制标题
抽象状态机、Alloy、B、VDM 和 Z
DOI：
10.1007/978-3-642-30885-7_18
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Jones C
中科院分区：
文献类型：
--
作者：
Jones C
程序的规范经常涉及到没有在其所有（语法）域上定义的操作符和函数。关于规格说明的证明--以及那些在证明设计步骤的合理性时履行证明义务的证明--必须基于形式规则。由于经典逻辑只处理定义的值，因此需要一些额外的思考。有几种方法可以处理无法表示值的术语-本文提供了三种最知名方法的基于语义的比较。此外，还指出了进一步的备选方案。
Specifications of programs frequently involve operators and functions that are not defined over all of their (syntactic) domains. Proofs about specifications –and those to discharge proof obligations that arise in justifying steps of design– must be based on formal rules. Since classical logic deals only with defined values, some extra thought is required. There are several ways of handling terms that can fail to denote a value — this paper provides a semantically based comparison of three of the best known approaches. In addition, some pointers are given to further alternatives.
登录
查看更多内容
经典重构的部分函数的类型化逻辑
影响因子：
0.6
作者：
Cliff B. Jones;K. Middelburg
通讯作者：
K. Middelburg
VDM 中的证明：从业者指南
DOI：
10.1007/978-1-4471-2033-9
发表时间：
1993
期刊：
Int. J. Softw. Informatics
影响因子：
--
作者：
J. Bicarregui;J. Fitzgerald;P. Lindsay;Richard C. Moore;B. Ritchie
通讯作者：
B. Ritchie
部分函数和逻辑：警告
DOI：
10.1016/0020-0190(95)00042-b
发表时间：
1995
期刊：
Inf. Process. Lett.
影响因子：
--
作者：
Cliff B. Jones
通讯作者：
Cliff B. Jones
PLT方案Web服务器的实现与使用
DOI：
--
发表时间：
2007
期刊：
High. Order Symb. Comput.
影响因子：
--
作者：
S. Krishnamurthi;Peter Walton Hopkins;J. McCarthy;P. Graunke;Greg Pettyjohn;M. Felleisen
通讯作者：
M. Felleisen
DOI：
--
发表时间：
2011
期刊：
International Journal of Software and Informatics
影响因子：
--
作者：
Cliff B. Jones
通讯作者：
Cliff B. Jones