Formal validation 笔记 - building boolean formula

Formal Model

state：状态，系统在某一时刻的变量的值。
transition： 变迁（转移），给定状态下，行为发生前后的变化。
computation：计算，无限状态序列变迁的过程。
Kripke structure (KS)：先把程序转化成一阶逻辑公式，再转换成KS（4-tuple），定义 $M=(S,S0,R,L)$，其中
$AP$: （atomic propositions）原子命题的集合。
$S$: 状态的有限集合。
S 0 ⊆ S S_0\sube S S0​⊆S: 初始状态集合。
$R\subseteq S\times S$ (笛卡尔乘积的)子集，一个total的变迁
(Total定义：每个 s ∈ S，存在 s’ ∈ S，如此的R(s,s’))
L : S → 2 A P L: S\to 2^{AP} L:S→2AP 标签函数，标识某状态下的。

举例：

A P = { a , b , c } AP=\{ a,b,c \} AP={a,b,c} （所有）
S = { s 0 , s 1 , s 2 } S=\{s0, s1,s2\} S={s0,s1,s2} （图中圆圈所示）
s 0 = { a , b } s_0=\{a,b\} s0​={a,b}（图中s0）
R ( s 0 , s 1 ) = 箭 头 1 ， R ( s 0 , s 2 ) = 箭 头 2 ， R ( s 1 , s 2 ) = 箭 头 3 ， R ( s 2 , s 0 ) = 箭 头 4 R(s_0,s_1)=箭头1，R(s_0,s_2)=箭头2，R(s_1,s_2)=箭头3，R(s_2,s_0)=箭头4 R(s0​,s1​)=箭头1，R(s0​,s2​)=箭头2，R(s1​,s2​)=箭头3，R(s2​,s0​)=箭头4
L ( s 0 ) = { a , b } ， L ( s 1 ) = { a , c } ， L ( s 2 ) = { b } L(s_0)=\{a,b\}，L(s_1)=\{a,c\}，L(s_2)=\{b\} L(s0​)={a,b}，L(s1​)={a,c}，L(s2​)={b}

一阶逻辑公式

• V = { v 1 , … , v n } V=\{v_1,…,v_n\} V={v1​,…,vn​}是变量的集合，如： < v 1 ← 2 , v 2 ← 3 , v 3 ← 5 > <v1​←2,v2​←3,v3​←5>，将其公式化： ( v 1 = 2 ) ∧ ( v 2 = 3 ) ∧ ( v 3 = 5 ) (v_1=2) \land(v_2=3) \land (v_3=5) (v1​=2)∧(v2​=3)∧(v3​=5)
• V ′ = { < v 1 ← 1 , v 2 ← 5 , v 3 ← 4 > } V'=\{\} V′={<v1​←1,v2​←5,v3​←4>}，公式化为 ( v 1 ′ = 1 ) ∧ ( v 2 ′ = 5 ) ∧ ( v 3 ′ = 4 ) (v_1'=1 ) \land (v_2'= 5) \land (v_3'= 4) (v1′​=1)∧(v2′​=5)∧(v3′​=4)
• 那么，其变迁为表示为： R ( V , V ′ ) ≡ ( v 1 = 2 ∧ v 2 = 3 ∧ v 3 = 5 ) ∧ ( v 1 ′ = 1 ∧ v 2 ′ = 5 ∧ v 3 ′ = 4 ) R(V, V' )\equiv (v_1=2 \land v_2=3 \land v_3=5) \land(v_1' = 1 \land v_2'= 5 \land v_3'= 4) R(V,V′)≡(v1​=2∧v2​=3∧v3​=5)∧(v1′​=1∧v2′​=5∧v3′​=4)
• 注：其真值不一定为真。

一阶逻辑公式的KS

直接举例：
V = { x , y } , 值 域 为 { 0 , 1 } V=\{x,y\} , 值域为 \{0,1\} V={x,y},值域为{0,1}
S 0 ( x , y ) ≡ x = 1 ∧ y = 1 S_0(x,y)\equiv x=1\land y=1 S0​(x,y)≡x=1∧y=1
Transition: R ( x , y , x ′ , y ′ ) ≡ x ′ = ( x + y ) m o d 2 ∧ y ′ = y R(x,y,x',y')\equiv x'=(x+y) mod 2 \land y'=y R(x,y,x′,y′)≡x′=(x+y)mod2∧y′=y
则 K S = ( S , S 0 , R , L ) ？ KS=(S,S_0,R,L)？ KS=(S,S0​,R,L)？

题中S集合有:
S 0 ( x , y ) ≡ x = 1 ∧ y = 1 S_0(x,y)\equiv x=1\land y=1 S0​(x,y)≡x=1∧y=1
S 1 ( x , y ) ≡ x ′ = 0 ∧ y = 1 S_1(x,y)\equiv x'=0 \land y=1 S1​(x,y)≡x′=0∧y=1
S 2 ( x , y ) ≡ x ′ = 0 ∧ y = 0 S_2(x,y)\equiv x'=0 \land y=0 S2​(x,y)≡x′=0∧y=0
S 3 ( x , y ) ≡ x ′ = 1 ∧ y = 0 S_3(x,y)\equiv x'=1 \land y=0 S3​(x,y)≡x′=1∧y=0
题中的变迁有：
S0–>S1
S1–>S0
S2–>S2
S3–>S3

