守护命令语言

守护命令语言（GCL）是EdsgerDijkstra在EWD472中为谓词变换器语义定义的一种编程语言。

它以一种紧凑的方式结合了编程概念。它使开发一个程序和它的证明携手并进变得更加容易，证明的思路处于领 先地位；此外，一个程序的部分内容实际上可以被计算。

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。

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

简单的例子在伪代码中。如果a<b，则将c设为True，否则将c设为False。在有防护的命令语言中。

如果a=b，则选择a或b作为最 大值的新值，其结果相同。然而，执行过程中可能会发现，其中一个比另一个更容易或更快。由于对程序员来说没有区别，任何实现都可以。