--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on November 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C labels/States




B?rbara Vieira wrote:
> Hi Claude!
> Thanks for your help. The predicate sumone, just tries to specify b[i] =
> a[i] + 1.
> 
> So you are saying that there is no trick to Frama-C accept axiomatic
> definitions. If I want to define a predicate with some axioms I have use the
> oldest version. Is it correct?  

Of course not ! You have to use axiomatic definitions which provide a 
better replacement for older definitions by "reads" clauses and axioms.

what is the role of k1 , k2 , n, a1, b1, a2 , b2 if you just want to 
specify that b[i] = a[i] + 1 ? You do not need to axiomatize such a 
simple property: you can say

/*@ // sumone(a,b,n) is true whenever b[i] == a[i] + 1 for 0 <= i < n
   @ predicate sumeone(a,b,n) =
   @   \forall integer i; 0 <= i < n ==> b[i] == a[i] + 1;
   @*/

So why are you giving those complicated axioms ?

If your predicate is not exactly that, please explain in english what 
you are looking for. If you have hard time to define it, then ask for 
help in this list.

- Claude





-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |