Allow the specification of ADT using a simple equational
language: The ManTa 3 language. The formal background of this language ensures that every specification written with it has a model.
Can generate semi-automatically new ADTs by some methods (Copy, Instatiation,
Cartesian Product, Restriction, Completion and Variation)
Includes some predefined types: NAT, BOOL, Char, String, List, Stack and Queue.
Allows the representation of ADTs using existing ADTs (e.g Represent the
ADT Stack with ADT Queue)
Rewriting
Includes a rewriting motor to evaluate expressions.
Theorem prover
Allows to prove equality theorems on specifications by Rewriting
and Induction
It can prove if a representation mantains the pretended semantics
Code Generation
It can generate implantations of the ADTs in ANSI C, and it also generates
a program to test the implanted ADT. The makefiles generated can
be used with almost every make program (includes special support for BC++
Make)
Includes a tool (m2ocaml) that can generate implementations of ADTs in Ocaml.
Interface
It can be configured in several languages (it's distributed with english
and spanish support), to interact with any text editor and supports some
compilers (gcc and bcc). Basic configurations can be done with a program
(manconf).
It also contains independent tools that can be used from the
command line or other applications:
mancomp the compiler
manrew the rewriting motor
mantheo the theorem prover
m2c C code generator
Plain and Emacs interfaces
It's written in ANSI C and is highly portable. The most recent version has been
compiled and tested in DOS with the compiler DJGPP, and in Linux, SunOS and OpenBSD with
the compiler gcc.
Sources
Some portions of the sources and documentation is in the public domain, while
others are covered by the GPL.
