--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on July 2010 ---
Hello all, working with the example from chapter 6 in the ACSL mini-tutorial, I arrived (after what I believe are changes that make it simpler to understand for both provers and students) at: /*@ requires n > 0; requires \valid(p+ (0..n-1)); assigns \nothing; ensures \forall int i; 0 <= i <= n-1 ==> \result >= p[i]; ensures \exists int e; 0 <= e <= n-1 && \result == p[e]; */ int max_seq(int* p, int n) { int res = *p; /*@ loop invariant \forall integer j ; (0 <= j < i) ==> (res >= p[j]) ; loop invariant 0 <= i <= n; loop invariant \exists integer j ; (0 <= j <= n-1) && (res == p[j]) ; loop variant n-i ; */ for(int i = 0; i < n; i++) { if (res < p[i]) { res = p[i]; } } return res; } Good news! Almost everything is proved (alt-ergo 0.91) And what is not proved such as the establishment of the invariant with the existential quantifier is a good opportunity to explain how these are usually difficult for automatic provers to handle. Then as a last change to make the source code more readable, I changed the *p to p[0] in the first line of the function. And then, better news! Everything is proved now. I didn't even know that it was possible to distinguish between *p and p[0] after normalization by CIL. So my questions are: - are the proof obligations generated when the program uses *p provable (sorry for this naive question but I only have alt-ergo for technical reasons)? - should one of the various translations between C and the proof obligations have the same results whether *p or p[0] is used, or would that be likely to cause more issues than it solves? Pascal