Implementations are used to tell the compiler what algorithm to use.
There are two types of implementation: value implementation and state implementation. A value implementation specifies how a value is to be computed; a state implementation specifies how a predicate is to be satisfied.
An implementation that directly follows "^=" and an expression is a value implementation, as are implementations for functions specified with a satisfy condition. All other implementations are state implementations.
Implementations are built up from implementation items, separated by semicolons. A variant may be given at the start if the implementation is recursive. The grammar is:
Implementation:
via [decrease Variant ";"] ImplList [";"] end.NvImplementation:
via ImplList [";"] end.ImplList:
ImplItem *[";" ImplItem].ImplItem:
LocalDeclaration;
LetStatement;
PostCondition [NvImplementation];
ConditionalStatement;
ValueCompletor;
StateCompletor;
Assertion;
Label;
Jump;
BlockStatement;
Loop.
The initial Variant is only needed if the implementation is recursive and either the specification was not recursive (so no variant was given in the specification) or a the specification variant is insufficient for the implementation.
[SC] A discontinuous statement is defined as any statement which is a Jump, ValueCompletor, StateCompletor or a conditional statement each of whose branches ends in a discontinuous statement. A discontinuous statement may only appear as the last item in an implementation, the last item in a branch of a conditional statement, or immediately before a label (because the following statements would otherwise be unreachable).
[SC] The last ImplItem in an implementation must be a discontinuous statement.
LocalDeclaration:
LocalVarDecls;
FunctionDeclaration;
SchemaDeclaration;
PropertyDeclaration;
AxiomDeclaration;
ClassDeclaration;
TypeDeclaration;
HeapDeclaration.LocalVarDecls:
var LocalVarDeclGroup *["," LocalVarDeclGroup].LocalVarDeclGroup:
Identifier *["," Identifier] ":" PossConstrainedTypeExpression;
Identifier ":" AbbrevTypeExpression;
Identifier ":" TypeExpression "!" "=" Expression;
Identifier ":" "(" (ConstrainedTypeExpression | AbbrevTypeExpression) ")" "!" "=" Expression.
Variables, types, classes, functions, schemas, properties and axioms may be declared. The forms of declarations in an implementation are similar to the forms of global declarations. Declarations within implementations are referred to as local declarations and are not member declarations irrespective of whether the implementation is for a member or nonmember entity.
Local variables may be initialized at the time of their declaration using the "!=" forms of declaration.
LetStatement:
let Identifier "^=" Expression.
The let-statement is used to evaluate an expression and save the resulting value. It is similar to a constant declaration except that the expression need not be a compile-time constant.
The postcondition statement declares a postcondition to be satisfied. The rules defining what may be changed are exactly as for schema postconditions. The postcondition may itself be implemented.
Labels serve as the targets for jumps. The syntax for a label is:
Label:
Identifier ":" pre PredicateList.
The scope of a label is determined in the same way as the scope of a declaration (which means that it is not possible to jump into an implementation from outside).
The label precondition must be satisfied at the point immediately prior to the label unless that point is immediately after a jump. It must also be satisfied at all jumps to the label. Following the label, the only knowledge available to the validation is the following:
Therefore, the predicate list must encapsulate all assumptions required to satisfy the proof obligations of the following statements up to and including the next jump, label or completor (if any), or otherwise to the end of the statement list.
[PO: the precondition is true on the fall-through.]
A jump may be made to any label which is defined at a later point in the current implementation and is in scope at the point of the jump, provided that the label precondition is satisfied at that point. The syntax is:
Jump:
goto Identifier.
Labels obey the same scope rules as other declarations. Therefore, a label declared in an inner block cannot be referred to from outside the block; so jumping into a block is not possible.
Jumps are permitted only if there are no declarations or let-statements (other than within block statements, conditional statements, loops and nested implementations) between the jump and the target label.
[Note: it might be thought that jumps are anachronistic and have no place in a modern programming language; however, there are some situations where their use can simplify the code substantially. By insisting on a specification for the target of every jump, we tame the label/jump combination.]
[SC: the identifier after goto corresponds to a label in scope and within the current implementation. The jump is to a later point in the code.]
[PO: the precondition of the label which is the target of a jump is satisfied at the point of the jump.]
Loops have the following syntax:
Loop:
loop
LoopChangedVars
keep PredicateList
[until PredicateList]
decrease Variant ";"
ImplList [";"]
end.LoopChangedVars:
[LocalVarDecls ";"] change ExpressionList;
LocalVarDecls ";".
The loop begins with a set of local variable declarations (which will also usually initialize the variables), together with, following the word change, a list of variables from the enclosing scope which the loop is permitted to change. All variables other than those declared and listed in this section must remain constant.
The predicate list which follows keep is the loop invariant, a set of conditions which must be true at the start of the loop and remain true throughout its execution. Together with the until part, the loop invariant forms the postcondition for the loop.
The predicate list after until may be viewed both as a termination condition and as a partial postcondition for the loop (if multiple comma-separated predicates are given, they are &ed together as usual). If no until part is specified, the condition that the variant can no longer decrease is used (for example, if the variant consists of a single integer value, the loop will terminate when it is zero)
The variant following decrease follows the same rules as for variants in recursive functions and schemas (each iteration of the loop must decrease the variant).
Within the invariant, until-part and variant, primed expressions refer to the value of the expression at the start of each iteration; unprimed subexpressions refer to the value before any part of the loop is executed. Only objects which the loop is permitted to change may appear primed. Local variables must always appear primed as they have no meaning before the loop is executed (since they are declared within the loop).
The final implementation comprises a loop body which decreases the variant while preserving the invariant. This implementation may only modify local variables and terms which were declared in the change list. Within the loop body primed and unprimed expressions have their usual meanings.
[PO: The loop invariant is true on loop entry (where local variables have their initial values). The variant is valid on loop entry. If the until part is false, the loop body preserves the loop invariant, and either decreases the variant or causes the until part to become true.]
Assertions declare a set of predicates to be true at a point in an implementation without further work being necessary to achieve them, provided only that the original precondition is satisfied. They may serve as hints to the theorem prover as well as additional validation checks. Even if an assertion is unproven, it is still assumed satisfied during validation of the statements that follow. The syntax for assertions was given in section 5.4.2.
ConditionalStatement:
if Guard ImplList *[";"Guard ImplList] [";" LastImplGuard] fi.LastImplGuard:
EmptyGuard ImplList [";"];
";";
"[" "]".
The conditional statement is structurally similar to the conditional expression except that the enclosing brackets are replaced by if fi and each guard is followed by an implementation item list instead of an expression. If no EmptyGuard part is present, at least one of the guards must be satisfied.
Each ImplList within a conditional statement defines a new scope; therefore any declarations within a branch of a conditional statement are not visible in other branches, nor are they visible outside the conditional statement.
BlockStatement:
begin ImplList [";"] end;
par ImplList [";"] end.
The begin...end block statement puts the enclosed implementation in its own scope. The par...end statement is similar, except all the statements in the list are notionally executed in parallel, and so must modify disjoint objects.
A value completor has the syntax:
ValueCompletor:
value ExpressionList.
Value completors are only allowed in value implementations (not in state implementations). The number of expressions in ExpressionList must be one, except for implementations of functions that return multiple results, in which case the number of expressions must either match the number of returned results or there must be only one expression and this must take the form of a recursive call to the function. The expression(s) must be provably equivalent to the required value(s) as defined in the specification of the function, operator, selector or constructor which is being implemented. The effect of a value completor is to exit the entire implementation, yielding the specified result value.
[PO: all variables and function calls in Expression which are not present in the original specification of the value of the function can be eliminated using information about the state at this point and the result is equivalent to the value of the function in the original specification.]
A state completor comprises the keyword done.
StateCompletor:
done.
State completors are only allowed in state implementations. There is an implicit assertion that the schema or constructor postcondition which is being implemented has been satisfied at the point of a state completor. The effect of a state completor is to exit the implementation.
There is an implicit state completor at the end of any state implementation whose final statement is not discontinuous.
[PO: the required postcondition is satisfied at the point of a state completor.]
Proof lists are used to give hints to the theorem prover about how an assertion or property might be proved. The grammar is:
Proof:
proof ProofList [";"] end.ProofList:
ProofItem *[";" ProofItem];
*[ProofItem ";"] if Guard ProofList *[";" Guard ProofList] [";"] fi.ProofItem:
Assertion;
LetStatement.
A proof list contains a sequence of assertions and temporary name definitions separated by semicolons. The last element in a proof may be a conditional proof.
The theorem prover should attempt to prove the predicate lists in the order in which they are given, using each assertion as an assumption when proving later assertions in the proof list. The prover will attempt to prove the assertion to which the proof list is attached by assuming all assertions in the proof list are satisfied.
Perfect Language Reference Manual, Version 3.0, December 2004.
© 2001-2004 Escher Technologies Limited. All rights reserved.