• 例:设程序P由三条语句组成:
• t:=x; x:=y; y:=t; • 对任意的X=(x,y,t), 程序P的执行结果Y=(y,x,x) • 因此,程序函数是{(x,y,t),(y,x,x)}
• 本质: 计算输入和输出的关系
15
Chap4 结构化程序设计及正确性证明
二、结构化定理
2. 七种基本程序的程序函数 [f] = {(x,y)| y=f(x)} [f;g] = {(x,y)| y = g ·f(x)} [if-then] = {(x,y)|p(x)y=f(x)|¬p(x)y=x} [if-then-else] = {(x,y)| p(x)y=f(x)|¬p(x)y=g(x)}
| p(x) q•f(x) r • h • f(x)y=g•h • f(x)
| p(x) q•f(x) r • h • f(x)y=h • f(x)
| p(x) …
21
|…
Chap4 结构化程序设计及正确性证明
二、结构化定理
3. 程序函数的计算
3)循环程序的程序函数
g2
g5
g1
g3
p f
8
Chap4 结构化程序设计及正确性证明
正规程序
• 4. 正规程序
• 定义:满足以下两个条件的流程图程序称为正规程 序。条件:
• 具有一条入口线和一条出口线,且 • 对每个节点,都有一条从入口线到出口线的通路通过该
节点。
• 例:下面两个流程图程序不是正规程序
f
p
g
f p
9
Chap4 结构化程序设计及正确性证明
p1
p2
p3
执行树: 1 g1
2 g3
g4
g2