循环不变，没有返回值，是否可能？并且程序正确

So I'm writing this program that store user input on linked list and reverse it, but I'm a bit lost. Is it possible to come up a loop invariants for types of loop where it doesn't return any value? For example a loop that is located inside main.

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

Here's an example of a loop I use to get user input inside main and store it in a linked list, of course there are more on the code, but I only showed what's relevant.

这是一个循环示例,我用来在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; 
}

Is it possible to come up with a loop invariant for this? Also what does it mean by program correctness and how do I proof it in my case?

是否有可能为此设置一个循环不变量?程序的正确性又是什么意思?我如何在我的案例中对其进行证明?

Thanks!

2 个解决方案

#1

A loop invariant is a condition that is necessarily true immediately before and immediately after each iteration of a loop

循环不变量是一个条件,它必须在循环的每次迭代之前和之后立即生效

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. You can use this as a proof.

所以在这种情况下,temp在循环的每次迭代之前和之后都是NULL。您可以将此作为证据。

For more details refer http://en.wikipedia.org/wiki/Loop_invariant and What is a loop invariant?

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

#2

A loop invariant is a formal statement about the relationship between variables in your program which holds true just before the loop is ever run (establishing the invariant) and is true again at the bottom of the loop, each time through the loop (maintaining the invariant)

循环不变量是关于程序中变量之间关系的形式语句,它在循环运行之前保持为真(建立不变量),并且在循环的底部再次为真,每次循环(保持不变量) )

Presuming this is what you wanted. The code shown by you looks good to add a node to the linked list so regarding correctness it should be fine.

假设这是你想要的。您显示的代码看起来很好,可以将一个节点添加到链表中,所以关于正确性它应该没问题。

char str[100];
int cnt = 0;
int n;
fgets(str,100,stdin);
if(strlen(str) < 99)
str[strlen(str) -1] = '\0';

n = strlen(str);
/* cnt <= n */
while(str[i] != '.')
{
   /* cnt <= n */
   // Do your stuff
   cnt++;
   /* cnt <= n */
}
/* cnt <= n */

The loop invariant will be

循环不变量将是

cnt <= n

#1