C语言 没有返回值的循环不变，可能吗?和程序正确性

Question

所以我正在编写这个程序，将用户输入存储在链表上并反转它，但我有点迷茫。 是否有可能为不返回任何值的循环类型提出循环不变量？例如，位于 main 内部的环路。

这是我用来在 main 中获取用户输入并将其存储在链表中的循环示例，当然代码上还有更多内容，但我只展示了相关的内容。

typedef struct node {
char x; // data
struct node* next; // link to next node
} Node;
int main(void){
char c = ' ';
Node* start = NULL; 
Node* temp; 
while(c!='.'){
    c=getchar();
    temp=(Node*)calloc(1, sizeof(Node));
    temp->x = c; 
    temp->next = start; 
    start = temp; 
}

是否有可能为此提出一个循环不变？另外，程序正确性是什么意思，我如何在我的情况下证明它？

谢谢！

Answer 1

循环不变量是循环每次迭代之前和之后必须为真的条件

int main(void)
{
    char c = ' ';
    Node* start = NULL; 
    Node* temp = NULL; 
    while(c!='.'){
        /* temp = NULL before each iteration*/
        c=getchar();
        temp=(Node*)calloc(1, sizeof(Node));
        temp->x = c; 
        temp->next = start; 
        start = temp;
        temp = NULL;
        /* temp = NULL after each iteration*/
    }

So in this case temp is NULL before and after each iteration of the loop .你可以用这个作为证明。

有关更多详细信息，请参阅 http://en.wikipedia.org/wiki/Loop_invariant什么是循环不变量？

Answer 2

循环不变量是关于 程序中的变量在循环之前为 true 曾经运行（建立不变量），并且在底部再次为真 的循环，每次通过循环（保持不变性）

假设这是你想要的。您显示的代码看起来不错，可以将节点添加到链表中，因此关于正确性应该没问题。

char str[100];
int cnt = 0;
int n;
fgets(str,100,stdin);
if(strlen(str) < 99)
str[strlen(str) -1] = '';
n = strlen(str);
/* cnt <= n */
while(str[i] != '.')
{
   /* cnt <= n */
   // Do your stuff
   cnt++;
   /* cnt <= n */
}
/* cnt <= n */

循环不变性将是

cnt <= n