ex. 4.2.6.4, wrong clauses?

[alexioslyrakis]

In the exercise 4.2.6.4 the provided answer is the following:

void foo(){
  int i ;
  int x = 0 ;
  /*@
    loop invariant 0 <= i <= 19 ;
    loop assigns i ;
    loop variant 20 - i ;
  */
  for(i = 0 ; i < 20 ; ++i){
    if(i == 19){
      x++ ;
      break ;
    }
  }
  //@ assert x == 1 ;
  //@ assert i == 19 ;
}

I see three issues here:

• Shouldn't we include "x" as well in the loop assigns clause?
• I don't see how this is verified by WP. First we say that loop doesn't assign "x", i.e. x value isn't changed, and then Frama-C asserts that x is equal to 1.
• the loop variant clause can change to loop variant 20 - i ;, right?

[AllanBlanchard]

Hello,

You should have a closer look to the section 4.2.5 ;) . About your 2 first questions, basically, the reason why, this properties are proved is due to the early termination of the loop.

For the variant, I think that you made a mistake in your question, as it is the same as in the source code of the function. However, I see that I forgot to exclude 20 for this illustration of early termination. In fact here, I wanted to write loop variant 19-i, which is also a correct variant.

Thank you!

[alexioslyrakis]

Hello,

You're right, I haven't noticed! Section 4.2.5 says "It basically corresponds to any algorithm that searches, using a loop, a particular condition respected by an element in a given data-structure and stops when it founds it to perform some operations that are thus not really part of the loop. From a verification point of view, it allows us to simplify the contract of the loop: we know that the (potentially complex) operations performed just before we stop do not need to be considered when designing the invariant.". That clarifies it, "x" assignment is not part of the loop.

For the variant, yes I meant to write loop variant 19 - i ; so we agree on that, IMO the issue can close, thank you Allan :)

[AllanBlanchard]

I fixed the variant, thank you :)

[AllanBlanchard]

@AlexLyrr I want to add you in the list of contributors (in the introduction) in the next version of the tutorial. Which name should I use?