Program Verification 05 - Guarded Command
# 前置知识
在阅读本文档前,请确保你已了解最弱前置条件的相关概念,详见 Program Verification 知识板块中的 04 - Weakest Precondition 文档。
# 基本概念
卫式命令 (guarded command) 是一种描述程序 不确定性 (nondeterministic) 的形式化规则,由 Dijkstra 在 1975 年提出。
卫式命令的最基本形式如下:
<guarded command> ::= <guard> -> <statement list>
<guard> ::= <boolean expression>
<statement list> ::= <statement> {; <statement> ...}
其中 guard
是一个布尔表达式,仅在 guard
为真时程序段 statement list
才会被执行。可以看作是 statement list
受到 guard
的保护,这也是卫式命令之名 guarded 的由来。
卫式命令的精髓在于 guarded command set ,以及由此构造的条件分支和循环构造:
<guarded command set> ::= <guarded command> {[] <guarded command> ...}
<alternative construct> ::= if <guarded command set> fi
<repetitive construct> ::= do <guarded command set> od
guarded command set 是 guarded command 的无序列表,由 []
分隔,其在文本中的出现顺序和卫式命令的语义无关。
卫式命令的语义规则的非形式化描述如下:
对于 if-fi
语句,考虑 guarded command set 中的每个 guarded command :
若仅有一个 ,则执行 ;
若不止一个 ,则 不确定地 选择并执行其中一个 ;
若所有 ,则抛出错误。
对于 do-od
语句,考虑 guarded command set 中的每个 guarded command :
若仅有一个 ,则执行 ,随后重新判定每个 的真假;
若不止一个 ,则 不确定地 选择并执行其中一个 ,随后重新判定每个 的真假;
若所有 ,则退出循环。
若允许 guarded command set 为空,则 if fi
等价于 abort
,而 do od
等价于 skip
。
至此不难发现,卫式命令的语法虽然简单,却已经构成了一个基本完整的、支持运行时不确定性的形式化编程语言。下面是一些由卫式命令表示的程序示例。
求 和 的最大值:
if (x >= y) -> (m := x)
[] (x <= y) -> (m := y)
fi
对 进行排序:
do (q1 > q2) -> (q1, q2 := q2, q1)
[] (q2 > q3) -> (q2, q3 := q3, q2)
[] (q3 > q4) -> (q3, q3 := q4, q3)
od
对于给定的 ,和定义域为 的确定性函数 ,求出 满足 且 。
k := 0;
i := 1;
do (j != n) -> (
if (f(i) <= f(k)) -> (j := j + 1)
[] (f(i) >= f(k)) -> (k := j; j := j + 1)
fi
) od
k := 0;
i := 1;
do (j != n) -> (
if (f(i) >= f(k)) -> (k := j) fi
j := j + 1;
) od
# 形式化语义
# 最弱前置条件
Dijkstra 使用最弱前置条件来描述卫式命令的形式化语义。
设 表示 ,对于任意的后置条件 ,其最弱前置条件为:
其中式一的含义是当所有 时 if-fi
语句不会导致 abort
。若允许 guarded command set 为空,则可抛弃式一。
(unfinished)
# 操作语义
TBD.
# 参考资料
Edsger W. Dijkstra - A Discipline of Programming (opens new window)
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01