1、軟件工程的形式化方法Formal Methods for Software Engineering形式規約部分q 引言為什么需要軟件規約 ？軟件項目開發周期長；軟件系統的生命周期中 ，功能需要更新、調整等以滿足用戶需求；軟件系統可能會包含成百上千萬行的代碼；可能需要不同地域的人們共同進行開發和維護 ；系統可能由很多部分組成 ；q 引言形式化規約（形式規約 formal specification） 是指用具有堅實數學基礎的語言和方法給出的軟件的描述。軟件需求規約從用戶的角度描述了對所需軟件的 各種需求 。軟件的功能和性能規約通常是基于抽象的數學模q 引言軟件設計規約是從可執行的角度描述軟件的數

2、據結 構和抽象算法。軟件規約是軟件設計與研制工作的出發點，也是q 規約機制的屬性（1）規約應該是精確的并且有唯一和一致的解釋（2）規約機制要直觀并且易于使用（3）規約機制應該是有效的q Z 表示法（Z語言）Z 是一種形式規約語言，是在上世紀 70 年代末和 80 年代初由牛津大學程序研究小組的成員設計的。建立了 Z 方法和工作的標準。1992年底在國際 Z 用戶會議上通過了新的標準。Z 語言的特點：l Z 語言的數學基礎是集合論和一階邏輯。l Z 表示方法可以使數學結構化。l Z 語言是一個強類型系統。l Z 表示方法中可以使用自然語言。數據抽象是用數據集上的運算來表示數據，體現了表示上的抽象

3、，因此也稱為表示抽象，它是利用抽象的數據 結構，如集合、關系、函數、序列和多重集等來進行功過程抽象是指忽略任務具體完成的過程，而只精確描述該任務所要完成的功能，即描述了從輸入集到輸出值的映 射，其定義域和值域均使用數據抽象來描述。Z 表示方法支持這種兩類型的抽象，并分別稱為表示抽在表示抽象中，數據從數據結構的表示細節中抽象出來，使用集合、關系、函數、序列、包等抽象的數據類型，這 些類型構成了 Z 表示法的類型系統 。操作抽象描述了在數據抽象中所引入的數據上的抽象算法模式（schema）是 Z 表示方法的基本描述單模式分為兩類：狀態模式和操作模狀態模式定義了目標軟件系統某一部分的狀態空間以及約束

4、特性。它通過相應抽象數據類型模式分為兩類：狀態模式和操作模操作模式描述了系統某部分的行為特征，它通過描述在操作之前的該部分的狀態值與操作之l 模式的表示垂直形式：水平形式：模式名 = 模式名 | PhoneDB members:P Person telephones:Person«PhoneAddEntry DPersonDBname?: Person newnumber?:Phonel Z 表示法的文檔結構給定類型的和全局變量（常量）的定義系統的抽象狀態描述系統的初始化定義對正常條件下系統操作的定義計算已經定義的操作的前置條件描述完整的操作對規約說明的一些性質進行證明Z 語言的表示

