--- layout: fc_discuss_archives title: Message 17 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 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>