守護命令語言（GCL）是EdsgerDijkstra在EWD472中為謂詞變換器語義定義的一種編程語言。它以一種緊湊的方式結合了編程概念。它使開發一個程序和它的證明攜手并進變得更加容易，證明的思路處于xxx地位；此外，一個程序的部分內容實際上可以被計算。GCL的一個重要屬性是非決定性。例如，在if語句中，有幾個選項可能是真的，而選擇哪個選項是在運行時完成的，即在執行if語句時。這使程序員不必做出不必要的選擇，是對程序正式開發的一種幫助。GCL包括多重賦值語句。例如，語句x,y:=y,x的執行是通過首先評估右邊的值，然后將其存儲在左邊的變量中。因此，這個語句交換了x和y的值。以下書籍討論了使用GCL開發程序的問題。SpringerVerlag.ISBN978-1-4613-9706-9.守護命令守護命令是守護命令語言中最重要的元素。在一個受保護的命令中，正如其名稱所說，命令是受保護的。守護是一個命題，在語句執行前必須為真。在該語句的執行開始時，人們可以假設該防護是真的。另外，如果守護是假的，該語句將不會被執行。使用保護性命令可以更容易地證明程序符合規范。語句通常是另一個受保護的命令。

受保護的命令是一個形式為G→S的語句，其中G是一個命題，稱為守護S是一個語句語義在計算中遇到G的時候，對它進行評估。如果G是真的，就執行S如果G是假的，就看上下文來決定做什么（在任何情況下，都不要執行S）skip和abortskip和abort是守護命令語言中的重要語句。abort是未定義指令：做任何事情。它甚至不需要終止。它用于在制定證明時描述程序，在這種情況下，證明通常會失敗。skip是空指令：不做任何事情。它用于程序本身，當語法需要一個語句但狀態不應改變時。

skip中止

skip:donothingabort:doanything賦值給變量賦值。語法v:=Ev是程序變量E是與其對應的變量具有相同數據類型的表達式Catenation語句之間用一個分號（;）分隔選擇：如果選擇（通常稱為條件語句或if語句）是一個受保護的命令列表，從中選擇一個來執行。如果有一個以上的保護措施為真，則非確定地選擇保護措施為真的一個語句來執行。如果沒有防護措施為真，則結果是未定義的。因為至少有一個守護必須為真，所以經常需要空語句跳過。語句iffi沒有被守護的命令，所以永遠不會有一個真正的守護。因此，iffi等同于abort。語法ifG0→S0□G1→S1...□Gn→Snfi

在執行一個選擇時，所有的守衛都被評估。如果沒有一個防護措施被評估為真，那么選擇的執行就會中止，否則就會非決定性地選擇其中一個防護措施的值為真，并執行相應的語句。簡單的例子在偽代碼中。如果a<b，則將c設為True，否則將c設為False。在有防護的命令語言中。如果a=b，則選擇a或b作為xxx值的新值，其結果相同。然而，執行過程中可能會發現，其中一個比另一個更容易或更快。由于對程序員來說沒有區別，任何實現都可以。