--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on December 2012 ---
Thank you for your answers but I still not yet solve my problem: I would like to write this in ACSL " if there exists an integer i in? [0 n-1] such that for any integer j in the same intervall queue[i]>queue[j] and queue[i]>5 and? queue[i]<10 so \result==queue[j]" 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/20121220/6f1d352c/attachment-0001.html>