With ManTa a user can: specify ADT, propose terms to rewrite (find
normal form), or propose conjectures to be proved. Each one has a specific
2.1 Lexical Conventios
2.2 ADT Syntax in BNF
|ident = ['A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '0'-'9' '_']*||An identifier should begin with a letter. We could allow more identifiers (e.g. $, %, &, etc), but this could make difficult the translation to some programming languages|
| EQUAL( expr , expr )
| if expr thenexprelseexprfi
| ident ( arguments )
|The expressions are built with: ERROR, EQUAL(.,.) if . then . else
. fi. Functions instanced and constants.
Constants are treated as functions without parameters (empty domain), they should be written without parenthesis.
|The arguments of function should be separated with comma ','.|
|An axiom is an equality between expressions. It's not an assignment but a rewriting rule (the left side rewrites in the rigth one) as will be seen later.|
|The user can give axioms only for selectors|
ident (i) *notEmptyDomain
| ident * notEmptyDomain
| ident (i)
|The domain of a function can be a product of ADTs each one of them can be inductive (used to make induction in proofs) or not.|
|A function can have empty domain (they are constants)|
|A generator is a function whose codomain should be the defined ADT. There are two kinds of them: initials and constructors. However the differences are not captured here but with the static semantics.|
|User should not give axioms for generators. Note that an ADT can have no generators in that case it is an extension (just a set of new selectors to extend other ADTs)|
|A selector is a function with axioms given by the user. The presented rule only describes the signature for a selector, the sintax of the axioms was already presented (see axiom)|
|User should give at least one selector for each ADT. If it has generators it must have at least an equality.|
|An ADT can have parameters (in that case it is a generic ADT).|
|In this version of ManTa the parameters are not fully supported. Hence their dynamic semantics will not be described in this document.|
ADT ident [parameters ]
|An ADT has a name, it can have parameters, generators called initials (they don´t include the defined ADT in it's domain) and generators called constructors (they include the ADT in it's domain). Each declared selector should have axioms to define it's behavior on generators|
There are available a lexical analyzer to
be used with ocamllex, and a parser to be used
with ocamlyacc. They can be adapted easily to other tools (e.g. flex
2.3 Normalization Syntax
2.4 Conjectures Syntax
expr = expr
2.5 Predefined Abstract Data Types
The only primitive ADT in ManTa is BOOL. It defines boolean values TRUE, FALSE and the functions AND(.,.), OR(.,.), NOT(.), IMP(.,.), EQ_BOOL(.,.). It's required by the built in function if E1 then E2 else E3 fi, whose first parameter (E1) must have type BOOL.
Other predefined ADTs are: NAT (natural numbers), Char and String. By default these types can't be modified.
In adition to those types there are some classical ADT: List,
2.6 The preprocessor
Writing ManTa files (ADT, conjectures or terms to rewrite) that require
the primitive types NAT, Char
and String is difficult,
boring and prone to errors. This is so since the numbers have to
be represented as SUC(SUC...(SUC(ZERO))..), the character
as char(SUC(SUC(...SUC(ZERO)...)) and the String
as lists of characters.
With a preprocessor the user can write easier and faster by using numbers, character constants and strings. The preprocessor receives such files as inputs, transforms them to ManTa syntax and writes files.
The preprocessor works only at lexical level, it doesn't check the syntax of the file (so it can be used with any file, i.e. specifications, terms to rewrite or conjectures).
2.7 The postprocessor
This component should be the inverse of the preprocessor. It receives
a ManTa file and it returns a text file easy to read. (NAT ground
terms translated to numbers, special characters translated, strings translated,
2.8 Suggested conventions
To facilitate writing and reading ADTs and conjectures, some conventions are suggested (inspired in the Java Language conventions)