--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on November 2008 ---
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 |