循环不定式可以用来证明一个算法的正确性:

比如我现在有一个算法A,我要证明它的正确性:步骤如下:

第0步:定义循环不定式;

第1步:证明循环不定式在算法开始的时候是正确的;

第2步:证明循环不定式在算法每次迭代(循环)的时候是正确的;

第3步:证明循环不定式在算法结束时是正确的;

以下是用循环不定式来证明冒泡排序的正确性:

首先看代码:

#include<stdio.h>
int main()
{
	int data[15];
	int len = 15;
	for(int i = 0; i < 15; i++)
	{
		scanf("%d",&data[i]);
	}
	for(int i = 0; i < len - 1; i++)
	{
		for(int j = 0; j < len - 1 - i; j++)
		{
			if(data[j] > data[j+1]
            {
                int temp = data[j];
    			data[j] = data[j+1];
	    		data[j+1] = temp;
            }

		}
	}
	for(int i = 0; i <15; i++)
	{
		printf("%d ",data[i]);
	}
	printf("\n");
	
	
	return 0;
} 

第0步:定义循环不定式data[len-1 - i] ~ data[len - 1]  是有序的;

第1步:在算法开始前,i = 0;data[len -1 - i]  ~ data[len-1] 是有序(这是很显然的,因为一个数一定是有序)的;

第2步:首先来看第二个循环,这个循环的作用是将data[0] ~ data[len - 1 - i]之间的最大数移动到dp[len - 1 -  i];

             我们来看第一个循环,每次循环结束后data[len - 1 -i] 到data[len -1]都是有序的,因为第二个循环的的

              作用就是将data[0] ~ data[len - 1 - i]之间的最大数移动到data[len - 1 -  i]移动到data[len-1-i];

第3步:当算法结束后,i = len - 1,data[len - 1 - i] 到 data[len - 1] 也就是data[0] ~ data[len - 1]是有序;

证毕

不理解的借助纸和笔来模拟一下;