Циклический инвариант без возвращаемого значения, возможно ли это? И правильность программы

Question

Итак, я пишу эту программу, которая хранит пользовательский ввод в связанном списке и отменяет его, но я немного потерян. Можно ли создать инварианты цикла для типов циклов, где он не возвращает никакого значения? Например, цикл, который находится внутри основного.

Вот пример цикла, который я использую, чтобы получить пользовательский ввод внутри основного и сохранить его в связанном списке, конечно, в коде есть больше, но я только показал, что актуально.

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

Петля инвариант является официальным заявлением об отношениях между переменными в программе, которая справедливо только перед циклом когда-либо работать (установление инварианта) и верно снова в нижних петле, каждый раз через петлю (поддерживая инвариант)

Предполагая, что это то, что вы хотели. Код, показанный вами, выглядит хорошо, чтобы добавить узел в связанный список, поэтому в отношении корректности это должно быть хорошо.

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 */ 

Инвариантный цикл будет

cnt <= n 

Answer 2

инварианта цикла является состоянием, которое необходимо истинно непосредственно перед и сразу же после каждой итерации цикла

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 и What is a loop invariant?