程序验证(八):形式语义

Tattoo

发布日期: 2020-07-01 11:58:25 浏览量: 20
评分:
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/106698807

一、语义描述方法

  • 操作语义:用抽象机描述程序执行引起的状态改变,关心状态改变是怎样产生的,与语言的实现关系紧密

  • 指称语义:使程序执行的效果对应数学对象,只关心程序执行的效果,不关心其是怎样产生的

  • 公理语义:将程序的语义性质表示为命题,采用数理逻辑的方法研究

二、引入玩具语言Imp

2.1 语法范畴

  • 数字集NumNum,用nn表示数字

  • 变元集VarVar,用xx表示变元

  • 算术表达式集AexpAexp,用aa表示算术表达式

  • 布尔表达式集BexpBexp,用bb表示布尔表达式

  • 语句集ComCom,用cc表示语句

2.2 语法

aAExp::=nZxVara1+a2a1a2a1a2a\in AExp::=n\in Z |x\in Var|a_1+a_2|a_1*a_2|a_1-a_2

bBExp::=truefalsea1=a2a1a2¬bb1b2b\in BExp::=true|false|a_1=a_2|a_1\le a_2|\neg b|b_1\wedge b_2

cCom::=skipx:=ac1;c2if b then c1 else c2while b do cc\in Com::=skip|x:=a|c_1;c_2|if~b~then~c_1~else~c_2|while~b~do~c

三、表达式语义

3.1 表达式的语义

采用二进制

n::=01n0n1n::=0|1|n0|n1

语义函数N:NumZN: Num \to Z

N[0]=0N[0]=0

N[1]=1N[1]=1

N[n0]=2N[0]N[n0]=2*N[0]

N[n1]=2N[n]+1N[n1]=2*N[n]+1

3.2 状态

环境是从变元集到整数集的函数

Env=VarZEnv=Var \to Z

  • σ=[x5,y7,z0]\sigma = [x \mapsto 5,y \mapsto 7,z \mapsto 0],即σx=5,σy=7,σz=0\sigma x=5,\sigma y=7,\sigma z=0

  • σ=σ[x7]\sigma^{\prime} =\sigma [x\mapsto 7],则σx=7\sigma^{\prime} x=7,对于不同于xx的变元yyyσy=σyy\sigma^{\prime} y=\sigma y

状态是一个二元组c,σ\langle c,\sigma\rangle,其中σ\sigma是当前变量的赋值,cc为下一条被执行的语句。

3.3 算术表达式的语义

语义函数A:Aexp(EnvZ)A: Aexp\to (Env\to Z)

  • A[n]σ=N[n]A[n]\sigma = N[n]

  • A[x]σ=σxA[x]\sigma = \sigma x

  • A[a1+a2]σ=A[a1]σ+A[a2]σA[a_1+a_2]\sigma = A[a_1]\sigma +A[a_2]\sigma

  • A[a1a2]σ=A[a1]σA[a2]σA[a_1a_2]\sigma = A[a_1]\sigma A[a_2]\sigma

  • A[a1a2]σ=A[a1]σA[a2]σA[a_1-a_2]\sigma = A[a_1]\sigma -A[a_2]\sigma

3.4 布尔表达式的语义

语义函数B:Bexp(EnvT)B:Bexp\to (Env\to T)

B[true]σ=trueB[true]\sigma = true

B[false]σ=falseB[false]\sigma = false

B[a1=a2]σ=A[a1]σ=A[a2]σB[a_1=a_2]\sigma = A[a_1]\sigma = A[a_2]\sigma

B[a1a2]σ=A[a1]σA[a2]σB[a_1\le a_2]\sigma = A[a_1]\sigma\le A[a_2]\sigma

B[¬b]σ=¬B[b]σB[\neg b]\sigma = \neg B[b]\sigma

B[b1b2]σ=B[b1]σB[b2]σB[b_1\wedge b_2]\sigma = B[b_1]\sigma\wedge B[b_2]\sigma

3.5 举例

在环境σ=[x1,y3]\sigma = [x\mapsto 1,y\mapsto 3]下计算表达式(x+2)y(x+2)*y的值

A[(x+2)y]σ=A[(x+2)]σA[y]σ=(A[x]σ+A[2]σ)A[y]σ=(1+2)3=9A[(x+2)*y]\sigma =A[(x+2)]\sigma * A[y]\sigma = (A[x]\sigma +A[2]\sigma) * A[y]\sigma =(1+2)* 3 = 9

3.6 代入

用算术表达式a0a_0替换算术表达式aa中变元yy的所有出现得到的算术表达式记为a[ya0]a[y\mapsto a_0]