5、抽象分為兩類：基于集合理論的表示抽象關系 A«B= P（A´B）集合冪集元組和笛卡爾積關系復合關系的閉包定義域和值域恒等關系關系的逆PhoneDBPhoneDBmembers:P Person telephones:Person«Phone函數部分函數與全函數A ®/B = R : A « B | ("a Î A; b, c Î B · (a a b) Î R Ù (a a c) Î R Þ b = c)A ® B = f : A ®/B | d

6、om f = A有限函數入射函數函數的重載 Å例：給定月份的集合Month=jan,feb,mar,apr,may,jun,jul,aug,sep,oct,nov,dec 定義兩個函數分別返回非閏年和閏年的月天數 normal,leap： Month®N1。normal = jan a 31, feb a 28, mar a 31, apr a 30, may a 31, jun a30,jul a 31, aug a 31, sep a 30,oct a 31, nov a 30, dec a 31UpdateDWeatherMap r?: Regiont?: Z Wea

7、therMapknown:P Regiontemp: RegionZdom temp=knownr?Îknown temp=tempÅr? t?temp = west a17, east a-3, south a8, north a0序列 seq X例如給定集合Month=jan,feb,mar,apr,may,jun,jul,aug,sep,oct,nov,dec<feb,apr,dec,jan>Îseq Month；序列分解函數: head,last,front,tailhead,last: seq1 X®X-Ç-：(seq X

8、)´(seq X)®(seq X) rev-：(seq X)®(seq X)-­-：seq X ´ P X® seq X序列截去和截取-after-,-for-：seq X ´N®seq X序列的減冪包（多重集）： ，bag X包的處理函數： count B iL=john,john,tom,fred,tom,tom就等價于函數bag L：john 2,fred 1,tom 3如：count L tom=3，count L mary=0問題描述：假設輸入是類型為 X 的對象的序列，輸出是一個元素為非遞減的序列。要求

9、 X 中的元素是全序的，即滿足元素是自反的、反TotordX totord:P (X«X)NondecreasingXnondecreasing: (X«X)®P(seq X)"F：X«X,s: seq X ·sÎnondecreasing FÛ"i,jÎdom s | i < j · si a sj ÎFSortX in?,out!：seq X F?：X«Xl 自由類型FreeType:=constant1|constantn|constructor1sou

10、rce1| constructormsourcemCoins:=50|10|5|1User:=custCustomer|stfStaff|mgrManagerWff:=atIdent|negWff|conjWff´Wff|l 模式User name：seq Char password：seq Charstorage_limit：NUser all：P User s"u1,u2:User u1¹u2Ùu1ÎallÙu2Îall·¹name ¹ password

11、#password<8l 模式模式名參數列表 TableX1,X2first_column：seq X1 部分second_column：seq X2部分（4）Z 語言的操作抽象 模式運算及模式擴充 給定模式 S，可以對 S 的說明部分和部分分別進行擴充。記號“S；D”表示對 S 的說明部分用說明 D 進行擴充；記號“S | P”表示對 S 的部分用進行擴充P 。（4）Z 語言的操作抽象模式擴充例如：給定模式S，令，S1 Ù S; y : N ,S 2 Ù S1 | y > 5則有相應的模式為：S1S2S（4）Z 語言的操作抽象 模式運算及模式包含模式 T 的說

12、明部分可以包含模式 S，其結果是：模式S的說明部分作為 T 說明的一部分出現，S 的部分作為模式 T 部分的一部分出現。（4）Z 語言的操作抽象模式包含TTSx,y:Nx<y（4）Z 語言的操作抽象 模式運算及模式范化令變量 x 在不同的模式中說明的類型分別為X1,X2,Xm，（4）Z 語言的操作抽象模式范化NormAABx:Z U:P Zx:1.57 U:P ZxÎU（4）Z 語言的操作抽象 模式運算及模式連接兩個模式 S 和 T 可以用命題聯結詞 Ú,Ù,Þ,Û 加以連接， 其連接的結果是：連接后的模式的說明部分是 S 和 T說明部分

13、的合并，部分是將 S 的部分與 T 的部分（4）Z 語言的操作抽象模式連接 Alpha BetaSTx,y:Z z:Rx,y:Z z:Rx,y:Zx,y:Z z:Rx<yz=y/x(x<y)Ù(z=y/x)（4）Z 語言的操作抽象模式連接ABGammax:1.57 U:P Zx:Z U,V:P ZxÎU（4）Z 語言的操作抽象 模式運算及模式變量換名記號Sy1/x1,y2/x2,yn/xn表示對模式 S 中所有自由出現的變量 x1,x2,.xn，分別用變量 y1,y2,yn 替換所得到的模（4）Z 語言的操作抽象模式變量換名例如給定模式S，并且令TÙS

14、m / xSx:N y:P NTm:Ny:P NmÎy（4）Z 語言的操作抽象 模式運算及模式變量消除記號S(x1,x2,xn)表示在模式 S 中的說明部分去掉變量x1,x2,xn，在部分用存在量詞對它進行約束。（4）Z 語言的操作抽象模式變量消除TÙS (x)例如令Sx:N y:P NT y:P N$x:N·（4）Z 語言的操作抽象 模式運算及模式的修飾為了刻畫一個狀態的轉換，必須給出轉換前和轉換后的狀態。在 Z 表示法中用模式 S表示模式 S 轉換后的狀態，S是通過將模式 S 中的所有變量后加修飾符“”而得（4）Z 語言的操作抽象模式的修飾Sx:N y:P N

15、S x:Ny:P N（4）Z 語言的操作抽象 模式運算及模式的 D 表示和 X 表示在 Z 表示法中用 DS 表示模式S 和 S的合取；用 XS 表示模式 S 的狀態沒有發生改變。DSXSS x:Ny:P NSx:N y:P Nx,x:NDS y,y:P N（4）Z 語言的操作抽象 模式運算及模式的（復合）給定模式 S 和 T，“S q T”稱為 S 與 T 的復合或。模式是通過用中間變量在前一個模式中的變化后變量與后一個模式中的變化前變量之間建立，然后去掉中（4）Z 語言的操作抽象模式的（復合）Tx?,s,s:NSx?,s,s,y!:Ns < x?s= s（4）Z 語言的操作抽象例：系

16、統的規約PhoneDBPhoneDBmembers:P Persontelephones:Person«Phonemembers:P Persontelephones:Person«Phone（4）Z 語言的操作抽象例：系統的規約 XPhoneDB DPhoneDB DPhoneDBPhonemembers = members telephones = telephones（4）Z 語言的操作抽象為分配一部未被使用的AddEntry DPersonDB name?: Personnewnumber?:Phone（4）Z 語言的操作抽象收回分配給的RemoveEntry DP

17、ersonDBname?: Person oldnumber?:Phone（4）Z 語言的操作抽象號碼FindPhonesXPersonDBname?: Person number!:P Phone（4）Z 語言的操作抽象增加成員、減少成員AddMember RemoveMember DPersonDBname?: PersonDPersonDB name?: Personname? Ï membersmembers= membersÈ name? telephones=telephones（4）Z 語言的操作抽象更改號碼可以考慮先收回已經分配給他的號碼，然后再考慮給他分配

18、一個新的號碼不同。號碼，并且新的號碼一定與舊的可以模式個模式的方式將收回號碼和分配新號碼兩，形成一個新模式，即為更改號碼的模RemoveEntryDPersonDBname?: Person oldnumber?:Phone RemoveEntry(換名)AddEntryDPersonDBname?: Person newnumber?:PhoneAddEntry(換名) RemoveAdd(整合)DPersonDB name?: Personoldnumber?,newnumber?:Phonename? Î members+ Ù name? a oldnumber?&#

19、206;telephones Ùname? a newnumber?Ïtelephones+Ùtelephones+= telephones name? a oldnumber? Ù telephones= telephones+È name? a newnumber? Ù members+= membersÙ members= members+RemoveAddDPersonDBname?: Personoldnumber?,newnumber?:Phonename? Î membersname? a oldnu

20、mber?Îtelephonesname? a newnumber?Ï telephones name? a oldnumber?telephones= telephones name? a oldnumber?È name? a newnumber?members= members（4）Z 語言的操作抽象例外處理在Z表示法中，對每一個操作都附帶有輸出操作結果的信息，如果成功則輸出成功的信息；如果失敗則輸出錯誤原 因信息。輸出信息在 Z 表示法中通過自由類型來定義。Report:=Ok|Not a member|Entry already exist| Unkno

21、wn name|Unknown number| Unknown entry|Already a member|Not a memberSuccess rep!:Reportrep!=Ok例外處理NotMemberXPersonDB name?: Personrep!:Report EntryAlreadyExistsXPersonDB name?: Personnewnumber?:Phone rep!:Reportname? Ï members rep!=Not a membername? a newnumber?Î telephones rep!=Entry alrea

22、dy existsDoAddEntry Ù ( AddEntry Ù Success) Ú NotMember Ú EntryAlreadyExists（4）Z 語言的操作抽象 通用式函數顯式的函數定義明確地描述了如何獲得輸出參數。例如：對輸入參數求平方的函數 SqrSqr : N®N"n : N · Sqr(n) = n*n（4）Z 語言的操作抽象 通用式函數隱式函數定義只是之間的關系。了輸入參數與函數的輸出參數max : F1 N®N例如，函數max的定義"nset : F1 N; n : N

23、83; max(nset) = n ÛnÎnset Ù "i : N · iÎnset Þ i£n 通用式函數函數也可以遞歸定義。例如，定義對整形列表中的所有數進行求和并返回結果 的函數sum_listList:=nil | cons Z´List Sum_list : List ® Z"n : Z; L : List · Sum_list(nil) = 0 ÙSum_list(cons(n,L)=n+Sum_list(L)（4）Z 語言的操作抽象通用式函數的一般定

24、義X1,X2,XnDPTlength : seq T ® N"inseq : seq T ·inseq = <> Þ length(inseq) = 0 Ùinseq ¹ <> Þ length(inseq) = 1+length(tail inseq)（5）模式推理 教室的規約ÙClass1d: P PersonDClass1Class1ÙClass1XClass1ÙDClass1 | d=d#d £ MaxÙClass1 | d=Init1（5）模

25、式推理 教室的規約Enter1DClass1 p? : PersonLeave1DClass1 p? : Person#d < Max p? Ï dd= dÈp?p? Î dd= dp?（5）模式推理 模式和教室某個時刻可能沒有人$ d: P Person | #d £ Max · d= (1)教室里在某個時刻均為女性。用female:P Person表示女性的集合"d: P Person | #d £ Max · d Í female(2)（5）模式推理 模式和計算教室里當前的實有人數ld: P

26、Person | #d £ Max · #d(3)$Class1 · d="Class1 · d Í femalelClass1 · #d（5）模式推理 模式和模式名可以出現在出現的任何位置$d: P Person | #d£ Max · Init1$d: P Person | #d£ Max · d= $Class1 · Init1（5）模式推理 初始化證明初始化證明是證明每個規約都有初始化狀態存在。$d: P Person | #d £ Max · d

27、= （5）模式推理 規約理論的構造例如，教室系統的一個性質是：當開，教室的狀態沒有發生變化。進入教室后又離（Enter1 q Leave1）Û (XClass1 | p?Ï d)展開上式的右端，得到： DClass1 | d=dÙ p?Ïd#d £ Max Ù #d£ Max Ù d=d Ù p?Ïd即（5）模式推理 規約理論的構造（Enter1 q Leave1）Û (XClass1 | p?Ï d)Alpha ÙEnter1DClass1 p? : Person

28、Enter1qLeave1Leave1DClass1 p? : Person#d < Max p? Ï dd= dÈp?p? Î dd= dp?（5）模式推理 規約理論的構造Alpha d,d: P Person p? : Person $d+: Person ·#d £ Max Ù # d < Max Ù p?Ïd Ùd+=dÈp? Ù # d+ £ Max Ù p?Îd+ Ù d=d+p?（5）模式推理 前置條件Ù在Z中

29、，PreSpre S。其中，S 是模式名因此 PreS 是模式 pre S 的另一種表示形#d £ Max #d < Max p? Ï d$d: Person · （#d £ Max Ù d= dÈp?） 前置條件PreEnter1 d : P PersonP? : PersonPreEnter1 d : P PersonP? : Person$d: Person ·（#d £ Max#d £ Max#d < Max p? Ï dd= dÈp?） 前置條件PreEnter1

30、 d : P PersonP? : Person#d < Max p? Ï d（5）模式推理 規約的完整性規約的完整性是指：對任一操作，要分別考慮滿足前置條件和不滿足前置條件兩種情形，特別是對不滿足前置條件的情形必須要 有定義。（5）模式推理 規約的完整性AlreadyPresentFull1Full1XClass1 p?: Personrep! : Report#d ³ Maxrep！= “Class Full”4、時態邏輯時態邏輯又稱為時序邏輯，是一種特殊的模態邏輯，適合于并發軟件系統的規約和驗證。（1）模態邏輯模態邏輯（Modal Logic）是經典命題邏輯和一

31、階邏輯的擴展形基于命題邏輯的擴展稱為模態命題邏輯，基于一階邏輯的擴展稱為模態一階邏輯。模態邏輯涉及到必然性和可能性概念。（1）模態邏輯模態詞具有聯接詞的類似功能，是構成模態邏輯中復合命題的基本運算子。常用的基本模態詞包括：必然（ ）和可能（à）。（1）模態邏輯模態邏輯公式模態命題邏輯公式，簡稱為模態邏輯公式，定義如下： 原子命題（命題常量或者命題變元）是模態邏輯公式； 如果A是模態邏輯公式，那么（àA）和（ A）是模態邏輯公式； 如果A、B是模態邏輯公式，那么（A）、（AÚB）、（AÙB）、（A®B）、（A«B）是模態邏輯公式； 當且

32、僅當有限次使用上述規則所組成的符號串是模態邏輯公（1）模態邏輯反映模態詞性質的一些模態邏輯公式：u A®Au A®àA必然A真則A真；A真則可能A 真；u A®àA 必然A真則可能A真；u A «àu àA «u àA Ú àAA必然A當且僅當不可能非A；可能A當且僅當并非必然非A；A可能A或者可能A反映模態詞性質的一些模態邏輯公式： (AÙA）既有必然A，又有必然A； (A ÚA） 必然有A成立或者A成立；à(AÙA)不可能A與A同時

33、成立； (A Ù B) « A Ù B 必然有A并且B等價于必然A并且必然B； A Ú B® (AÚ B)有A真或者B真；à(A ÚB) « à AÚ àB或者可能B為真；à(A ÙB) ® à AÙ àB必然A或者必然B有一為真，那么必然可能A或者B為真當且僅當可能A為真如果可能有A并且B為真，那么可能A為真并且可能B為真。（1）模態邏輯模態一階邏輯公式模態一階邏輯公式，簡稱為模態一階邏輯公式，定義如下： 原子公式

34、是模態一階邏輯公式； 如果A、B是模態一階邏輯公式，那么（àA）、（ A）、（A）、（ÚA B）、（ÙA B）、（®AB）、（«AB）也是模態一階邏輯公式； 如果A是模態一階邏輯公式，x是A中出現的變量（ 那么$x·A、"x·A也是模態一階邏輯公式；變元）， 當且僅當有限次使用上述規則所組成的符號串是模態一階邏輯公（1） 模態邏輯模態一階邏輯公式u "x· A« ("x·A)u $x·à A«à ($x·A)u &#

35、224;("x·A) ® ("x·A)u $x· A® ($x·A)u A«àu àA«A A（1）模態邏輯Kripke結構三元組M=（W,R,L）稱為模態邏輯的一個模型，或者Kripke結構（模型），其中W是可能世界的非空集合； RÍW´W是可能世界W上的二元關系；L：W®P(A)（A 為原子公式集合）是標記函數，它是對可能世界的真值指派，即對每個模態邏輯公式，指明它在每個可能世界中取真值還是假值。（1）模態邏輯標準模型模態邏輯的標準模型是滿足

36、下述條件的三元組M=（W,R,L）：對于p,qÎA和s,tÎW有： L(p,s)=1Ú0L(p,s)=L(p,s)L(pÚq,s)= L(p,s) Ú L(q,s)L(pÙq,s)= L(p,s) Ù L(q,s)L( p,s)= ("t)(sRt®L(p,t)=1L(àp,s)= ($t)(sRtÙL(p,t)=1（1）模態邏輯分支或線性任一當前時刻存在唯一的可能未來時刻，時間的推進 是線性的，稱之為線性時間；時間具有分支或者樹結構的性質：任一當前時刻可能分叉為多種可能未來時刻，稱為

37、分支時間。采用了分支（或線性）時間結構的時態邏輯，稱為分支（或線性）時態邏輯。（1）模態邏輯離散或連續當某計算或活動需要描述成隨時間連續變化時，需要采用一個稠密時間模型，即時間對應于實數或實數域上的一個子集；當系統行為出現在一序列特定的時刻，就可以采用一個離散的時間模型，即時間對應于非負整數或非負整數的一個子集。若系統的時間特征行為出現在一序列時間區間上，那么就需要使用一些連續時間區間，稱為區間時間模型。（1）模態邏輯常用時態邏輯包括：命題線性時態邏輯（PLTL） 一階線性時態邏輯（FOLTL）命題分支時態邏輯或計算樹邏輯（CTL、CTL*）等。（2）線性時態邏輯命題線性時態邏輯（PLTL）是

38、在命題邏輯中增加了如下模態詞（時態算子）：ÿ always算子， A表示 A 總是為真或者 A 永遠為真；à sometimes算子，àA表示 A 最終為真或者 A 有時為真onext算子，oA表示 A 在下一時刻為真；Until算子，AB 表示 A 一直為真直到 B 為真。（2）線性時態邏輯命題線性時態邏輯（PLTL）公式 原子命題（命題常量或者命題變元）是 PLTL 公式； 如果 A 是 PLTL 公式，那么（àA）和（ A）（oA）是 PLTL公式； 如果 A、B 是 PLTL公式，那么（A）、（AÚB）、（AÙB）、（A

39、74;B）、（A«B）、（AB）是 PLTL 公式； 當且僅當有限次使用上述規則所組成的符號串是 PLTL公A® B (A®àB）如果當前狀態 A 為真，則會出現 B 永為真的狀態；從當前狀態開始，使 A 為真的狀態后終將有使 B 為真的狀態；從某一狀態開始 A 永遠為真；à Aà (AÙoA）終將有一狀態，在該狀態中 A 為真并且下一狀態中A假；對今后任何狀態而言，其后都將有狀態使 A為真；對今后狀態而言，A 真將導致 B 從此永遠真；為 àA (A® B) A Ú(AB)或者 A 從此永遠真

40、，或者 A 從此一直真直到使 B 真的狀態出現；如果 A 從此永遠真，那么下一狀態中，A 仍然將永遠ÿ A® o A為真；rJ（v1,v2,v3）= (v3­®o(v1 Ù v2®v2­)Ù (v3­®o(v1 Ù v2®v2¯)（2）線性時態邏輯f1.1基本元素的規約f2.1電路行為規約yT2I1I2z1電路性能的推演zxT1(a)v3v2v2v1v1(b)(c)（2）線性時態邏輯時間點012345678輸入信號時鐘信號負載信號 z 點電位y 點電位xflxflz

41、.flz yfflflz yf flz y.lz ylz y.zy（2）線性時態邏輯一階線性時態邏輯（FOLTL）是一階邏輯的擴展，類似于 PLTL，FOLTL 是在一階邏輯中增加了模態詞 always（ ）、sometimes（à）、next（o）、Until（）。（2）線性時態邏輯一階線性時態邏輯公式，簡稱為FOLTL公式，定義如下： 原子公式是 FOLTL 公式； 如果 A、B 是 FOLTL 公式，那么（àA）、（ A）、（oA）、（AB）、（A）、（AÚB）、（AÙB）、（A®B）、（A«B）也是FOLTL公式； 如果A是F

42、OLTL公式，x是A中出現的變量（ 元），那么$x·A、"x·A也是FOLTL公式； 當且僅當有限次使用上述規則所組成的符號串是FOLTL公式變（2）線性時態邏輯隊列及其操作隊列的狀態改變有兩個操作：一個元素到隊尾（PUT）；從隊列的頭部移除一個元素（GET）。（2）線性時態邏輯假設：cur_queue 描述隊列的當前狀態；putval和getval分別表示 PUT 操作和 GET 操作的參數； GET 操作的前置條件為：getval¹nil；后置條件 getval= nil；PUT 操作的前置條件為 putval= nil；后置條件為 putval&#

43、185;nil；enter(PUT)、enter(GET)、exit(GET)和exit(PUT)分別表示相應操作的開始和結束。隊列及其操作l 活性PUT操作的活性就是要求其能夠終止；GET操作的活性是指只有在隊列中取出一個值后才能終止.enter(PUT) Ù（length(cur_queue)<max）®à(exit(PUT)Ù(cur_queue=cur_queue*putval) enter(PUT) Ù（length(cur_queue)=max）®à(exit(PUT)Ù(cur_queue=cu

44、r_queue)隊列及其操作l 活性enter(GET) Ùempty(cur_queue)®à(exit(GET)Ù(cur_queue=getval*cur_queue)enter(GET) Ùempty(cur_queue)®(enter(GET)exit(PUT)empty(cur_queue)® àenter(PUT)隊列及其操作l 安全性假設(enter(PUT) Ùputval¹nil)在cur_queue下成立 ( enter(PUT) Ù putval¹ni

45、l) ®(lehgth(cur_queue)=max)Ù(cur_queue=cur_queue)Ú(length(cur_queue)<max)Ù(cur_queue=cur_queue*putval)隊列及其操作l 安全性假設(enter(GET) Ùgetval=nil)在cur_queue下成立 ( enter(GET) Ùgetval=nil) ®(empty(cur_queue) Ùempty(cur_queue) Ú(empty(cur_queue)Ù( cur_queue=

46、getval*cur_queue) 操作規劃問題P1P3P2P3P2P1定義如下：u 操作的約束條件move(X，p) 將盤X移動到柱子p；on(X,Y) 盤X在盤Y上； smaller(X,Y) 盤X比盤Y??； top(X,p) 盤X在柱子p的最上面；free(X) 盤X可以被移動u 規約假設u 活動的前置后置條件ABCABC（3）計算樹邏輯計算樹邏輯（CTL）是一種離散、分支時間、命題時態 邏輯。在 CTL 中，除了具有時態算子 always（ ）、sometimes（à）、next（o）、Until（）外，增加了路徑量詞：所有未來路徑（A）、至少某一路徑（E）。（3）計算樹邏輯

47、計算樹邏輯公式，簡稱 CTL 公式，定義如下： 原子命題是 CTL 公式； 如果 a、b 是 CTL 公式，那么 (a( a « b) 是 CTL 公式；)、a( Ú b)、a( Ù b)、a(® b)、 如果a、b 是 CTL 公式， 那么 (Ao a)、 (Eo a)、 (Aà a)、(Eàa) 、 (A a) 、 (E a) 、 (A(ab) 、(E(ab) 是CTL公式； 當且僅當有限次使用上述規則所組成的符號串是CTL公（3）計算樹邏輯基于Kripke結構，可以CTL 的語義。當且僅當 pÎL(s)M,s|=pa&

48、#217;bAoa當且僅當 aÎL(s)和 bÎL(s)M,s|=當且僅當對于所有滿足<s,s1>ÎR(s)的M,s1 |= a當且僅當對于滿足<s,s1>ÎR(s)的一些M,s|=s1 滿足M,s|=Eoas1 滿足M,s1 |=a M,s |= A a當且僅當對于所有s1=s的路徑<s1,s2><s2,s3>,這些路徑上的si滿足 M,si |=a M,s |= E a當且僅當存在s1=s的路徑<s1,s2><s2,s3>,該路徑上的si滿足 M,si |=a M,s |= Aàa 當且僅當對于所有s1=s的路徑<s1,s2><s2,s3>,這些路徑上均存在一些 si 滿足 M,si |=a M,s |=Eàa當且僅當存在 s1=s 的路徑<s1,s2><s2,s3>,該路徑上有些 si 滿足 M,si |=aA(ab）當且僅當所有 s1=s 的路徑 <s1,s2><s2,s3>, M,s滿足 a|=bE(ab)的路徑<