【正文】 五章、 最弱前置謂詞和程序語言的語義 ? 前言 ? 引進最弱前置謂詞（ Weakest Prepredicate）的概念， ? 并用它來定義一個小程序語言 L。該語言的主要成分： ? 賦值語句、 ? 選擇語句、 ? 循環(huán)語句， ? 數(shù)據(jù)類型只有整型和布爾型 最弱前置謂詞 ：假定 S是一個語句， Q是一個謂詞，它描述 S執(zhí)行后所確定的某種關系。從 S和 Q定義另外一個謂詞，記為 wp(S,Q),它表示： “ 所有這樣的狀態(tài)的集合， S從其中任一狀態(tài)開始執(zhí)行必將在有限的時間內(nèi)終止于滿足 Q的狀態(tài) ” 。 ? S ? {wp(S,Q) } { Q } 最弱前置謂詞 我們稱 wp(S,Q) 是語句 S關于 Q的 最弱前置謂詞 。 “ 最弱 ” 反映在 “ 所有 ” 一詞之中，外延最大，內(nèi)涵自然最弱。 最弱前置謂詞 例 1. 假設 S是賦值語句 i := i+1。 Q為 i≤10 則： wp(S,Q) = wp(i := i+1, i≤10 ) = (i ≤9) 最弱前置謂詞 例 2. 假設 S是 if x=y then z:=x else z:=y Q為 z:=max(x,y) 則： wp(S,Q) = T 例 3. 令 S同例 2， Q為 z:=y, 則： wp(S,Q) = (x ≤y) 例 4. 令 S同例 2， Q為 z = y1, 則： wp(S,Q) = FALSE 最弱前置謂詞 wp(S,Q)與 {P} S {Q}： ? {P} S {Q}表示 “ 若 S的執(zhí)行開始于一個滿足 P的狀態(tài)，則 S的執(zhí)行必在有限的時間內(nèi)終止于一個滿足 Q的狀態(tài) ” wp(S,Q)表示 “ 所有這樣的狀態(tài)的集合， S從其中任一狀態(tài)開始執(zhí)行必將在有限的時間內(nèi)終止于滿足 Q的狀態(tài) ” 因此： {P} S {Q} ? ( P ? wp(S,Q)) 基本語句的語義－前言 ? 前言： ? 用 wp定義一個小程序設計語言 L，此語言的表達式只有整型和布爾型兩類，說明語句采用類 Pascal的形式，其基本執(zhí)行語句有空語句（ Skip）、賦值語句、選擇語句、循環(huán)語句。 ? 令記號 “ =df” 為定義符，讀做 “ 定義為 ” 基本語句的語義 空語句 （ Skip） Skip語句表示什么事都不做，相當于空語句。其定義如下： 定義 1： wp(skip,Q) =df Q 基本語句的語義 賦值語句 2. 賦值語句 1）簡單變量賦值 ? 賦值形式： y := e ? 其中 y為簡單變量， e為表達式； y， e必須相同類型。這個語句在某種狀態(tài)下執(zhí)行意味著：首先在此狀態(tài)下計算出 e的值，然后將此值存放在以 y為名字的存儲單元中，即用 e的值代替 y的值。 基本語句的語義 賦值語句 ? 定義 2： wp(“y := e”,Q) =df domain(e) ∧ 其中， domain(e) 是一個謂詞，表示所有使 e可求值的狀態(tài)集。 在多數(shù)情況下， domain(e) 總是成立，故常省略它，只寫： wp(“y := e”,Q) =df yeQyeQ 基本語句的語義 例 1： 例 2： 例 3： 例 4： 5)y,5:yw p ( p ( x ) ),a/ b :xw p ( 0)x,1x:xw p ( 5)x,5:xw p ( ???????? 基本語句的語義 例 1： 例 2： 例 3： 例 4： f a l s e 5)(5 5)y,5:yw p ( p ( a / b ) ) 0(b p ( x ) ),a / b :xw p ( 1 )(x 0)(x 0)x,1x:xw p ( T r u e )5)( ( x 5)x,5:xw p ( x1xx5?????????????????????? 基本語句的語義－ 多個簡單變量的同時賦值 2)多個簡單變量的同時賦值 )(:1:)()(),:(4.,...,2,1。,...,2,1)1(:::eid o m a i nniied o m a i nQed o m a i nQexwpeneenexnxxnxexsxedf??????????其中：定義個表達式為個互不相同的變量為其中例 8： wp(“x,y:=xy,yx”,x+y=c) = （ xy+yx = c） = (0 = c) 基本語句的語義－ 順序復合 3. 順序復合 考慮由兩個語句 s1和 s2構(gòu)成的復合語句 “ s1。s2”的語義： 定義 5： wp(“s1。s2”,Q) =df wp(“s1”,wp(“s2”,Q)) 基本語句的語義－ 順序復合 wp(“s1。s2”,Q) =df wp(“s1”,wp(“s2”,Q)) 例： wp(“t:=x。 x:=y。 y:=t”, x=u2 ∧ y=u1) =wp(“t:=x。 x:=y”,wp(“y:=t”, x=u2 ∧ y=u1)) =wp(“t:=x。 x:=y”, x=u2 ∧ t=u1) =wp(“t:=x”,wp(“x:=y”, x=u2 ∧ t=u1)) =wp(“t:=x”,y=u2 ∧ t=u1) = y=u2 ∧ x=u1 基本語句的語義－ 選擇語句 形式： IF ::= if c1 ? s1。 □ c2 ? s2。 ...... □ ? sn。 fi 其中， n0。 ci為布爾表達式 。 si為任意語句 。 ci ? si是一個帶衛(wèi)哨（ Guard）語句 , ci為 si的衛(wèi)哨 。 用 BB表示所有衛(wèi)哨的析?。? BB = c1∨ c2 ∨ ... ∨ IF語句的執(zhí)行過程： ?首先計算每個 ci， ?若所有 ci都不為真，或 有某個 ci無定義則執(zhí)行中斷（ abort），否則，執(zhí)行任一個其值為真的 ci所對應的 si。 ?當 si執(zhí)行完畢后，整個IF就執(zhí)行完了。 基本語句的語義 ? 定義 6： wp(IF,Q) =df domain(BB) ∧ BB ∧ c1?wp(s1,Q) ∧ c2?wp(s2,Q) ∧ ... ?wp(sn,Q) =df domain(BB) ∧ (?j : 1≤j ≤ n : cj) ∧ (?i : 1≤i ≤ n : ci ? wp(si,Q) ) 基本語句的語義 ? 例：令 IF為 if x=0 ? y := x x=0 ? y := x。 fi Q : y = abs(x) 則： wp(IF, y = abs(x)) = ((x=0 ∨ x=0 )∧ x=0 ? wp(“y := x”, y = abs(x)) ∧ x=0 ?wp(“y := x”, y = abs(x))) = true ∧ x=0 ?x= abs(x) ∧ x=0 ?(x= abs(x)) = true wp(IF,Q)=df domain(BB)∧ BB ∧ c1?wp(s1,Q) ∧ c2?wp(s2,Q) ∧ ... ?wp(sn,Q) 定理 1（ Theorem 1） 考慮 IF命令，假設謂詞 P滿足： (1) P ? BB