--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on December 2012 ---
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