A[a[ya0]]σ=A[a](σ[yA[a0]σ])A[a[y\mapsto a_0]]\sigma = A[a](\sigma [y\mapsto A[a_0]\sigma ])

用算术表达式a0a_0替换布尔表达式bb中变元yy的所有出现得到的布尔表达式记为b[ya0]b[y\mapsto a_0]

B[b[ya0]]σ=B[b](σ[yA[a0]σ])B[b[y\mapsto a_0]]\sigma = B[b](\sigma [y\mapsto A[a_0]\sigma])

四、操作语义

4.1 概念

包括以下两种:

  • 结构操作语义(小步操作语义):描述执行语句的各步计算如何发生

  • 自然语义(大步操作语义):描述如何得到语句执行终止的最终状态

4.2 结构操作语义

结构操作语义强调计算的具体步骤,基于状态之间的迁移关系\to来定义,即

c,σc,σ\langle c,\sigma\rangle\to\langle c',\sigma'\rangle

意义:语句cc从环境σ\sigma执行到中途,这时环境为σ\sigma^{\prime},待执行的语句为cc^{\prime}

反复应用上面的迁移关系,直至程序终止状态skip,σ\langle skip, \sigma \rangle

若无状态c,σ\langle c^{\prime}, \sigma^{\prime} \rangle使得c,σc,σ\langle c,\sigma \rangle \to\langle c^{\prime},\sigma^{\prime} \rangle,则称c,σ\langle c,\sigma\rangle是呆滞的(stuck)。

4.2.1 Imp的结构操作语义

Asgn:x:=a,σskip,σ[xA[a]σ]Asgn:\frac{}{\langle x:=a,\sigma\rangle\to\langle skip,\sigma [x\mapsto A[a]\sigma]\rangle}

Skip:no ruleSkip:no~rule

Seq1:c1,σc1,σ1c1;c2,σc1;c2,σSeq1:\frac{\langle c_1,\sigma\rangle\to\langle c'_1,\sigma'_1\rangle}{\langle c_1;c_2,\sigma\rangle\to\langle c'_1;c_2,\sigma'\rangle}

Seq2:skip;c,σc,σSeq2:\frac{}{\langle skip;c,\sigma\rangle\to\langle c,\sigma\rangle}

IfTrue:if b then c1 else c2,σc1,σIfTrue:\frac{}{\langle if~b~then~c_1~else~c_2,\sigma\rangle\to\langle c_1,\sigma\rangle}

IfFalse:if b then c1 else c2,σc2,σIfFalse:\frac{}{\langle if~b~then~c_1~else~c_2,\sigma\rangle\to \langle c_2,\sigma\rangle}

While:while b do c,σif b then(c;while b do c)else skip,σWhile:\frac{}{\langle while~b~do~c,\sigma\rangle\to\langle if~b~then(c;while~b~do~c)else~skip,\sigma}

4.2.2 推导序列

语句cc从环境σ\sigma开始的推导序列有以下两种形式(记γ0=c,σ\gamma_0=\langle c,\sigma\rangle):

  • 有限状态序列γ0,γ1,..,γk\gamma0,\gamma_1,..,\gamma_k,其中γ0γ1,..,γ\gamma_0\to \gamma_1,..,\gamma{k-1}\to \gamma_k可以推导得出。γk\gamma_k的形式为skip,σ\langle skip,\sigma^{\prime} \rangle或者γk\gamma_k是呆滞的

  • 无限状态序列γ0,γ1,..\gamma_0,\gamma_1,..,其中γ0γ1\gamma_0\to \gamma_1γ1γ2\gamma_1\to\gamma_2等可以推导得到

  • γ0γ1..γk\gamma_0\to \gamma_1\to .. \to\gamma_k简记为γ0γk\gamma_0 \to ^{*}\gamma_k

4.2.3 确定性

结构操作语义具有确定性:对于任意语句cc,从任意环境σ\sigma出发,只要c,σc,σ\langle c,\sigma\rangle\to\langle c^{\prime},\sigma^{\prime}\ranglec,σc,σ\langle c,\sigma\rangle\to\langle c^{\prime\prime},\sigma^{\prime\prime}\rangle,就有σ=σ\sigma^{\prime}=\sigma^{\prime\prime}

4.2.4 终止和循环

  • 若存在从状态c,σ\langle c,\sigma\rangle开始的有限推导序列,则称语句cc从环境σ\sigma执行是终止的

  • 若存在从状态c,σ\langle c,\sigma\rangle开始的无限推导序列,则称语句cc从环境σ\sigma执行是循环的

  • 若语句cc从每个环境执行都是终止的,则称语句cc总是终止的

  • 若语句cc从每个环境执行都是循环的,则称语句cc总是循环的

