--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on July 2010 ---
Hi, I cannot comment on the issue *p vs p[0] but I would like to refer to our treatment of max_seq and the slightly more general max_element algorithm in our "ACSL by Example" tutorial (Sections 3.7 and 3.8 in http://www.first.fraunhofer.de/owx_download/acsl-by-example-5_1_0.pdf). Here max_element was completely verified using alt-ergo, Z3, CVC3, Yices, and Simplify. Regards Jens -----Original Message----- From: frama-c-discuss-bounces at lists.gforge.inria.fr on behalf of Pascal Cuoq Sent: Thu 7/8/2010 12:08 AM To: Frama-C public discussion Subject: [Frama-c-discuss] *p and p[0] 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 _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- A non-text attachment was scrubbed... Name: not available Type: application/ms-tnef Size: 4018 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100708/ec646564/attachment-0001.bin>