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

[Frama-c-discuss] axiomatic recursive definition



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                    |