程序验证(十):演绎验证(上)

2024-03-02 14:32
文章标签 验证 演绎 程序验证

本文主要是介绍程序验证(十):演绎验证(上),希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

程序验证(十):演绎验证(上)

基础路径(Basic Approach)

给定一个程序 c c c,由以下specification注解:
{ P } c { Q } \{P\}c\{Q\} {P}c{Q}
为了证明这个三元组,我们构造一个验证条件(verification condition, VC)的集合

  • 每个VC都是某个理论的一阶公式
  • 如果所有的VC都是永真的,那么 { P } c { Q } \{P\}c\{Q\} {P}c{Q}就是永真的

谓词转换器

给定一个断言 Q Q Q和一个程序 c c c,一个谓词转换器(predicate transformer)是一个函数,输出另一个断言
最弱前置条件(weakest precondition)谓词转换器产生一个 w p ( c , Q ) wp(c,Q) wp(c,Q),使得

  • [ w p ( c , Q ) ] c [ Q ] [wp(c,Q)]c[Q] [wp(c,Q)]c[Q]是永真的,且
  • 对于任何满足 [ P ] c [ Q ] [P]c[Q] [P]c[Q] P P P P ⇒ w p ( c , Q ) P\Rightarrow wp(c,Q) Pwp(c,Q),也就是说, w p ( c , Q ) wp(c,Q) wp(c,Q)是这种断言中最弱的。
    广义最弱前置条件(weakest liberal precondition)谓词转换器产生一个 w l p ( c , Q ) wlp(c,Q) wlp(c,Q),使得
  • { w l p ( c , Q ) } c { Q } \{wlp(c,Q)\}c\{Q\} {wlp(c,Q)}c{Q}是永真的,且
  • w l p ( c , Q ) wlp(c,Q) wlp(c,Q)是这种断言中最弱的
    w l p wlp wlp为我们提供了一种逆向的思路,这也符合我们的直觉。

w l p wlp wlp的定义

我们用霍尔三元组来定义 w l p wlp wlp
比如 w l p ( y : = x + 1 , ( ∀ x . x < z → x < y ) → x + 1 ≤ y ) wlp(y:=x+1, (\forall x.x<z\to x<y)\to x+1\le y) wlp(y:=x+1,(x.x<zx<y)x+1y)=?
注意,答案并不是 ( ∀ x . x < z → x < x + 1 ) → x + 1 ≤ x + 1 (\forall x.x<z\to x<x+1)\to x+1\le x+1 (x.x<zx<x+1)x+1x+1
因为当我们用 x + 1 x+1 x+1替换 y y y以处理 ( ∀ x . x < z → x < y ) (\forall x.x<z\to x<y) (x.x<zx<y)时,变量 x x x是被捕获的(captured)

捕获避免代入(capture-avoiding substitution)

当我们扩展 P [ a / x ] P[a/x] P[a/x]时,我们需要:

  • 只代入 x x x的自由形式(free occurence)
  • a a a中不自由的变量重命名以避免捕获

数组赋值规则