KS图：（flowchart画的不好）

注意：

1. 状态变迁时，其中一个子变量的变迁，用函数表示为： v i → v i ′ = f i ( V ) v_i \to v_i' = f_i(V) vi​→vi′​=fi​(V)
2. R i ( V , V ′ ) ≡ f i ( V ) R_i(V, V') \equiv f_i(V) Ri​(V,V′)≡fi​(V)
3. R ( V , V ’ ) ≡ R 0 ( V , V ′ ) ∧ R 1 ( V , V ′ ) ∧ … ∧ R n − 1 ( V , V ′ ) R(V, V’) \equiv R_0(V, V') \land R_1(V, V') \land… \land R_{n-1}(V, V') R(V,V’)≡R0​(V,V′)∧R1​(V,V′)∧…∧Rn−1​(V,V′)

代码的状态变迁

对于一段代码，我们用 P L P^L PL进行标记：

1. 简单语句（如赋值;skip;wait,lock,unlock等）， P L = P P^L=P PL=P
   assignment:
   C ( l , v ← e , l ′ ) ≡ p c = l ∧ p c ′ = l ′ ∧ v ′ = e ∧ s a m e ( V { v } ) C (l, v\leftarrow e, l' )\equiv pc=l \land pc'=l' \land v'=e \land same(V\{v\}) C(l,v←e,l′)≡pc=l∧pc′=l′∧v′=e∧same(V{v})
   解释：从$l$ 跳到 l ′ l' l′,$v$赋值变成了 v ′ v' v′, 可以表示为： 执行前$pc$是$l$，执行后 p c ′ pc' pc′是 l ′ l' l′，$v$变成了$e$，$V$中除了$v$，其他不变.
   skip:
   C ( l , s k i p , l ′ ) ≡ p c = l ∧ p c ′ = l ′ ∧ s a m e ( V ) C (l, skip, l' )\equiv pc=l \land pc'=l' \land same(V) C(l,skip,l′)≡pc=l∧pc′=l′∧same(V)
   解释：skip语句前后没什么变化，只是语句从$l$跳到了 l ′ l' l′.

2. 复合多条语句（ P 1 ; P 2 P_1;P_2 P1​;P2​）， P L = P 1 L ; l ′ ′ : P 2 L P^L=P_1^L; l'' : P_2^L PL=P1L​;l′′:P2L​
   Sequential composition :
   C ( l , P 1 ; l ′ ′ : P 2 , l ′ ) ≡ C ( l , P 1 , l ′ ′ ) ∨ C ( l ′ ′ , P 2 , l ′ ) C (l,P_1; l'':P_2, l' )\equiv C (l, P_1, l'') \lor C (l'',P_2, l' ) C(l,P1​;l′′:P2​,l′)≡C(l,P1​,l′′)∨C(l′′,P2​,l′)

3. 条件语句（ i f b t h e n P 1 e l s e P 2 e n d i f if\ b\ then\ P_1\ else\ P_2\ endif if b then P1​ else P2​ endif)，
   P L = i f b t h e n l 1 : P 1 L e l s e l 2 : P 2 L e n d i f P^L=if\ b\ then\ l_1: P_1^L\ else\ l_2:P_2^L\ endif PL=if b then l1​:P1L​ else l2​:P2L​ endif
   conditional：
   C ( l , i f b t h e n l 1 : P 1 e l s e l 2 : P 2 e n d i f , l ′ ) C (l, if\ b\ then\ l_1 : P_1\ else\ l_2:P_2\ endif, l') C(l,if b then l1​:P1​ else l2​:P2​ endif,l′)
   转化为如下四条语句：
   b 真： p c = l ∧ p c ′ = l 1 ∧ b ∧ s a m e ( V ) pc=l \land pc'=l_1 \land b \land same(V) pc=l∧pc′=l1​∧b∧same(V)
   b 假： p c = l ∧ p c ′ = l 1 ∧ ¬ b ∧ s a m e ( V ) pc=l \land pc'=l_1 \land \neg b \land same(V) pc=l∧pc′=l1​∧¬b∧same(V)
   b 真则执行： C ( l 1 , P 1 , l ′ ) C (l_1, P_1, l') C(l1​,P1​,l′)
   b 假则执行： C ( l 2 , P 2 , l ′ ) C (l_2, P_2, l' ) C(l2​,P2​,l′)

4. 循环语句（while b do P 1 P_1 P1​ endwhile），
   P 1 P_1 P1​ 前标记为 l 1 l_1 l1​
   C ( l , w h i l e b d o l 1 : P 1 e n d w h i l e , l ′ ) C (l, while\ b\ do\ l_1: P_1\ endwhile, l' ) C(l,while b do l1​:P1​ endwhile,l′)
   转化为如下3条语句：
   b真则 l → l 1 l \to l_1 l→l1​：① p c = l ∧ p c ′ = l 1 ∧ b ∧ s a m e ( V ) pc=l \land pc'=l_1 \land b \land same(V) pc=l∧pc′=l1​∧b∧same(V)
   b假则跳出循环 l → l ′ l \to l' l→l′： ② p c = l 1 ∧ p c ′ = l ′ ∧ ¬ b ∧ s a m e ( V ) pc=l_1 \land pc'=l ' \land \neg b \land same(V) pc=l1​∧pc′=l′∧¬b∧same(V)
   唯一的一个Transition procedure ，是 P 1 P_1 P1​执行前 l 1 l_1 l1​到执行后$l$（因为执行完会回到while去判断真假）：③ C ( l 1 , P 1 , l ) C (l_1, P_1, l ) C(l1​,P1​,l)

题目：

building boolean formula for the following program, while
V = { x , y , z } , i n i t i a l v a l u e : x = y = z = 0 V=\{x,y,z\},\ initial\ value: x=y=z=0 V={x,y,z}, initial value:x=y=z=0
Program
$x=y+1;z=z+2;$
$for(y;y<=3;y++)$
    $ifx<ythenx++;elsey++;$

三句话分别为：
① C ( l , x ′ = y + 1 , l 1 ) ∨ C ( l 1 , z ′ = z + 2 , l 2 ) C (l, x'=y+1, l_1) \lor C (l_1, z'=z+2, l_2) C(l,x′=y+1,l1​)∨C(l1​,z′=z+2,l2​)
② for循环转化为while语句： C ( l 2 , w h i l e ( y < = 3 ) d o l 3 ; l 4 : y + + ; e n d w h i l e , l ′ ) C (l_2, while\ (y<=3)\ do\ l_3; l_4: y++; \ endwhile, l' ) C(l2​,while (y<=3) do l3​;l4​:y++; endwhile,l′)
③ C ( l 3 , i f ( x < y ) t h e n l 5 : ( x + + ) ; e l s e l 6 : ( y + + ) ; e n d i f , l 4 ) C( l_3, if\ (xC(l3​,if (x<y) then l5​:(x++); else l6​:(y++);endif,l4​)

答案：

p c = l ∧ p c ’ = l 1 ∧ x ’ = y + 1 ∧ s a m e ( V / { x } ) pc= l ∧ pc’=l_1 ∧ x’=y+1 ∧ same(V/\{x\}) pc=l∧pc’=l1​∧x’=y+1∧same(V/{x})
∨
p c = l 1 ∧ p c ’ = l 2 ∧ z ’ = z + 2 ∧ s a m e ( V / { z } ) pc= l_1 ∧ pc’=l_2 ∧ z’=z+2 ∧ same(V/\{z\}) pc=l1​∧pc’=l2​∧z’=z+2∧same(V/{z})
∨
p c = l 2 ∧ p c ’ = l 3 ∧ y < = 3 ∧ s a m e ( V ) pc= l_2 ∧ pc’=l_3 ∧ y<=3 ∧ same(V) pc=l2​∧pc’=l3​∧y<=3∧same(V)
∨
p c = l 2 ∧ p c ’ = l ’ ∧ ¬ y < = 3 ∧ s a m e ( V ) pc= l_2 ∧ pc’=l’ ∧ \neg y<=3 ∧ same(V) pc=l2​∧pc’=l’∧¬y<=3∧same(V)【⭐️ end】
∨
p c = l 3 ∧ p c ′ = l 5 ∧ x < y ∧ s a m e ( V ) pc=l_3 ∧ pc'=l_5 ∧xpc=l3​∧pc′=l5​∧x<y∧same(V)
∨
p c = l 3 ∧ p c ′ = l 6 ∧ ¬ x < y ∧ s a m e ( V ) pc=l_3 ∧ pc'=l_6 ∧ \neg xpc=l3​∧pc′=l6​∧¬x<y∧same(V)
∨
p c = l 5 ∧ p c ′ = l 4 ∧ x ’ = x + 1 ∧ s a m e ( V / { x } ) pc=l_5∧ pc'=l_4 ∧x’=x+1 ∧same(V/\{x\}) pc=l5​∧pc′=l4​∧x’=x+1∧same(V/{x})
∨
p c = l 6 ∧ p c ′ = l 4 ∧ y ’ = y + 1 ∧ s a m e ( V / { y } ) pc=l_6∧ pc'=l_4 ∧y’=y+1 ∧same(V/\{y\}) pc=l6​∧pc′=l4​∧y’=y+1∧same(V/{y})
∨
p c = l 4 ∧ p c ’ = l 2 ∧ y ’ = y + 1 ∧ s a m e ( V / { y } ) pc= l_4 ∧ pc’=l_2 ∧ y’=y+1 ∧ same(V/\{y\}) pc=l4​∧pc’=l2​∧y’=y+1∧same(V/{y}) 【⭐️ 循环中y++】

——未完待续——

本文来自互联网用户投稿，文章观点仅代表作者本人，不代表本站立场，不承担相关法律责任。如若转载，请注明出处。 如若内容造成侵权/违法违规/事实不符，请点击【内容举报】进行投诉反馈！