Floyd良序集法证明程序终止性

发布时间 2023-12-12 23:33:53作者: 鸢凛

1.设断点并建断言

  (1)开始处A:

  (2)循环主干处B,C等:

2.取良序集并定义函数

  (1)良序集:一般为<N,<>(与证良函数有关)

  (2)函数:为存在循环的断点定义函数f(x)(注意:f(x)需要随着循环递减)

    • 找随循环递减的f(x)的技巧:
      • 看变化量和跳出循环的判断条件中的变量
      • 尝试单个变量
      • 尝试简单相加减
      • 尝试给变量乘以循环中变化系数的反函数

3.证良断言(与归纳断言法的证明方法一致)

  (1)回顾:

    

4.证良函数

  (1)证明fB(X,Y)是良函数,只需证

      

5.证明终止条件成立

  (1)只需证明以下成立

    例:

6.例题

  以下例题是证明完全正确性,即证明部分正确性+终止性,需要使用归纳断言法和良序集法一起证明

   

 

  解题过程: