程序的公理化证明.ppt_第1页
程序的公理化证明.ppt_第2页
程序的公理化证明.ppt_第3页
程序的公理化证明.ppt_第4页
程序的公理化证明.ppt_第5页
已阅读5页，还剩10页未读， 继续免费阅读

下载本文档

版权说明：本文档由用户提供并上传，收益归属内容提供方，若内容存在侵权，请进行举报或认领

文档简介

1、程序公理化证明，赵建华南京大学计算机系统，概述，C.A.R. Hoare提出的公理系统断言包括逻辑表达式和代码组合表达式证明，先证明程序的各个部分，再将这些证明组合起来，证明更大的代码一种程序，其中证明系统基于一阶推论系统，并且断言的形式指示Hoare三元表达式P S Q S :代码p (前置条件) q (后置条件) p和q是一阶逻辑表达式三元表达式s选择： if p then S else S fi循环： while p do S，公理：代入语句，Qe/v v:=e Q语句v 3360=如果e执行前的状态满足Qe/v，则v:=e执行后的状态满足的Qe/v表将公式q中的v置换为e 例如，x 1

2、=10 x:=x 1x=10、公理： skip文件、skip文件不改变状态。 P skip P、pre、post规则在证明断言后，可减弱其后置条件或强化前置条件。 P=P，Q=Q P S Q，Q=Q P S Q，顺序组合规则在证明一个顺序组合句时，可以分别证明两个子句的性质，然后将其组合起来得到组合句整体的性质。 P S1 Q、QS2R P S1。 关于S2 R、if-then-else规则、Pp S1 Q、PPS2q、if-then s1else s2q if语句的意思，如果p成立则执行S1，否则执行S2。 前提条件表示，如果开始状态满足Pp，则在执行S1后满足q。如果开始状态满足Pp，则在执行s后也满足q。如果开始状态满足p，则是满足Pp，还是满足Pp。 从if句的意思可以看出结论是成立的。while规则(部分正确性)、Pp S P Pwhile p do S P P被称为while语句的不变式。 在执行while语句时，这个性质总是成立的。 执行while语句直到p不再成立。 因此，当while语句终止循环时，状态必然满足Pp。 这个性质不确保while语句终止循环，并且while规则(完全正确)与一个函

人人文库> 全部分类> 生活休闲 > 科普知识

温馨提示

  • 1. 本站所有资源如无特殊说明，都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等，如果需要附件，请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸，网页内容里面会有图纸预览，若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对用户上传分享的文档内容本身不做任何修改或编辑，并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容，请与我们联系，我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

最新文档

评论

0/150

提交评论