讲义第三章下版

Chapter

3.结构化程序设计方法(下）谢在鹏EMAIL:

ZXIEHHU@163.COM本讲义修改自叶枫老师去年的讲义知识点回顾：结构化程序设计特征1.2.3.知识点回顾：结构化程序设计的原则1.顺序、选择、循环2.3.4.5.Floyd部分正确性证明--流程图方法Floyd部分正确性证明-例：N

-1s

=

A(i

)i=0Floyd的不变式断言法输入断言输出断言y：一组中间变量

x：输入变量

xy：蕴含符ri(x,y)：通过该通路后y的值通过此路径的条件实例1

21

2(x1,x2)fi

(y1,y2)y1-y2fi

y1y2-y1fi

y2DB

…

P(x,y)

Tru(1)若y1>y2，gcd(y1,y2)=gcd(y1-y2,y2)(2)若y2>y1，gcd(y1,y2)=gcd(y1,y2

-y1)(3)若y=y，gcd(y

,y

)=y1=y2ey1fi

zC…y(x,z)GFalseETrue开始A

…

j(x)y1=y2Falsey1>y2结束设x1,x2是正整数，求他们的最大公约数z=gcd(x1,x2)。我们知道，对于任意正整数y1,y2，有下列关系：(x1,x2)fi

(y1,y2)y1-y2fi

y1y2-y1fi

y2y1fi

zC…y(x,z)DB

…

P(x,y)

TrueGFalseETrue开始A

…

j(x)y1=y2Falsey1>y2结束(1)建立断言(x1,x2)fi

(y1,y2)y1-y2fi

y1y2-y1fi

y2A

…

j(x)y1fi

zC…y(x,z)DB

…

P(x,y)

TrueGFalseETrue开始y1=y2Falsey1>y2结束通路1：A-->B所以(2)建立检验条件-1(x1,x2)fi

(y1,y2)y1-y2fi

y1y2-y1fi

y2A

…

j(x)y1fi

zC…y(x,z)DB

…

P(x,y)

TrueGFalseETrue开始y1=y2Falsey1>y2结束通路条件(2)建立检验条件-2所以检验条件为：(x1,x2)fi

(y1,y2)y1-y2fi

y1y2-y1fi

y2A

…

j(x)y1fi

zC…y(x,z)DB

…

P(x,y)

TrueGFalseETrue开始y1=y2Falsey1>y2结束通路条件通路2：B-->D-->B通路后的y值(2)建立检验条件-3(x1,x2)fi

(y1,y2)y1-y2fi

y1y2-y1fi

y2A

…

j(x)y1fi

zC…y(x,z)DB

…

P(x,y)

TrueGFalseETrue开始y1=y2Falsey1>y2结束(3)

证明检验条件-1通路1：通路2：(3)

证明检验条件-2通路3：通路4：不变式断言法实例-2n2<x<(n+1)2(0,0,1)->(y1,y2,y3)y2+y3->y2y1->zABDx

Z

=

开始C(y1+1,y3+2)->(y1,y3)结束y2<x(0,0,1)->(y1,y2,y3)y2+y3->y2y1->zADC开始(y1+1,2*y1+1)->(y1,y3)结束By2<xy1=n;y3=2*y1+1；y2=

(y1+1)2;通路1：A-->B(2)建立检验条件-1(0,0,1)->(y1,y2,y3)y2+y3->y2y1->zABDC开始(y1+1,2*y1+1)->(y1,y3)结束y2<xy1=n;y3=2*y1+1；y2=

(y1+1)2;(2)建立检验条件-2通路2：B-->D-->B(0,0,1)->(y1,y2,y3)y2+y3->y2y1->zABD开始C(y1+1,2*y1+1)->(y1,y3)结束y2<xy1=n;y3=2*y1+1；y2=

(y1+1)2;(2)建立检验条件-2通路2：B-->C(0,0,1)->(y1,y2,y3)y2+y3->y2y1->zABD开始C(y1+1,2*y1+1)->(y1,y3)结束y2<xy1=n;y3=2*y1+1；y2=

(y1+1)2;(3)

证明检验条件-1通路1：通路2：(3)

证明检验条件-2通路3：良序集方法证明程序终止性实例

x

(0,0,1)

(y1,y2,y3)(y1+1,y3+2)(y1,y3)y1

zB’y2+y3

y2B…

p(x,y)y2<x开始结束Dy2

<xy3>0终止表达式

x-y2循环结构终止的条件表达式(0,0,1)

(y1,y2,y3)y2+y3

y2(y1+1,y3+2)(y1,y3)y1

zB’

…q(x,y1,y2,y3)A…φ(x)B…

p(x,y)y2<x开始结束D终止表达式(0,0,1)

(y1,y2,y3)y2+y3

y2(y1+1,y3+2)(y1,y3)y1

zB’

…q(x,y1,y2,y3)A…φ(x)B…

p(x,y)y2<x开始结束D终止表达式y2

<xy3>0(0,0,1)

(y1,y2,y3)(y1+1,y3+2)(y1,y3)y1

zB’

…q(x,y1,y2,y3)y2+y3

y2B…

p(x,y)A…φ(x)2y

<x开始结束D