text: 守衛命令語言是艾茲赫爾·戴克斯特拉為定義的一門語言。它以精簡方式組合了程式設計概念，它們處在以某種實際的程式語言書寫程式之前。它的簡單性使得采用霍爾邏輯證明程式的正確性更加容易。守衛命令.守衛命令是守衛命令語言的最重要元素。在守衛命令中，同名字所說一樣，這個命令是被守衛著的。這個守衛是先決條件，在這個語言被之前，它必須為真。在這個語句執行開始時，可以假定這個守衛為真。還有，如果這個守衛為假，這個語句將不被執行。使用守衛命令使得證明程式滿足更加容易。這個語句也經常是另一個守衛命令。語法.一個守衛命令是形如G → S的一個語句，這裡的如果G為真，守衛命令可以簡單的寫為S。語義.當在計算中遇到G的時刻，求值它。躍過和中止.在守衛命令語言中，躍過。在公式化一個證明的時候，它被用來描述一個程式，在這種情況下證明通常失敗。躍過是空指令：什麼事情都不做。它被用在程式自身中，當語法要求一個語句的時候，而程式設計者卻不想要機器改變。語法.skipabort賦值.將值指派給變數。語法.v := E或v0, v1, ..., vn := E0, E1, ..., En這裡的串接.語句由分號來分割。選擇：if.選擇是守衛命令的列表，從中選取一個來執行。如果多於一個守衛為真，非確定性的選取一個語句來執行。如果沒有守衛為真，結果是未定義的。因為至少一個守衛必須為真，空語句"skip"經常是需要的。語法.if G0 → S0| G1 → S1| Gn → Snfi語義.在執行一個選擇的時候求值所有的守衛。如果沒有守衛被求值為真，則選擇的執行會abort，否則非確定性的選擇其值為真的守衛之一，並執行對應的語句。例子.簡單.用虛擬碼：if a d → c, d := d, cod這個程式在其中一個元素大於它的後續者的時候持續的置換元素。這個非確定性氣泡排序不比它的確定性版本更加有效率， 但是易於證明：只要元素仍未有序它就不會停止並且它每步至少排序2個元素。Arg max.x, y = 1, 1do x≠n →| if f(x) ≤ f(y) → x := x+1| | f(x) ≥ f(y) → y := x; x := x+1| fiod這個演算法找到值1 ≤ "y" ≤ "n"，對於它給定整數函式是最大的。不只是這個計算而且最終狀態都不是必然唯一確定的。應用.構造正確程式.將觀察的守衛命令的同餘關係推廣成格導致了。這已經機制化於形式化方法如中，它允許從它們的規定形式化的匯出程式。非同步電路.守衛命令適合於設計，因為重複允許不同命令選擇的任意相對延遲。在這種應用之，在電路中驅動一個節點y的邏輯閘構成自兩個守衛命令如下：PullDownGuard → y := 0PullUpGuard → y := 1這裡的PullDownGuard和PullUpGuard是邏輯閘輸入的函式，它描述了什麼時候這個邏輯閘分別將輸出拉下或拉上。不同於經典的電路評估模型，一組守衛命令的重複可以準確的描述這個電路的所有可能的動態行為。模型檢查.守衛命令可以用在程式語言中，它被用於。SPIN驗證併發軟體應用的正確操作。其他.Perl模組Commands::Guarded實現了戴克斯特拉的守衛命令的一個確定性的校正變體。
metadata: erhwenkuo/wikipedia-zhtw
metadata: 守衛命令語言
metadata: https://zh.wikipedia.org/wiki?curid=7385158