ManTa 3

ABSTRACT SYNTAX TREE
 3.1  Specification

The abstract syntax trees can be described in ManTa (in fact they are), although the Z specification language will be used as metalanguage.  The following Z definitions will be assumed:

[Bool]
true,false:Bool
(true=false)
x:Bool x=truex=false
Description
Z
ManTa
Identifiers (Strings that follow the ident rule of syntax) [Ident]  String
One parameter of an ADT is an identifier Parameter::=parameter<<Ident>> ADT Parameter []
INITIALS
  parameter:String->Parameter
CONSTRUCTORS
Function domain (generator or selector) is composed of the name and a boolean to indicate if it is an inductive parameter (in induction proofs inductive parameters are the first tried ) Domain::=domain<<IdentBool>> ADT Domain []
INITIALS
  domain:String*BOOL->Domain
CONSTRUCTORS
A generator is a name and its domain, the codomain is always the defined ADT.  The domain is a product of ADTs represented here as a list. Generator::=generator<<Ident
seq Domain>>		 ADT Generator []
INITIALS
 generator:String*LDomain
           ->Generator
CONSTRUCTORS
The possible expressions are: ERROR, variables, instanced generators, instanced selectors, EQUAL(.,.) or if E1 then E2 else E3 fi.  Expr::=
  errorExpr |
  varExpr<<Ident>> | 
  genExpr <<identseq Expr>> |
  selExpr <<identseq Expr>> |
  eqExpr <<ExprExpr>> |
  ifExpr <<ExprExprExpr>>		 ADT Expr []
INITIALS
 errorExpr:->Expr
 varExpr:String->Expr
 genExpr:String*LExpr
         ->Expr
 selExpr:String*LExpr
         ->Expr
CONSTRUCTORS
  eqExpr:Expr*Expr -> Expr
  ifExpr:Expr*Expr*Expr 
         -> Expr
An axiom has a left expression and a right expression (it's a rewriting rule, the first expression rewrites in the second) Axiom::= axiom<<ExprExpr>> ADT Axiom []
INITIALS
  axiom:Expr*Expr -> Axiom
CONSTRUCTORS
A selector function has a name, a domain, a codomain, it can be a characterizer and it should have axioms (at least one) Selector:=selector<<Identseq Domain
IdentBoolP1 Axiom>>		 ADT Selector []
INITIALS
  selector:String*LDomain*
        String*LAxiom
           ->Selector
CONSTRUCTORS
An Abstract Data Type, has a name ,  a list of parameters, a set of generators and a non empty set of Selectors AbsType::=absType<<Ident
seq ParameterP Generator
P1 Selector>>		 ADT AbsType []
INITIALS
  absType:String*
        LParameter*
        LGenerator*
        LSelector
         -> AbsType
CONSTRUCTORS

 
 3.2 Hierarchy of ManTa ADTs

ManTa ADTs can be classified in the following way:
 

Generators Parameters Commentaries
Basic
Yes
 Usual ADT (e.g. NAT)
Extension They only add new selectors to the system of ADTs
(e.g. NumTh defines new function for NAT)
Generic
Yes
Yes
 Also known as parametric types (e.g. List). 
Generic Extension
Yes
 Types that generate extensions when instanced
(e.g. AddNEQ)

Other classification for ADTs is:


Concrete Syntax
Static Semantics