数组赋值的霍尔规则可以表示为:
A s g n A r r { Q [ x ⟨ a 1 ◃ a 2 ⟩ / x ] } x [ a 1 ] : = a 2 { Q } AsgnArr~\frac{}{\{Q[x\langle a_1\triangleleft a_2\rangle /x]\}x[a_1]:=a_2\{Q\}} AsgnArr {Q[xa1a2/x]}x[a1]:=a2{Q}
相应的转换器即为
w l p ( x [ a 1 ] : = a 2 , Q ) = Q [ x ⟨ a 1 ◃ a 2 ⟩ / x ] wlp (x[a_1]:=a_2,Q)=Q[x\langle a_1\triangleleft a_2\rangle /x] wlp(x[a1]:=a2,Q)=Q[xa1a2/x]
举例:
计算 w l p ( b [ i ] : = 5 , b [ i ] = 5 ) wlp(b[i]:=5,b[i]=5) wlp(b[i]:=5,b[i]=5)
w l p ( b [ i ] : = 5 , b [ i ] = 5 ) = ( b ⟨ ◃ 5 ⟩ [ i ] = 5 ) = ( 5 = 5 ) = t r u e wlp(b[i]:=5,b[i]=5)=(b\langle\triangleleft 5\rangle [i]=5)=(5=5)=true wlp(b[i]:=5,b[i]=5)=(b5[i]=5)=(5=5)=true
计算 w l p ( b [ n ] : = x , ∀ i . 1 ≤ i < n → b [ i ] ≤ b [ i + 1 ] ) wlp(b[n]:=x,\forall i.1\le i<n\to b[i]\le b[i+1]) wlp(b[n]:=x,i.1i<nb[i]b[i+1])
进行代入
w l p ( b [ n ] : = x , ∀ i . 1 ≤ i < n → b [ i ] ≤ b [ i + 1 ] ) = ∀ i . 1 ≤ i < n → ( b ⟨ ◃ x ⟩ ) [ i ] ≤ ( b ⟨ n ◃ x ⟩ ) [ i + 1 ] = ( b ⟨ n ◃ x ⟩ ) [ n − 1 ] ≤ ( b ⟨ n ◃ x ⟩ ) [ n ] ∧ ∀ i . 1 ≤ i < n − 1 → ( b ⟨ n ◃ x ⟩ ) [ i ] ≤ ( b ⟨ n ◃ x ⟩ ) [ i + 1 ] wlp(b[n]:=x,\forall i.1\le i<n\to b[i]\le b[i+1])=\forall i.1\le i<n\to (b\langle\triangleleft x\rangle)[i]\le (b\langle n\triangleleft x\rangle)[i+1]=(b\langle n\triangleleft x\rangle)[n-1]\le (b\langle n\triangleleft x\rangle)[n]\wedge \forall i.1\le i<n-1\to (b\langle n\triangleleft x\rangle)[i]\le (b\langle n\triangleleft x\rangle)[i+1] wlp(b[n]:=x,i.1i<nb[i]b[i+1])=i.1i<n(bx)[i](bnx)[i+1]=(bnx)[n1](bnx)[n]i.1i<n1(bnx)[i](bnx)[i+1]

序列(sequencing)

依据霍尔规则
S e q { P } c 1 { P ′ } { P ′ } c 2 { Q } { P } c 1 ; c 2 { Q } Seq~\frac{\{P\}c_1\{P'\}\qquad\{P'\}c_2\{Q\}}{\{P\}c_1;c_2\{Q\}} Seq {P}c1;c2{Q}{P}c1{P}{P}c2{Q}
相应的谓词转换器即为
w l p ( c 1 ; c 2 , Q ) = w l p ( c 1 , w l p ( c 2 , Q ) ) wlp(c_1;c_2,Q)=wlp(c_1,wlp(c_2,Q)) wlp(c1;c2,Q)=wlp(c1,wlp(c2,Q))

条件

依据霍尔规则
I f { P ∧ b } c 1 { Q } { P ∧ ¬ b } c 2 { Q } { P } i f b t h e n c 1 e l s e c 2 { Q } If~\frac{\{P\wedge b\}c_1\{Q\}\qquad\{P\wedge\neg b\}c_2\{Q\}}{\{P\}\mathbf{if}~b~\mathbf{then}~c_1~\mathbf{else}~c_2\{Q\}} If {P}if b then c1 else c2{Q}{Pb}c1{Q}{P¬b}c2{Q}
相应的转换器即为
w l p ( i f b t h e n c 1 e l s e c 2 , Q ) = ( b → w l p ( c 1 , Q ) ) ∧ ( ¬ b → w l p ( c 2 , Q ) ) wlp(\mathbf{if}~b~\mathbf{then}~c_1~\mathbf{else}~c_2,Q)\\ =(b\to wlp(c_1,Q))\wedge (\neg b\to wlp(c_2,Q)) wlp(if b then c1 else c2,Q)=(bwlp(c1,Q))(¬bwlp(c2,Q))

while循环

