Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Frama-C labels/States
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Mon Nov 24 09:03:01 2008
  • In-reply-to: <024701c94bfc$439c2c40$cad484c0$@com>
  • References: <023801c94bef$bef36960$3cda3c20$@com> <4926E88E.1070101@inria.fr> <024701c94bfc$439c2c40$cad484c0$@com>

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                    |