--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on December 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with ACSL annotations



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>