依据等价关系
w h i l e b d o c ≡ i f b t h e n c ; w h i l e b d o c e l s e s k i p \mathbf{while}~b~\mathbf{do}~c\equiv \mathbf{if}~b~\mathbf{then}~c;\mathbf{while}~b~\mathbf{do}~c~\mathbf{else}~\mathbf{skip} while b do cif b then c;while b do c else skip
相应的 w l p wlp wlp即为
此处略,最后转了个圈又回来了。

近似最弱前置条件

一般来说,我们无法总是算出循环的 w l p wlp wlp,比如上面的情况。
但是,我们可以借助于循环不变式来近似它
下面,我们使用这种方式表示循环:
w h i l e b d o { I } c \mathbf{while}~b~\mathbf{do}\{I\}c while b do{I}c
这里 I I I是由程序员提供的循环不变量
最为直观的想法是令
w l p ( w h i l e b d o { I } c , Q ) = I wlp(\mathbf{while}~b~\mathbf{do}\{I\}c,Q)=I wlp(while b do{I}c,Q)=I
但此时 I I I可能不是最弱的前置条件
如果我们草率地认为 w l p ( w h i l e b d o { I } c , Q ) = I wlp(\mathbf{while}~b~\mathbf{do}\{I\}c,Q)=I wlp(while b do{I}c,Q)=I,我们漏了两件事情:

  • 没有检查 I ∧ ¬ b I\wedge\neg b I¬b得到 Q Q Q
  • 我们不知道 I I I是否真的是一个循环不变式

