守卫命令语言

**守衛命令語言**（**GCL**：Guarded Command Language）是艾茲赫爾・戴克斯特拉為謂詞變換語義定義的一門語言。它以精簡方式組合了編程概念，它們處在以某種實際的程式語言書寫程序之前。它的簡單性使得採用霍爾邏輯證明程序的正確性更加容易。

## 守衛命令

守衛（guarded）命令是守衛命令語言的最重要元素。在守衛命令中，同名字所說一樣，這個命令是被守衛著的。這個守衛是先決條件，在這個語言被執行之前，它必須為真。在這個語句執行開始時，可以假定這個守衛為真。還有，如果這個守衛為假，這個語句將不被執行。使用守衛命令使得證明程序滿足規定更加容易。這個語句也經常是另一個守衛命令。

### 語法

一個守衛命令是形如 G → S 的一個語句，這裡的

* G 是先決條件，叫做守衛（guard）；
* S 是語句。

如果 G 為真，守衛命令可以簡單的寫為 S。

### 語義

當在計算中遇到 G 的時刻，求值它。

* 如果 G 為真，執行 S；
* 如果 G 為假，查看上下文來決定做什麼（在任何情況下，都不執行 S）。

## 躍過和中止

在守衛命令語言中，躍過（skip）和中止（abort）是非常簡單也是非常重要的語句。中止是未定義指令：做任何事情。中止語句甚至不需要終止（terminate）。在公式化一個證明的時候，它被用來描述一個程序，在這種情況下證明通常失敗。躍過是空指令：什麼事情都不做。它被用在程序自身中，當語法要求一個語句的時候，而編程者卻不想要機器改變狀態。

### 語法

```
**skip**
```

```
**abort**
```

### 語義

* Skip: 什麼事情都不做
* Abort: 做任何事情

## 賦值

將值指派給變量。

### 語法

```
v := E
```

或

```
v0, v1, ..., vn := E0, E1, ..., En
```

這裡的

* v 是程序變量，
* E 是數據類型同於其對應變量的表達式。

## 串接

語句由分號（;）來分割。

## 選擇：if

選擇（經常叫做「條件語句」或「if 語句」）是守衛命令的列表，從中選取一個來執行。如果多於一個守衛為真，非確定性的選取一個語句來執行。如果沒有守衛為真，結果是未定義的。因為至少一個守衛必須為真，空語句 "skip" 經常是需要的。

### 語法

```
**if** G0 → S0
|  G1 → S1
...
|  Gn → Sn
**fi**
```

### 語義

在執行一個選擇的時候求值所有的守衛。如果沒有守衛被求值為真，則選擇的執行會 abort，否則非確定性的選擇其值為真的守衛之一，並執行對應的語句。

### 例子

#### 簡單

用偽代碼：

　
: if a < b then c := True

　
: else c := False

用守衛命令語言：

```
**if** a < b → c := true
|  a ≥ b → c := false
**fi**
```

#### 使用 skip

用偽代碼：

　
: if error = True then x := 0

用守衛命令語言：

```
**if** error = true → x := 0
|  error = false → **skip**
**fi**
```

如果第二個守衛被省略，並且 error = False，結果是 abort。

#### 多個守衛為真

```
**if** a ≥ b → max := a
|  b ≥ a → max := b
**fi**
```

如果 a = b，要麼 a 要麼 b 被選取為極大值的新值，具有相同的結果。但是，在實現這個例子的時候，可能會發現一個比另一個更容易或更快。因為對於編程者這裡沒有區別，可以隨意實現任何一種方式。

## 重複：do

重複會反覆的執行守衛命令知道沒有守衛為真。通常，這裡只有一個守衛。

### 語法

```
**do** G0 → S0
|  G1 → S1
...
|  Gn → Sn
**od**
```

### 語義

當執行重複的時候所有守衛都求值。如果所有守衛都求值為假，則執行 skip。否則非確定性的選取其值為真的守衛之一，並執行對應的語句，此後再次執行重複。

### 例子

#### 歐幾里德算法

```
a, b := A, B;
**do** a < b → b := b - a
|  b < a → a := a - b
**od**
```

這個重複在 a = b 時候結束，在這種情況下 a 和 b 持有 A 和 B 的最大公約數。

戴克斯特拉在這個算法中見到了兩個無限循環 `a := a - b` 和 `b := b - a` 同步的一種方式，在這種方式下 `a≥0` 和 `b≥0` 保持為真。

#### 擴展歐幾里德算法

```
a, b, x, y, u, v := A, B, 1, 0, 0, 1;
**do** b ≠ 0 →
|  q, r := a **div** b, a **mod** b;
|  a, b, x, y, u, v := b, r, u, v, x - q*u, y - q*v
**od**
```

這個重複在 b = 0 的時候結束，在這種情況下變量持有對貝祖等式：xA + yB = gcd (A,B) 的解。

#### 非確定性排序

```
**do** a>b → a, b := b, a
|  b>c → b, c := c, b
|  c>d → c, d := d, c
**od**
```

這個程序在其中一個元素大於它的後續者的時候持續的置換元素。這個非確定性冒泡排序不比它的確定性版本更加有效率， 但是易於證明：只要元素仍未有序它就不會停止並且它每步至少排序 2 個元素。

#### Arg max

```
x, y = 1, 1 
**do** x≠n →
|  **if** f(x) ≤ f(y) → x := x+1
|  |  f(x) ≥ f(y) → y := x; x := x+1
|  **fi**
**od**
```

這個算法找到值 1 ≤ _y_ ≤ _n_，對於它給定整數函數是最大的。不只是這個計算而且最終狀態都不是必然唯一確定的。

## 應用

### 構造正確程序

將觀察的守衛命令的同餘關係推廣成格導致了精製演算。這已經機制化於形式化方法如 B 方法中，它允許從它們的規定形式化的導出程序。

### 異步電路

守衛命令適合於准延遲不敏感電路設計，因為重複允許不同命令選擇的任意相對延遲。在這種應用之，在電路中驅動一個節點 y 的邏輯閘構成自兩個守衛命令如下：

```
PullDownGuard → y := 0
PullUpGuard → y := 1
```

這裡的 PullDownGuard 和 PullUpGuard 是邏輯閘輸入的函數，它描述了什麼時候這個邏輯閘分別將輸出拉下或拉上。不同於經典的電路評估模型，一組守衛命令的重複（對應於一個異步電路）可以準確的描述這個電路的所有可能的動態行為。

### 模型檢查

守衛命令可以用在 Promela 程式語言中，它被用於 SPIN 模型檢查器。SPIN 驗證並發軟體應用的正確操作。

### 其他

Perl 模塊 Commands::Guarded 實現了戴克斯特拉的守衛命令的一個確定性的校正變體。

## 引用

## 參見

* 衛語句