Maude-help mailing list

["Morandi Benjamin" <benjamin.morandi AT inf.ethz.ch>]

Dear All,

 

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?

 

Best regards

 

Benjamin Morandi