结构化定理--证明
最后，利用已经得到的一些gi（I=1,2,3,…,n），按 下图形式构造一个while-do循环。这个循环体是 一个对L从1到n进行测试的嵌套的IF-THENELSE程序（最内层的I表示恒等函数）：
F=
L:=1
g1
L=1?
g2
L>0
L=2?
•••
•••
gn-1
L=n-1?
gn
L=n?
[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)}
Chap4 结构化程序设计及正确性证明
二、结构化定理
2. 七种基本程序的程序函数(续)
其次，对原程序种的每一个编号为i，出口线编号 为J的函数节点h，构造一个新的序列程序gi，如图：
h i
j
gi= h
L:=j
对每一个编号为i，出口线编号为j、k的谓词节点p， 构造一个新的IF-THEN-ELSE程序gi，如图：
j
i p k
L:=j
gi=
p
L:=k
Chap4 结构化程序设计及正确性证明
练习： 计算下列语句序列的程序函数： y:=a; y:=x*y+b; y:=x*y+c; y:=x*y+d
Chap4 结构化程序设计及正确性证明
二、结构化定理
3. 程序函数的计算
2)无循环程序的程序函数 首先：构造有穷的执行树 然后：对每条路径写出相应的表达式 例：
f
q
g
p
h