所以我们需要构造一个额外的验证条件(verification condition)的集合,
v c ( w h i l e b d o { I } c , Q ) = { I ∧ ¬ b ⇒ Q I ∧ b ⇒ w l p ( c , I ) vc(\mathbf{while}~b~\mathbf{do}\{I\}c,Q)=\begin{cases}I\wedge \neg b\Rightarrow Q\\I\wedge b\Rightarrow wlp(c,I)\end{cases} vc(while b do{I}c,Q)={I¬bQIbwlp(c,I)
为了在执行循环后确保 Q Q Q能够实现,需要满足两个条件:

  • v c ( w h i l e b d o { I } c , Q ) vc(\mathbf{while}~b~\mathbf{do}\{I\}c,Q) vc(while b do{I}c,Q)中的每一个公式都是永真的
  • w l p ( w h i l e b d o { I } c , Q ) = I wlp(\mathbf{while}~b~\mathbf{do}\{I\}c,Q)=I wlp(while b do{I}c,Q)=I一定是永真的

构造vc

while是唯一一个引入额外条件的命令,但是其他的声明可能也包含循环,所以:

  • v c ( x : = a , Q ) = ∅ vc(x:=a,Q)=\empty vc(x:=a,Q)=
  • v c ( c 1 ; c 2 , Q ) = v c ( c 1 , w l p ( c 2 , Q ) ) ∪ v c ( c 2 , Q ) vc(c_1;c_2,Q)=vc(c_1,wlp(c_2,Q))\cup vc(c_2,Q) vc(c1;c2,Q)=vc(c1,wlp(c2,Q))vc(c2,Q)
  • v c ( i f b t h e n c 1 e l s e c 2 , Q ) = v c ( c 1 , Q ) ∪ v c ( c 2 , Q ) vc(\mathbf{if}~b~\mathbf{then}~c_1~\mathbf{else}~c_2,Q)=vc(c_1,Q)\cup vc(c_2,Q) vc(if b then c1 else c2,Q)=vc(c1,Q)vc(c2,Q)

综合

综上,我们得到验证 { P } c { Q } \{P\}c\{Q\} {P}c{Q}的通用方法:

  1. 计算 P ′ = w l p ( c , Q ) P'=wlp(c,Q) P=wlp(c,Q)
  2. 计算 v c ( c , Q ) vc(c,Q) vc(c,Q)
  3. 检查 P → P ′ P\to P' PP的永真性
  4. 检查每个 F ∈ v c ( c , Q ) F\in vc(c,Q) Fvc(c,Q)的永真性

若3,4检验均通过,那么 { P } c { Q } \{P\}c\{Q\} {P}c{Q}是永真的,但反之不一定成立,因为循环不变式可能不是最弱的前置条件。

这篇关于程序验证(十):演绎验证(上)的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/766437

相关文章

Spring Security基于数据库验证流程详解

Spring Security 校验流程图 相关解释说明(认真看哦) AbstractAuthenticationProcessingFilter 抽象类 /*** 调用 #requiresAuthentication(HttpServletRequest, HttpServletResponse) 决定是否需要进行验证操作。* 如果需要验证,则会调用 #attemptAuthentica

C++ | Leetcode C++题解之第393题UTF-8编码验证

题目: 题解: class Solution {public:static const int MASK1 = 1 << 7;static const int MASK2 = (1 << 7) + (1 << 6);bool isValid(int num) {return (num & MASK2) == MASK1;}int getBytes(int num) {if ((num &

C语言 | Leetcode C语言题解之第393题UTF-8编码验证

题目: 题解: static const int MASK1 = 1 << 7;static const int MASK2 = (1 << 7) + (1 << 6);bool isValid(int num) {return (num & MASK2) == MASK1;}int getBytes(int num) {if ((num & MASK1) == 0) {return

easyui同时验证账户格式和ajax是否存在

accountName: {validator: function (value, param) {if (!/^[a-zA-Z][a-zA-Z0-9_]{3,15}$/i.test(value)) {$.fn.validatebox.defaults.rules.accountName.message = '账户名称不合法(字母开头,允许4-16字节,允许字母数字下划线)';return fal

easyui 验证下拉菜单select

validatebox.js中添加以下方法: selectRequired: {validator: function (value) {if (value == "" || value.indexOf('请选择') >= 0 || value.indexOf('全部') >= 0) {return false;}else {return true;}},message: '该下拉框为必选项'}

web群集--nginx配置文件location匹配符的优先级顺序详解及验证

文章目录 前言优先级顺序优先级顺序(详解)1. 精确匹配(Exact Match)2. 正则表达式匹配(Regex Match)3. 前缀匹配(Prefix Match) 匹配规则的综合应用验证优先级 前言 location的作用 在 NGINX 中,location 指令用于定义如何处理特定的请求 URI。由于网站往往需要不同的处理方式来适应各种请求,NGINX 提供了多种匹

React 笔记 父子组件传值 | 父组件调用子组件数据 | defaultProps | propsType合法性验证

1.通过props实现父组件像子组件传值 、方法、甚至整个父组件 传递整个父组件则   [变量名]={this} import Header from "./Header"render(){return(<Header msg={"我是props传递的数据"}/>)} import React,{Component} from "react";class Header extends

Java验证辛钦大数定理

本实验通过程序模拟采集大量的样本数据来验证辛钦大数定理。   实验环境: 本实验采用Java语言编程,开发环境为Eclipse,图像生成使用JFreeChart类。   一,验证辛钦大数定理 由辛钦大数定理描述为: 辛钦大数定理(弱大数定理)  设随机变量序列 X1, X2, … 相互独立,服从同一分布,具有数学期望E(Xi) = μ, i = 1, 2, …, 则对于任意正数ε ,

【python因果推断库11】工具变量回归与使用 pymc 验证工具变量4

目录  Wald 估计与简单控制回归的比较 CausalPy 和 多变量模型 感兴趣的系数 复杂化工具变量公式  Wald 估计与简单控制回归的比较 但现在我们可以将这个估计与仅包含教育作为控制变量的简单回归进行比较。 naive_reg_model, idata_reg = make_reg_model(covariate_df.assign(education=df[

表单验证(WTF)

官方文档 在Flask项目开发中针对提交表单的校验,可以使用Flask-WTF扩展库进行快速的字段校验,也可以进行页面快速渲染,并提供跨站请求伪造的保护功能。 安装Flask-WTF pip install flask-wtf 实现注册功能 注册表单模型定义 在定义的表单类中定义需要验证的username、password和password2字段,并实现如下校验: 校验密码passw