--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on December 2012 ---
Thank you for your answer Virgile. This new version is verifiable: /*@ requires \valid_range(queue,0,14); ??? assigns \nothing; ??? ensures \exists int e; 0<=e && (\forall int i; 0<=i<15 && e > queue[i]) && ( (e >= 5) || (e >= 10) ) ==> \result == 0; ??? ensures \exists int e; 0<=e && (\forall int i; 0<=i<15 && e > queue[i]) && ( (e < 5) && (e < 10) ) ==> \result == e; ??? ???? */ int find_array_max(int queue[15]){ ?int i, largest; ? largest = 0; /*@ loop variant 15 - i; ??? loop invariant 0 <= i <= 15; ??? */ ? for (i = 0; i < 15; i++) { ??? if (queue[i] > largest) ????? largest = queue[i]; ? } ? if ( (largest >= 5) || (largest >=10) ) { ??? ??? ? return 0; ? } ?? return largest; } But my problem in this new specification is how to say that e is an element in the queue array. Could you help me, please? Best regards, Intissar ________________________________ De?: Virgile Prevosto <virgile.prevosto at m4x.org> ??: frama-c-discuss at lists.gforge.inria.fr Envoy? le : Mercredi 19 d?cembre 2012 10h36 Objet?: Re: [Frama-c-discuss] Problem with ACSL annotations Hello, Le mar. 18 d?c. 2012 12:28:20 CET, intissar mzalouat <intissar_mzalouat at yahoo.fr> a ?crit : > /*@ requires \valid_range(queue,0,14); > ??? ensures \result==0 ==> (\exists int i;0<=i<15 && ((\forall int j; > 0<=j<15 && queue[i] > queue[j] )&&((queue[i]>=5) || > (queue[i]<=10)))); */ int find_array_max(int queue[15]){ > > I had some problems to write postconditions in ACSL for this function. > Could you, please help me? It would have helped if you had stated explicitely what your problems were, but my guess is that \forall int j; 0<=j<15 && queue[i]>queue[j] should be replaced with \forall int j; 0<=j<15 ==> queue[i]>queue[j] The former says that for any int j, both 0<=j<15 and queue[i]>queue[j] hold, which is trivially falsified by taking j == -1. The latter says that for any int j between 0 and 15, we have queue[i]>queue[j]. More generally, the informal spec "for any x in P, Q holds" is written \forall x; P ==> Q, while "there exists x in P such that Q holds" is indeed written as what you've done: \exists x; P && Q. Best regards, -- E tutto per oggi, a la prossima volta. Virgile _______________________________________________ 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 -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121219/e7327b78/attachment.html>