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] axiomatic recursive definition

  • Subject: [Frama-c-discuss] axiomatic recursive definition
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Fri Nov 28 12:39:33 2008
  • In-reply-to: <C007348074AC41E4BAEB384DA3F45F73@AHARDPLACE>
  • References: <C007348074AC41E4BAEB384DA3F45F73@AHARDPLACE>
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                    |