Maude-help mailing list

[Marc Boyer <Marc.Boyer AT onera.fr>]

Le 25/08/2011 17:49, Morandi Benjamin a écrit :
> We are implementing a structural operational semantics in Maude. In this
> semantics, the state of a program is modeled as an abstract data type
> (ADT). The ADT consists of constructors that return a new ADT instance,
> queries that take an ADT instance to return the state of the instance,
> and commands that take an ADT instance to return another ADT instance
> with a modified state. Axioms describe the effect of constructors,
> commands, and queries.
>
> The OBJECT ADT serves as an example. It has the following query
> returning the type of an object:
>
> type: TYPE
>
> It also has a constructor that creates a new instance with a certain type t:
>
> make: TYPE -> OBJECT
>
> axioms
>
> type (make (t:TYPE)) = t
>
> I understand that I should define a functional module for the OBJECT
> ADT. However, I am not sure how to implement the ADT axioms. Does anyone
> have a suggestion?

I do not know exactly what is your complete need, but here is a simple 
example that seems to match you example.

fmod ADT is

  sort Type .
  sort Object .

  op make : Type -> Object .
  op type : Object -> Type .

  ops int float : -> Type .

  var t : Type .
  eq type( make( t ) ) = t .
endfm

red type( make( int ) ) .
red type( make( float ) ) .


--
Marc Boyer, Ingenieur de recherche                              ONERA
Tel: (33)  5.62.25.26.36                                         DTIM
Fax: (33)  5.62.25.26.52                          2, av Edouard Belin
http://www.onera.fr/staff/marc-boyer/          31055 TOULOUSE Cedex 4