排序方式： 共有3条查询结果，搜索用时 0 毫秒
1
1.
Hoare在1969年提出了关于程序部分正确性推导的形式系统,已经有不少文章讨论它的完全性问题。但是对于该系统判定问题,即对于任意(一级)公式P,Q及语句S,断言P{S}Q是否可证明的判定问题,还未见讨论。初看来,这问题的答案似乎是明显的:一方面,1—P{x:=x}Q等价于1—P→Q,所以如果在Hoare系统中关于一级逻辑部 相似文献
2.
<正> 一、前言 操作系统的实现语言一般应满足以下的要求: (1)应有足够的表示能力,能描述出操作系统的各部分的算法。 (2)应有足够的检验能力,能由编译系统查出尽可能多的错误。 (3)应有较好的可阅读性。 相似文献
3.
两年一度的J.McCarthy奖是为表彰在程序验证领域的杰出工作而设立的。首次奖是根据最近五年在该领域发表的研究工作评定的。美国德克萨斯大学的R.S.Boyer和J S.Moore被评选为首次获奖人。Boyer和Moore从七十年代就合作研究定理证明和程序验证。他们的主要成就是成功地发展了一种可实现高效率的定理证明系统的严谨的逻辑。这种逻辑特别强调了归纳法的使用以表现程序共有的属性。他们的系统是现今最有效的定理证明系统之一。该系统使用启发式来加强其自动定理证明的功能,并允许用户通过人权交换来推导不能由机器完全自动完成的证明。他们还扩充了该系统,使之包括一个FORTRAN验证条件产生程序,使该系统可以处理FORTRAN这 相似文献
1