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;
TraceStatement;
Label;
Jump;
BlockStatement;
Loop;
ThrowStatement;
TryStatement.
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, ThrowStatement, or a conditional statement each of whose branches ends in a discontinuous statement, or a try-statement whose body and catch-part are both discontinuous. A discontinuous statement may only appear as the last item in an implementation, the last item in a branch of a conditional statement, the last item in a block statement, the last item in a try-block or catch-block, or immediately before a label (because the following statements would otherwise be unreachable).
[SC] The last ImplItem in an implementation of a function, operator or selector 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.]
Throw statements raise or re-raise exceptions:
ThrowStatement:
throw Expression;
throw.
The first form raises a new exception, abandoning the containing implementation list. The second form, which is valid only in the catch-part of a try-statement, re-throws the exception caught in the catch-part.
The exception that is thrown or re-thrown must either be caught in the catch-part of an enclosing try-statement within the containing function, selector, operator, schema or constructor, or else it must be of a type contained in the exception signature of the containing function, selector, operator, schema or constructor. This condition is checked by the Perfect compiler.
Important note: The semantics of throw statements are not fully defined in this edition. In particular, there is currently no requirement or verification condition that class invariants are preserved at the point a throw-statement is executed. Therefore, if throw-statements are used in implementations that mutate objects, then when the exception is caught, object invariants may have been broken. We strongly recommend that you use throw-statements only in contexts where no modifications to the state of any object have been made between the start of the try-statement whose catch list catches the exception, and the throw-statement; except that modifications to objects that have passed out of scope when the catch list is reached are safe. It is expected that critical software will typically not use exceptions.
A try statement executes a contained implementation, catching some or all exceptions that it may throw:
TryStatement:
try ImplList [";"] catch CatchItem *[ ';' CatchItem] [";"] end.CatchItem:
'[' Identifier ':' TypeExpression ']' ':' ImplList.
The implementation list following the try keyword is executed. If that implementation list throws an exception, then control is transferred to the catch list. Each catch item declares a type to be caught, an identifier to name the value of the caught exception (so that it can be used in the following implementation list), and an implementation list to be executed when catching exceptions of that type. The catch item that is executed will be the first one (lexically) whose type is or includes the actual type of the exception that was thrown. At most one catch item will be executed, even if the types declared in the catch items are not disjoint. If the exception was of a type that is not contained in any of the types of the catch items, then it is not caught in that catch list and continues to propagate out of the context surrounding the try statement.
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 7.0, February 2017.
© 2017 Escher Technologies Limited. All rights reserved.