程序验证(十一):演绎验证(下)

Tattoo

发布日期: 2020-07-03 10:12:16 浏览量: 21
评分:
star star star star star star star star star star
*转载请注明来自write-bug.com

版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。
原文链接:https://blog.csdn.net/swy_swy_swy/article/details/106797717

一、新特征引入

向Imp语言引入新的特征:

  • 断言注释(assertion annotation)

  • 过程(procedure)

1.1 断言

断言注释具有以下形式:

{P}\{P\}

从语义上说,它们与运行时断言(runtime assertion)一样(比如c里面的assert)。如果当前环境使得断言表达式为假,程序停止执行。

1.2 程序

举个例子:

这个过程就是一个带有注释的过程:

  • 前置条件由requires注释

  • 后置条件由ensures注释

  • 前置条件与后置条件中的自由变量可以是形式参数

  • 后置条件也可以包括特殊的变量rvrv,代表返回值(return value)

二、部分正确性的证明

一个程序(program)是部分正确的,如果对于它的每个过程(procedure)PP都有:

  • 只要PP的前置条件在过程的入口处被满足

  • 那么PP的后置条件一定在过程的出口处被满足

我们从基本思路:

  • 使用注释(annotation)把程序分为更简单的几部分

  • 独立地为每个部分生成vcvc,假定每个注释都成立

  • 根据每个部分的正确性,推出整体的正确性

2.1 基本路径(Basic Paths)

一个基本路径是一系列指令,满足:

  • 开始于一个过程的前置条件或循环不变量

  • 终止于一个循环不变量,一个断言或一个过程的后置条件

  • 不穿过循环:循环不变量只在路径的开头或结尾出现

2.2 假设(assume)语句

assume b的意思:

  • 只有当b在当前环境下为真,路径的剩余部分才可以执行

  • 当讨论剩余的路径时,我们可以假定b成立

2.3 路径分割

每一个assume,都引入两个分支,一个假定bb成立,一个假定¬b\neg b成立,所以在之前的例子里,有更多的基本路径。

如何计算基本路径有多少呢?当我们计算基础路径的数量时,我们遵循深度优先的习惯。

当遇到一个assume时:

  • 先假定它成立,然后生成相应的路径

  • 再假定它不成立,重复

2.4 过程调用(Procedure Call)

可以把过程调用替换为后置条件断言,需要引入另一个基础路径以确保前置条件成立,将前置条件与后置条件中的形式参数换为在调用中真正出现的参数。

综上,过程调用的步骤为:

1.给定一个过程ff具有以下原型:

2.当ff在上下文w:=f(e1,..,en)w:=f(e_1 ,.. ,e_n)中被调用时,用断言{P[e1,..,en]}\lbrace P[e_1,.. ,e_n] \rbrace表示调用上下文

3.在穿过调用的路径中

  • 创建新的变量vv来存放返回值

  • 将调用替换为后置条件的假定:

三、vc生成

当我们列举基础路径时,我们实际上得到了vcvc

注意,由于基础路径不穿过循环,所以我们只需要为三种命令生成vcvc

  • 赋值:见上文

  • 序列:见上文

  • assume

举例:

上传的附件

发送私信

人生最好的三个词:久别重逢,失而复得,虚惊一场

48
文章数
33
评论数
最近文章
eject