守卫命令语言

Guard命令语言（GCL）是Edsger Dijkstra在EWD472中为谓词转换语义定义的一种编程语言。它以一种紧凑的方式结合了编程概念。它使开发一个程序和它的证明更容易，由证明来引导；此外，程序的一部分实际上可以被计算。

GCL的一个重要属性是非决定性。例如，在一个if语句中，有几个选项可能为真，而选择哪个选项是在运行时进行的，也就是在if语句的执行过程中。这使程序员不必做出不必要的选择，是对正式程序开发的一种帮助。

GCL包括多个赋值语句。例如，语句x, y:= y, x的执行是先对右边的值进行评估，然后将其存储在左边的变量中。因此，这条语句交换了x和y的值。

以下书籍讨论了使用GCL的程序开发：

• Dijkstra, Edsger W. (1976).A Discipline of Programming.Prentice Hall.ISBN 978-0132158718.
• Gries, D. (1981).The Science of Programming.Monographs in Computer Science（英语、西班牙语、日语、中文、意大利语和俄语）。纽约.Springer Verlag.
• Dijkstra, Edsger W.; Feijen, Wim H.J. (1988).A Method of Programming.Boston, MA:Addison-Wesley Longman Publishing Co.p.200.ISBN 978-0-201-17536-3。
• Kaldewaij, Anne (1990).Programming: the derivation of algorithms.Prentice-Hall, Inc.ISBN 0132041081.
• Cohen, Edward (1990).David Gries (ed).Programming in the 1990s.程序计算的介绍。Texts and Monographs in Computer Science.Springer Verlag.ISBN 978-1-4613-9706-9.

守护命令是守护命令语言的最重要元素。在守护命令中，正如其名称所暗示的那样，命令被保护起来。守护是一个命题，在语句执行前必须为真。在该语句的执行开始时，人们可以假设该守护是真的。或者，如果该保护是假的，该语句将不会被执行。使用受保护的命令可以更容易地证明程序符合规范的要求。语句通常是另一个受保护的命令。

skip和abort是守护命令语言中的重要语句。abort是未定义的命令：做任何事。它甚至不需要终止。它用于描述程序在制定证明时，在这种情况下，证明通常会失败。 skip是空指令：什么都不做。它用于程序本身，当语法需要语句但状态不应改变时。

给变量赋值。

语句之间用分号（;）分隔

选择（通常称为条件或if语句）是一个保护命令的列表，从中选择一个执行。如果有一个以上的保护为真，那么一个被保护的语句就会被非决定性地选择执行。如果没有防护措施为真，则结果是未定义的。因为至少有一个防护措施必须为真，所以空语句往往需要被跳过。语句if fi没有守护的命令，所以永远不会有一个真正的守护。因此，if fi等同于abort。

if G0 → S0 □ G1 → S1…Gn → Snfi

当执行选择时，所有的守卫被评估。如果没有一个守卫评估为真，那么选择的执行就会被中止，否则就会非决定性地选择一个值为真的守卫并执行相应的语句。

的伪代码。

如果a < b，那么将c设置为Trueelse，将c设置为False

在有防护的命令语言中。

if a < b → c := true □ a ≥ b → c := falsefi

的伪代码。

如果错误为真，将x设为0

在有防护的命令语言中。

if error → x := 0 □ ¬ {displaystyleneg } error → skipfi

如果省略了第二个卫兵，并且error为False，那么结果就是abort。

如果a≥b→max := a □ b ≥ a→max := bfi

如果a = b，如果选择a或b作为xxx值的新值，其结果是一样的。