--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on November 2008 ---
I'm sorry, I do not understand the question. Could you make it more precise ? An axiomatic definitions is a mean to provide a simple kind of algebraic specification. It is a set of declarations which, as a whole, define a mathematical model (or indeed a set of possible models if things are left unspecified). There is no notion of "execution" in it, it's purely declarative. May be you should consider reading some introductory material to algebraic specification ? Hope this helps, - Claude Christoph Weber wrote: > Hi, > > I want to know whether an axiomatic definition like nb_occ() processes an array in the meaning of execution? > > Cheers > > Christoph > > > ------------------------------------------------------------------------ > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss@lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- 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 |