4.2.5 语义等价

如果对于任意状态σ\sigma,满足下列条件:

  • 对于任意终止或呆滞格局c,σ\langle c^{\prime},\sigma^{\prime}\ranglec1,σc,σ\langle c_1,\sigma\rangle \to^{*} \langle c^{\prime},\sigma^{\prime}\rangle,当且仅当c2,σc,σ\langle c_2,\sigma\rangle \to^{*} \langle c^{\prime},\sigma^{\prime}\rangle

  • 存在从c1,σ\langle c_1,\sigma\rangle开始的无限推导序列当且仅当存在从c2,σ\langle c_2,\sigma\rangle开始的无限推导序列,则称语句c1c_1c2c_2是语义等价的,如语句c1;(c2;c3)c_1;(c_2;c_3)和语句(c1;c2);c3(c_1;c_2);c_3是语义等价的

4.2.6 语义函数

可将语句cc的意义概括为从EnvEnvEnvEnv的部分函数:

SSOS:Cmd(EnvEnv)S_{SOS} : Cmd\to(Env\hookrightarrow Env)

定义

例如,SSOS[while true do skip]σ=undefS_{SOS}[while \space true \space do \space skip]\sigma = undef

4.3 自然语义

自然语义关心语句执行对环境的改变。

从环境σ\sigma执行语句cc将终止于环境σ\sigma^{\prime}

c,σσ\langle c,\sigma\rangle\Downarrow \sigma^{\prime}

规则的一般形式:

4.3.1 Imp的自然语义

每个规则有若干前提和一个结论。称有0个前提的规则为公理,如BigAsgn, BigSkip, BigWhileFalse是公理。

当使用公理和规则得出c,σσ\langle c,\sigma\rangle\Downarrow \sigma^{\prime}时,就得到一推导树,树根是c,σσ\langle c,\sigma\rangle\Downarrow \sigma^{\prime},树叶是公理,每个分支点是某规则的结论,而它的儿子是该规则的前提。

4.3.2 终止和循环

  • 若存在环境σ\sigma^{\prime}使得c,σσ\langle c,\sigma\rangle\Downarrow\sigma^{\prime},则称语句cc从环境σ\sigma执行是终止的

  • 若不存在环境σ\sigma^{\prime}使得c,σσ\langle c,\sigma\rangle\Downarrow \sigma^{\prime},则称语句cc从环境σ\sigma执行是循环的

  • 若语句cc从每个环境执行都是终止的,则称语句cc总是终止的

  • 若语句cc从每个环境执行都是循环的,则称语句cc总是循环的

4.3.3 语义等价

如果对于任意环境σ\sigmaσ\sigma^{\prime}

c0,σσc1,σσ\langle c_0,\sigma\rangle\Downarrow\sigma^{\prime} \Leftrightarrow \langle c_1,\sigma\rangle\Downarrow \sigma^{\prime}

则称语句c0c_0c1c_1是语义等价的。

4.3.4 确定性

自然语义具有确定性:对于任意语句cc,和任意环境σ1,σ2,σ\sigma_1,\sigma_2,\sigma,只要c,σσ1\langle c,\sigma \rangle\Downarrow \sigma_1c,σσ2\langle c,\sigma\rangle\Downarrow \sigma_2,就有σ1=σ2\sigma_1=\sigma_2,即

σ,σ1,σ2,c.(c,σσ1c,σσ2)(σ1=σ2)\forall \sigma,\sigma_1,\sigma_2,c.(\langle c,\sigma\rangle\Downarrow\sigma_1\wedge\langle c,\sigma\rangle\Downarrow\sigma_2)\to (\sigma_1 =\sigma_2)

4.3.5 语义函数

可将语句cc的意义概括为从FnvFnvEnvEnv的部分函数:

Sns:Cmd(EnvEnv)S_{ns}: Cmd\to (Env\hookrightarrow Env)

定义

4.4 两种语义的对比

  • 对于语言Imp的每个语句cc,任意环境σ\sigmaσ\sigma^{\prime},若c,σσ\langle c,\sigma\rangle\Downarrow \sigma^{\prime},则c,σskip,σ\langle c,\sigma\rangle\to^{*}\langle skip,\sigma^{\prime} \rangle

  • 对于语言Imp的每个语句cc,任意环境σ\sigmaσ\sigma^{\prime} ,若c,σkskip,σ\langle c,\sigma\rangle\to^k\langle skip,\sigma^{\prime}\rangle,则c,σσ\langle c,\sigma\rangle\Downarrow\sigma^{\prime}

  • 对于语言Imp的每个语句ccSns[c]=SSOS[c]S_{ns}[c]=S_{SOS}[c]

上传的附件

发送私信

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

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