Clarifies measures and termination

[AllanBlanchard]

Use these commits directly to review the diff:

• https://github.com/acsl-language/acsl/commit/6b4c3b3a7a5521ede4b9ce7e0c8c8233ff4481f9
• https://github.com/acsl-language/acsl/commit/2fe777acc7cb3777602e0e73e0f45e5dbe85480c

There is a commit that trims spaces.

There was a misunderstanding in https://github.com/acsl-language/acsl/issues/79, this is also fixed.

[AllanBlanchard]

FYI @pbaudin @vprevosto @zilbuz

[vprevosto]

What if a function has a loop that might not terminate and another (before the first one, obviously) that ought to always terminate, as in

/*@ terminates \false; */
void f(void) {
  /*@ terminates \true; */
  {
     /*@ loop invariant  0 <= i <= 3;
            loop assigns i;
            loop variant 3 - i;
     */
     for (int i = 0; i < 3; i++) ;
  }
  while(1) ;
}

[vprevosto]

In other words, I'd suggest that the variant is conditioned by the terminates clause of the innermost contract enclosing it. In addition, it might also be worth it to state explicitly that , if a statement contract with terminates clause T1 is enclosed into another contract with terminates clause T2, we must have T2 ==> T1

[AllanBlanchard]

Oh yes, I forgot this case.

[pbaudin]

I have nothing more to say.

[AllanBlanchard]

Hum. What about the behavior of:

// decreases p for some_relation ;
void f(int *p){ 
  if(condition) f(p); 
}

The fact that some_relation must be well-founded is clear. If I correctly understand:

• some_relation cannot have labels,
• it must be evaluated @here.

This is somewhat what is explained in the section but I think that we could emphasize on this behavior.

[AllanBlanchard]

In fact, giving the details mentioned in the previous comment is probably more suitable for a course :thinking: , so let's forget about that.

[pbaudin]

@AllanBlanchard, in the branch clarifies-measures-termination of the Github project acsl-language/acsl I added a commit (the last one) that you could cherry-pick part of it to this pull request. By the way, these modifications can still be discussed here.

[AllanBlanchard]

I have included the commit made by @pbaudin and added a few details + fixed some typos. I think it is ready.

[pbaudin]

It is fine for me.

@vprevosto, are you ready to merge this pull request ?