IGNORANT

认识循环不变式

概念

循环不变式是Floyd首先引入的, 其后Dijkstra和Gries作了更深入的研究, 从算法逻辑上给出严格的定义:循环不变式是在循环体的每次执行前后均为真的断言。
循环不变式被广泛用于程序验证。根据循环不变式,容易设计清晰的循环结构。

高级语言的循环结构:

初始化;
while(条件){
    循环体;
}

在循环入口处,程序处于一种状态${p_0}$;循环出口处,程序处于一种状态${p_n}$。每次循环,对应一个程序状态${p_i}$。从循环入口到出口,程序状态变化:${p_0}$、${p_1}$、……、${p_i}$、……、${p_n}$。其中${p_n}$是目标状态。
程序状态是一个谓词逻辑,若存在谓词p,使得p从${p_0}$到${p_n}$都成立,则谓词p成为循环不变式。

特征

设计循环实例

例如求N!,N>=1为自然数。
分析:先引入I和Fact表示自然数和阶乘计算得到的结果。那么,

循环结束时有:Fact==N!,且I==N;

每次循环体有:Fact==I!,且I<=N;

因此,在下一次循环需要另一个自然数I'与Fact相乘,即I'=I+1。故循环体需要两条语句:I=I+1;Fact=Fact*I;
在初始化阶段,也要保证I<=N && Fact==I!为真,因此在入口点初始化I=Fact=1;。C语言实现如下:

int N=10;
int I=1;
int Fact=1;
//循环不变式Fact==I! && I<=N为真
while(I<N){
    I=I+1;
    Fact*=I;
//循环不变式Fact==I! && I<=N为真
}

根据上述,设计循环程序可以按如下步骤:
1.构思解决问题的循环策略。
2.决定循环所需变量。
3.由2写出循环结束后应得到的期望结果。
4.根据3的特点构造循环不变式。
5.根据循环不变式初始化变量。

文章摘抄自:
1.循环不变式在程序设计教学中的应用

当前页面是本站的「Google AMP」版。查看和发表评论请点击:完整版 »