Tag Archives: Jessie

Loop assigns, part 3: On the importance of loop invariants
Virgile Prevosto on 27 October 2010

Context Last week's post mentioned that it is not possible to prove the following loop assigns with Jessie: void fill(char* a, char x) { //@ loop assigns a, \at(a,Pre)[0..(a-\at(a,Pre)-1)]; for(;*a;a++) *a = x; return; } and in fact this annotation is not provable. An hint to where the issue lies...

Read More

loop assigns, part 2
Virgile Prevosto on 15 October 2010

Context Last week's post asked how to express a loop assigns for the following code: void fill(char* a char x) { for(;*a;a++) *a = x; return; } The difficulty here is that the pointer a is modified at each step of the loop and that we must take this fact...

Read More