|
Imperative Programs |
|
Imperative programs for AProVE can be written by using the language
IPAD. IPAD is an abbreviation for Imperative Programming Language with
Algebraic Data Structures. This language is highly
influenced by C and Java.
An IPAD program consists of a collection of data structures and
algorithms. Data structures can be defined by using the keyword
structure. An example for such a definition is the following which
defines the data structure nat. Nat is a representation for the
natural numbers.
structure nat {
0 : nat;
succ : nat p -> nat;
} witnessterm 0;
The data structure nat uses the two constructors 0 and succ. So the
natural number one, for example, is represented by succ(0). But there are
two things that should not be directly obvious. The first thing should be
the sign p in the declaration of succ. This is a name for a selector for the
argument of the constructor succ, so p(succ(0)) evaluates to 0. The other
thing that should not be directly obvious, is the statement closing the
declaration of nat. This statement is a so called witness term which is
used as a return value in case the selector is not applicable. In example
p(0) evaluates to 0. But this witness terms need not to be defined,
because the AProVE System is able to determine them by itself. An example
for such a data structure definition is the following, which defines a list of
natural numbers, using the above defined data structure for natural
numbers. In this example the witness term will be automatically set to
nil.
structure list {
nil : list;
cons : nat car, list cdr -> list;
}
There exists also one predefined datat structure in IPAD, called bool.
Bool has the two constructors true and false.
However, now we have defined our data structures, the question remaining
is, how do we define algorithms in IPAD. Defining algorithms in IPAD is
very easy, because this is pretty similar to the definition of functions in
C. All control structures supported by C can also be used in IPAD. The
following example shows a definition of the function plus.
nat plus( nat x, nat y ) {
while !(x==0) {
x = p(x);
y = succ(y);
}
return y;
}
In the above example x and y are modified during the calculation. But
these modification have no side-effects, because the above example has
call-by-value parameters. In IPAD there exists also the possibility to
have call-by-reference parameters. The above example can be rewritten to
use call-by-reference parameters so that y is used to return the result
of the calculation. These call-by-reference parameters are marked by the
keyword var.
void plus( nat x, var nat y ) {
while !(x==0) {
x = p(x);
y = s(y);
}
}
Because of the presence of algebraic data types there exists also the
possibility to use pattern matching. This is shown in the following
example which computes the reversal of a list of natural numbers. In the
head of the while loop it is checked if l could be matched against the
constructor cons, if so the expression is evaluated to true.
list reverse(list l) {
list k = nil;
while (l ~ cons) {
k = cons(car(l), k);
l = cdr(l);
}
return k;
}
For further details on IPAD please consult the following EBNF or this
diploma thesis[Has04].
Program = Declaration { Declaration }.
Declaration = (Structure | Function).
Structure = "structure" Identifier "{" Constructor {Constructor} "}"
[Witnessterm] ";".
Constructor = Identifier ":" [IdentifierList] Identifier ";".
IdentifierList = {IdentifierComma} Identifier Selector "->".
IdentifierComma = Identifier Selector ";".
Function = DataType | "void" Identifier "(" [ParameterList] ")" "{"
StatementList "}".
ParameterList = ["var"] DataType Identifier { "," ["var"] DataType
Identifier }.
StatementList = ""| NewStatementList.
NewStatementList = Statement [NewStatementList] ";".
Statement = "if" Term "{" Statementlist "}" "else" "{" Statementlist "}" |
"if" Term "{" Statementlist "}" |
"{" StatementList "}" |
"return" [Term] ";" |
"while" [Term] "{" StatementList "}" |
"do" "{" StatementList "}" "while" "(" Term close ")" ";"
"for" "(" [SimpleStatement] ";" [Term] ";" [SimpleStatement] ")" "{" StatementList "}" |
SimpleStatement";".
SimpleStatement = ["var"] Identifier "=" Term |
"skip" |
Identifier "(" TermList ")".
TermList = Term { "," Term }.
Term = SimpleTerm Identifier Term | SimpleTerm.
SimpleTerm = "(" Term ")" |
Constant |
Variable |
Identifier "(" TermList ")".
Variables, Identifiers, Constants and TypeNames could consist of any letter and
digit with the only restriction that the first sign is a letter or a _.