There are several sorts of declaration in Perfect:
Declaration:
ConstantDeclaration;
VariableDeclarations;
HeapDeclaration;
FunctionDeclaration;
SelectorDeclaration;
OperatorDeclaration;
SchemaDeclaration;
PropertyDeclaration;
AxiomDeclaration;
ClassDeclaration;
TypeDeclaration.
Class and type declarations were covered in Chapter 4. This chapter describes the remaining types of declaration.
Constants are declared using the syntax:
ConstantDeclaration:
[ghost] const ConstDeclItem *["," ConstDeclItem].
ConstDeclItem:
Identifier [":" TypeExpression] "^=" Expression [NvImplementation].
The TypeExpression and preceding colon are optional if the Expression is a literal, constructor expression, Boolean operator expression, quantified expression, type-widening expression or subclass expression; otherwise it is mandatory. If a TypeExpression is given, the type of the Expression will be widened to match it, if necessary.
If the optional ghost keyword is present, no code will be generated for the constants, and they may only be used in 'ghost' contexts (i.e. preconditions, assertions, invariants, variants and implemented specifications). The optional implementation tells the system how to calculate the value of the constant. Implementations are covered in chapter 8.
Heaps are declared as follows:
HeapDeclaration:
heap Identifier *["," Identifier].
A heap may be used to hold values of any number of types.
A heap declaration is visible wherever a class declaration at the same place would be visible.
Variables are declared using the following syntax:
VariableDeclarations:
var DataDeclarationList.DataDeclarationList:
DataDeclarations *["," DataDeclarations].DataDeclarations:
Identifier *["," Identifier] ":" PossConstrainedTypeExpression;
Identifier ":" AbbrevTypeExpression;
when Guard DataDeclarationList *["," Guard DataDeclarationList] end.
AbbrevTypeExpression:
those TypeExpression ":-" Predicate.
The abbreviated form of type expression avoids the need to introduce a new bound variable name, since the name of the single variable being declared can fulfil this function.
The when...end form is only permitted within the abstract or internal section of an abstract class declaration, and allows the presence of one or more variables to be made conditional on the value of other member variables. The Predicate within each Guard must be a function of variable members only, and may not contain calls to member functions of the class being declared.
[TBD: we could require all the guards within a when clause to be mutually exclusive, then it might be sensible to allow an "else" part as well. This would avoid a proliferation of styles and might improve readability since conditional declarations which were unrelated would have to be in different when clauses. However, there are other cases when it might be reasonable to have overlapping guards, e.g. "when [x=c]: decls, [x=d]: decls, [x=c | x=d]: decls end".]
[Semantic note: declaring a variable v of type T within when...end is similar but not equivalent to declaring v unconditionally with type "T || void", adding a class invariant that "v = null" whenever the corresponding guard is not satisfied, and replacing all non-assigning occurrences of v by "(v is T)". Declaring the data as guarded implies a stronger condition, since the data must be initialised whenever a postcondition modifies the guard so that it becomes true, even on intermediate instances of self, which we allow not to satisfy the class invariant. It is also legal to guard data which is of a type including void, whereas the previous construction makes no sense in this case.]
Like traditional programming languages, Perfect allows functions to be defined; however, Perfect functions are pure in that they have no side-effects. The Perfect notion of a schema corresponds to a function with side-effects in other languages.
A non-opaque function must either be a member of a class, or take at least one parameter. A constant declaration (see section 6.2) should be used instead of declaring a deterministic function with no parameters.
FunctionDeclaration:
FunctionHeader [ExceptionSpecification] [RequirePart] [pre PredicateList] [decrease RecursionVariant] FunctionBody [PostAssertion].FunctionHeader:
[opaque | ghost] function Identifier ["(" FunctionParameterList ")"] FunctionType.FunctionBody:
"^=" PossMultipleExpression [Implementation];
satisfy PredicateList [Implementation].PostAssertion:
assert "..." ["," PredicateList] [Proof];
Assertion.FunctionParameterList:
FunctionParameters [Separator repeated FunctionParameters];
repeated FunctionParameters.FunctionParameters:
FunctionParams *[Separator FunctionParams].FunctionParams:
Identifier *[Separator Identifier] ":" ParameterType.ParameterType:
class Identifier;
TypeExpression.FunctionType:
":" TypeExpression;
FunctionTypeList *["," FunctionTypeList].FunctionTypeList:
Identifier *["," Identifier] ":" TypeExpression.PredicateList:
Predicate *["," Predicate].RecursionVariant:
"..." ["," Variant];
Variant.Variant:
Expression *["," Expression].ExceptionSpecification:
throw TypeExpression.
The parameter list comprises declarations of formal parameters, with parameters being separated by any of the four separators ("," and the three forms of arrow). The keyword repeated indicates that the remaining formal parameters may be matched by one or more matching sequences of actual parameters. If there is more than one repeated formal parameter, the separators between the repeated formal parameters may not include comma (this rule is imposed for clarity since comma is used to separate multiple sequences of actual parameters matching the repeated parameters). Within the function declaration, the type of each repeated formal parameter is "seq of X" where X is the declared type of the parameter.
The function result type may be declared as either a simple type or a list of simple identifier declarations (similar to the declarations which may follow the keyword var). The second form is used for functions which return more than one value; the effect is to declare an anonymous class with the declared identifiers as data members. If this form is used for the declaration of a member function, the identifiers declared must be distinct from all the class member names (including the names of inherited members).
The precondition, if present, comprises the keyword pre followed by a comma-separated list of predicates. The predicates describe conditions (normally functions of the parameters and/or current class members) which must all be true whenever the function is evaluated (i.e. all the predicates in the list are combined with the logical "&" operator, and the resulting expression must yield true). If no precondition part is given, true is assumed (i.e. the function will succeed for all values of its input parameters). The precondition must be well-defined for all values of the parameters (i.e. the precondition for evaluating the precondition is true).
A variant part is only needed by recursive functions and serves to guarantee termination. It comprises the keyword decrease followed by a list of expressions, each of which is of type int, bool, char or an enumeration. If just one expression is given, this expression is guaranteed to decrease on every recursion but never to become negative. If more than one variant expression is given, it is required that those expressions having type int are non-negative and that on each recursion either the first expression decreases, or the first expression remains constant and the variant consisting of the remaining expressions decreases according to the same rule. A boolean variant expression is considered to decrease if its values changes from true to false. The variant must be well-defined and its integral components non-negative whenever the function precondition is satisfied.
The form of variant beginning "..." means that the subsequent variant terms should be appended to an inherited variant. This form may only be used when overriding an inherited method with a variant, and in this case it is compulsory.
The function body defines the result of the function. If the function result is defined by the "^= " symbol and a list of expressions, these expressions must be well-defined whenever the function precondition is satisfied, and the number and types of the expressions must match the declared return types. Alternatively, the function result may be defined using the keyword satisfy followed by a predicate list in which each predicate expresses a condition on the predefined identifier result.
The optional post-assertion specifies any additional properties of the function result that are expected to hold. These properties should be provable from the function definition. Within the post-assertion, the predefined identifier result refers to the result of the function. Each expression in the post-assertion must refer to result. The "... ," form of post-assertion may be used when the function overrides an inherited function that already has a post-assertion; in this case the total post-assertion is the post-assertion of the overridden function followed by the new post-assertion.
The optional implementation part tells the system on how best to implement the function. Implementations are covered in Chapter 8.
The exception specification declares that any exceptions thrown by the function are within the declared type. This type may be a union type, allowing exceptions conforming to any member type of the union to be thrown. If no exception specification is given, then the function does not throw any exceptions.
Within all expressions in a member function declaration, members of the current class may be used unqualified (they are implicitly prefixed by "self").
If the opaque keyword is given, the function is nondeterministic (i.e. two different calls to the same function with correspondingly equal parameters may yield results which are not equal to each other); otherwise the result must be precisely defined. Note that if the result includes a reference to a newly-constructed expression on a heap, this guarantees that the function is nondeterministic, therefore the opaque keyword must be used in this case.
The ghost keyword indicates that the function is used only in preconditions, class invariants, assertions, variants, and in the result expressions and postconditions of a method or constructor for which an implementation is given. It is therefore not necessary for the compiler to generate code for the function (unless run-time checks are being generated).
[SC] The names of the parameters, the names of the returned values (if the multiple-returned-value form is used) and (for a declaration of a member or nonmember function within a class) the names of accessible members of the current class must all be distinct, in order to avoid ambiguity.
[PO: the precondition does not directly or indirectly refer to the function recursively; the precondition can always be evaluated (i.e. its precondition is true); the variant and the function value can be evaluated whenever the precondition is true; if the function result specification is directly or indirectly recursive, the variant decreases on each recursion].
In parameter declarations, instead of following the colon by an actual type, it may be followed by the construct "class Identifier" to denote a class parameter. The same identifier may subsequently be used within the parameter list, result type or function body as a type name (without the class prefix).
This mechanism allows the construction of a polymorphic function (one which supports many operand types). Any member methods of the unspecified class that are used by the function specification or body must be declared in the optional require part (see section 7.4 for the grammar for RequirePart). The presence of these members will be checked when the function is invoked.
It is permissible to have multiple class parameters in a parameter list.
Polymorphic type names cannot occur within unions or after from. This restriction is imposed to guarantee that instantiation of polymorphic type names according to the actual parameter types is always unambiguous.
When the same polymorphic type name occurs more than once in a formal parameter list, the types in the corresponding actual parameter list of the call must be equivalent. This requirement is captured by the rules (n1-n4) in the formal definition of nesting. For example, if a function is declared with the signature "f(e: class X, s: seq of X)" then the call "f(p, q)" where "p" has type "a || int" and "q" has type "seq of int" is invalid: the types of the actual parameters can not be nested in the types of the formal parameters simultaneously.
Whenever a polymorphic function is declared, an additional condition is implicitly appended to the precondition; namely, that all methods declared in the require part must be declared for the actual operand types at the point of call, and their preconditions must be satisfied whenever the function precondition is satisfied.
A function is invoked in the conventional way using its name followed by a list of actual parameters in round brackets. Where there are no operands, no brackets are used.
Where a function returns more than one result, the function call may either be followed by "." and the name of a member of the result (in order to select just one part of the result), or the entire result object may be captured in a let declaration.
[PO: the function precondition (extended to cover operator definitions in the case of polymorphic functions) is satisfied at the point of invocation.]
Perfect also allows many of its own operator symbols to be redefined for user-defined classes. Operators are declared in a similar way as functions except that "function identifier" is replaced by "operator symbol". Operators may not have multiple result values (except by explicitly declaring a class having the required members) and must be class members. Polymorphic operators may be declared.
The unary operator symbols that may be defined are: # + - < >
The binary operator symbols that may be defined are: ^ ** ++ -- # + - * / % << <<= in [] ..
The binary operator symbols that may be re-implemented (see section 7.1.5) but not redefined are: = < <=
OperatorDeclaration:
OperatorHeader [ExceptionSpecification] [RequirePart] *[OperatorProperty] [pre PredicateList] [decrease RecursionVariant] OperatorBody [PostAssertion].OperatorHeader:
[opaque | ghost] operator UnaryRedefinableOp ":" TypeExpression;
[opaque | ghost] operator BinaryRedefinableOp OperatorParameter ":" TypeExpression;
[opaque | ghost] operator OperatorParameter RevRedefinableOp ":" TypeExpression.OperatorBody:
"^=" Expression [Implementation];
satisfy PredicateList [Implementation].OperatorParameter:
"(" Identifier ":" ParameterType ")".UnaryRedefinableOp:
"<"; ">";
" +"; "-"; "*"; "/"; "%"; "#"
"^".BinaryRedefinableOp:
"[" "]";
RevRedefinableOp.RevRedefinableOp:
"<"; "<="; "<< "; "<<=";
">";
"in";
" +"; "-"; "++"; "--";
"*"; "/"; "**"; "%"; "%%"; "#" "##";
".."; "^".OperatorProperty:
associative;
commutative;
idempotent;
identity Expression.
All operators must be declared as members, and there must be the correct number of parameters (zero or one) for the operator symbol being defined (i.e. one less than the arity of the operator). If a parameter is declared, it may be declared either before the operator keyword (in which case the current object will take the place of the right operand), or after the operator symbol (in which case the current object will take the place of the left operand).
When declaring comparison operators, additional properties normally associated with the operator symbol being used must be satisfied, as follows:
When declaring the comparison operator "~~", a special form of operator declaration is used where the parameter type and return type are not specified (they are automatically the type of the current class and rank respectively), there may not be any preconditions, and the specification must satisfy the properties for "~~" detailed in section 7.1.7.
Where a binary operator is declared with no precondition, the operator may be declared any or all of associative, commutative and idempotent; in addition, a left identity expression can be declared (i.e. an expression E such that E op X = X for all expressions X). Verification conditions will be generated to verify that the stated properties hold.
Selectors may only be declared as members of abstract classes (see Chapter 7) but selector declarations will be described here due to their similarity with function and operator declarations.
A selector declaration has similar syntax to a function declaration, except that the function keyword is replaced by selector, the selector name may either be an identifier or the "[]" symbol, the result type may not be a declaration list, and the result must be defined by "^=" and a writable or limited writable expression. The grammar is:
SelectorDeclaration:
SelectorHeader [ExceptionSpecification] [RequirePart] [pre PredicateList] [decrease RecursionVariant] "^=" Expression [Implementation] [PostAssertion].SelectorHeader:
[opaque | ghost] selector SelectorName ["(" FunctionParameterList ")"] ":" [limited] TypeExpression.SelectorName:
Identifier;
"[" "]".
The purpose of a selector is to identify a sub-part of the current object. Unlike a function, the result of a selector can be modified.
If the selector result type is declared limited, the access provided does not allow clients to reassign the result (but does allow member schemas and further selectors to be invoked on the result) and the result expression that follows "^=" must be writable or limited writable.
If the selector is not declared limited, clients may use the selector to re-assign the returned sub-object (and in doing so, to change its actual type, if its declared type is a union). The result expression that follows "^=" must be writable.
A classic example of a selector is the indexing operator "[]" on sequences.
A schema is a description of a change of state (with optional implementation detail). Schemas correspond to procedures in conventional programming languages. Every schema has a defined postcondition; schemas may also have parameters, preconditions, variants and implementations. The syntax is:
SchemaDeclaration:
SchemaHeader [ExceptionSpecification] [RequirePart] [pre PredicateList] [decrease RecursionVariant] post Postcondition [Implementation] [PostAssertion].SchemaHeader:
[opaque | ghost] schema ["!"] Identifier ["(" SchemaParameterList ")"].SchemaParameterList:
SchemaParameters [Separator repeated SchemaParameters];
repeated SchemaParameters.SchemaParameters:
SchemaParams *[Separator SchemaParams].SchemaParams:
SchemaParamIdentifier *[Separator SchemaParamIdentifier]
":" [limited | out] ParameterType.SchemaParamIdentifier:
Identifier;
Identifier "!".
The "!" symbol before the schema name may only appear in class member schemas; it indicates that the schema modifies the current object. The parameter list is similar to a function parameter list except that the names of the parameters may each be followed by an exclamation mark, and the parameter types may be preceded by the keywords limited and out. An exclamation mark indicates that the actual parameter may be modified by the schema. Parameters declared after repeated may not be decorated.
The optional keywords limited and out before the parameter type may only be used when all the parameters to which they apply are decorated with "!". The keyword out indicates that the parameter's initial value is of no interest to the schema. The keyword limited indicates that the parameter is to be limited writable (instead of fully writable), i.e. the schema is not permitted to reassign the parameter (and may therefore not change its actual type, if it is a union).
Polymorphic parameters are permitted in the same way as for functions and lead to the same implicit additional precondition.
The precondition and variant parts are exactly as already described for functions.
The postcondition (post part) describes one or more conditions that must be satisfied after execution of the schema. As with the precondition, a list of postconditions may be given; all must be satisfied. Postconditions are described in more detail in the following section.
Within the schema declaration, parameters which were listed in the parameter list without the keyword out may be referred to unprimed (but need not be referred to at all). Parameters which were listed with an exclamation mark may appear primed within the postcondition list. Parameters which were declared as out must be assigned by the postcondition.
A schema which is not a class member may only modify parameters which appear followed by "!". A schema which is a class member may be declared with the "!" symbol before the schema name, in which case it may modify members of the current object as well.
A schema post-assertion specifies additional conditions that are expected to hold when the schema completes. These conditions should be provable from the postcondition. Each expression in the post-assertion must refer to at least one primed entity (i.e. a primed instance of a modified parameter, or a primed member variable or primed self if it is a member schema that modifies the current object). As with function post-assertions, a schema post-assertion may start with "... ," to indicate that this post-assertion adds to rather then overrrides the post-assertion of the overridden inherited schema.
[SC] If the opaque keyword is used, the schema is nondeterministic (i.e. the postcondition does not uniquely determine the final state, in consequence multiple calls with the same parameters may give rise to different states); otherwise it is deterministic.
[SC] The nonmember keyword indicates that the schema is not a member of the class and does not have the "current object" parameter. It is only valid within in a class declaration.
[SC] A variant is specified if the postcondition refers to the schema under definition, i.e. if the schema specification is recursive.
[PO: the precondition can always be evaluated (i.e. its precondition is true); the postcondition can be evaluated whenever the precondition is true; if the postcondition is directly or indirectly recursive, the variant decreases on each recursion; the variant can never be negative.]
The full grammar for postconditions is as follows:
Postcondition:
change ExpressionList satisfy PredicateList;
PostconditionList;
"?".PostconditionList:
PostconditionElement *["," PostconditionElement].PostconditionElement:
forall BoundVariableDeclarations ":-" PostconditionElement;
Postcondition0.Postcondition0:
Postcondition0 then Postcondition1;
Postcondition1.Postcondition1:
Postcondition1 "&" Postcondition2;
Postcondition2.Postcondition2:
PrimableExpr8 "!" "=" Expression;
PrimableExpr8 "!" AssignableOp Expression;
"(" *[LetDeclarationVariableDeclarationsAssertionOrTrace] PostconditionOrChoices ")";
SchemaCall;
pass.AssignableOp:
BooleanImplicationOperator;
"&"; "|";
AddingOperator;
MultiplyingOperator;
"^"; "..".LetDeclarationVariableDeclarationsAssertionOtTrace:
LetDeclarationAssertionOrTrace;
VariableDeclarations ";".PostconditionOrChoices:
PostconditionList;
Guard Postcondition *["," Guard Postcondition] ["," LastChoice];
opaque Guard Postcondition "," Guard Postcondition *["," Guard Postcondition].LastChoice:
EmptyGuard Postcondition;
"[" "]".SchemaCall:
[PrimableExpr8] "!" IdentifierOrSuper [SchemaActualParameterList];
PrimableExpr8 "." IdentifierOrSuper SchemaActualParameterList;
IdentifierOrSuper SchemaActualParameterList.SchemaActualParameterList:
"(" SchemaActualParameter *[Separator SchemaActualParameter] ")".SchemaActualParameter:
PrimableExpr8 "!";
Expression.
In this form of postcondition, a list of expressions to be changed and a list of predicates to be satisfied is given. Each expression in the list must be a primable expression (but should not be primed in the list). The code generator will attempt to modify the specified variables to achieve the desired conditions.
Although this is the most general form of postcondition, it has two disadvantages; it is verbose (because subexpressions whose values change may have to be written twice - once in the expression list and once in the predicate) - and the code generator may not be able satisfy the predicate, in which case an implementation will have to be provided.
This form allows two postconditions to be joined in a strictly sequential manner. In each of the two component postconditions, a primed subexpression refers to the final value after execution of that postcondition (which, for the first postcondition, is not necessarily the final value after execution of the complete compound postcondition), and an unprimed subexpression refers to the value before execution of that postcondition (which, for the second postcondition, is not necessarily the same as the value before execution of the complete compound postcondition).
A then-postcondition may not appear in a postcondition list containing more than one postcondition, nor may it be combined with another postcondition using "&".
This form allows two postconditions to be joined in a parallel manner. This form is only valid if the sets of subexpressions modified in each of the component postconditions do not overlap. So if the component postconditions can be represented by "change exprlist1 satisfy cond1" and "change exprlist2 satisfy cond1" respectively, the combination is equivalent to "change exprlist1, exprlist2 satisfy cond1 & cond2".
The individual postconditions conjoined by "&" may not be or contain the then-form of postcondition.
The "x! = y" form of postcondition assigns the value of y to x. It is equivalent to the postcondition "change x satisfy x' = y".
The form "x! AssignableOp y" is shorthand for "x! = x AssignableOp y". The operator must be a binary operator accepting parameters of the types of x and y and returning a value of the type of x (exactly as if the full version had been used). Using this form also serves as a hint to the code generator that if possible the condition should be satisfied without copying x.
The bracketed form parallels the syntax and semantics of bracketed expressions: let declarations can be used to define temporary values (whose names are in scope until the closing bracket), assertions may be introduced, and in schema postconditions (but not in postconditions attached to constructors or after expressions) new temporary variables may be declared. Finally, either a single postcondition, a comma-separated list of postconditions, or a guarded list of postconditions may be provided.
If a guarded list is provided, at least one guard must be satisfied (unless an empty guard is provided); the guards are evaluated in the given order, and the postconditions of the first guard found to be true will be selected for execution, defaulting to the postcondition with the empty guard if no guard is satisfied. If the empty guard is of the form with no postcondition then no action is taken if no guard is satisfied. There is no restriction on the relationships between the sets of subexpressions modified by the postconditions.
If the guarded list is preceded by opaque, then the semantics is that of nondeterministic choice between those postconditions whose guards are true. No empty guard is permitted in this case.
The form "SchemaCall" indicates that the designated schema should be invoked with the parameters supplied.
The name of the schema to be invoked is followed by a parameter list in brackets (see the grammar for Expression). Each actual parameter in the brackets must be followed an exclamation mark if the corresponding formal parameter was in the declaration (this makes it possible to tell at the point of schema invocation which parameters are modified, but it is not possible to tell without reference to the original declaration if a modified parameter is read or not). When invoking a schema which has no parameters, the brackets which would have enclosed the actual parameters are omitted.
When invoking a schema which is a class member, the schema member name must follow an expression yielding an object of the class concerned and be separated from that expression by an exclamation mark if the schema modifies the object, or a period otherwise (therefore it is possible to tell at the point of schema invocation whether the current object is modified). If exclamation mark is used to separate the expression from the member name, the expression must be writable or limited writable.
Within the declaration of the class concerned, a member schema name may appear without a preceding expression, in which case the current object is understood, but if the schema modifies the object, a leading exclamation mark is required and the current object must be writable or limited writable.
In the case of a formal parameter which is decorated by "!", the corresponding actual parameter must be writable (limited writable will suffice if the formal parameter's type is declared limited).
Where the current class declares a schema that overrides an inherited schema, the overridden schema can be accessed by prefixing its name with the keyword super. If the circumstances require the schema name to be preceded by an exclamation mark or a period, then the exclamation mark or period must be placed just before the super keyword.
For the purposes of applying the rules concerning the combining of postconditions using "&", a schema call is assumed to modify all parts of any subexpressions that appear followed by "!" in its parameter list; and if the schema name is preceded by "!", the entire expression preceding "!" if there is one, otherwise the entire current object. This means that schema calls that modify an object can only be combined with other postconditions that modify the same object using "then".
[PO: The schema precondition is satisfied.]
Where a member function of a class has a return type that is the same as the type of self for that function, it is permitted to call that function as if it were a schema that modifies the self-operand. If foo(...) is such a function, then the call v!foo(parameters) is equivalent to v! = v.foo(parameters).
The internal-section of the class may also declare a reimplementation of the schema version of foo, in which case the reimplementation will be used when foo is called like a schema. The implementation may or may not call the reimplementation-as-schema (instead of the original function) when the form v! = v.foo(...) is used.
The form "forall BoundVariableDeclaration :- Postcondition" instantiates and satisfies Postcondition for every value of the bound variable in the bound. The instantiations are considered to be executed in parallel. The subexpressions changed by each instantiation must be distinct.
[PO: For any value of the bound variable in the bound, the postcondition is well defined. For distinct values of the bound variable the postconditions produced are independent. If the bound is a sequence or bag, the elements are distinct.]
[TBD: The uniqueness condition above is not necessary - a weaker sufficient condition is that for any element appearing more than once in the collection, the postcondition does nothing. However, in this case the postcondition can be rewritten as 'forall x::those y:: ...', so we use the simpler, stronger condition. A shorthand for writing this form of postcondition may be added at a later date.]
The postcondition pass can be trivially satisfied by doing nothing.
This form indicates that the postcondition has deliberately not been specified yet. Typically, it may be used in skeletal source files that do not yet need to be compiled but need to be included in other Perfect source files.
[TBD: whether to insist that postconditions are deterministic unless they are specifically written in a nondeterministic manner using the any keyword.]
Properties come in two forms: with and without postconditions. A property without a postcondition is essentially an assertion with optional parameters and, in the case of a member property, an implied current object. A property with a postcondition describes conditions that are expected to hold after the postcondition is satisfied. Typically, the postcondition will comprise one or more schema calls.
Properties serve to verify that the system will satisfy its requirements, and to give hints to the verifier for proving verification conditions (including other properties).
Properties are declared using the syntax:
PropertyDeclaration:
[nonmember] property [Identifier] ["(" FunctionParameterList ")"] [pre PredicateList] Assertion;
[nonmember | "!"] property [Identifier] ["(" SchemaParameterList ")"] [pre PredicateList] post Postcondition PostAssertion.
A property declaration without a postcondition is like a ghost function with no result, such that if it is called in a state satisfying the precondition and all applicable class invariants, all the expressions in the assertion should yield true. Mathematically, a property declaration can be turned into a traditional theorem by universally quantifying over each parameter (together with self, if it is a member property), and putting an implication operator between the precondition and the assertion.
A property declaration with a postcondition is like a ghost schema, although it cannot be called (even though it may be given a name), and it is not required to honour history invariants. Just as in the case of a real schema with a postassertion, if it is called in a state satisfying the precondition, then the postassertion should be true. If a member property declaration is prefixed with "!" then the postconditon may modify the current object; otherwise it may not.
The proof list is a hint to the theorem prover, needed if the property is valid but the prover is unable to prove it unaided.
Polymorphic properties are permitted. Property declarations may be overloaded in the same way as function declarations.
Member properties are inherited by derived classes, however they may not be deferred or redefined.
[SC] The nonmember keyword indicates that the property is not a member of the class and does not have the "current object" parameter. It is only valid within in a class declaration.
[SC] Neither the precondition nor the assertion list may directly or indirectly refer to the property.]
[PO: the precondition can always be evaluated; the assertion is satisfied whenever the precondition is satisfied and all the parameters and self (if applicable) satisfy the class invariants for their types.]
An axiom is similar to a property except that it asserts a truth which it is not possible for the theorem prover to prove but which is nevertheless to be assumed true. An axiom declaration has the syntax:
AxiomDeclaration:
[nonmember] axiom [Identifier] ["(" FunctionParameterList ")"] [pre PredicateList] assert PredicateList.
[SC] The nonmember keyword indicates that the axiom is not a member of the class and does not have the "current object" parameter. It is only valid within in a class declaration.
[PO: The precondition can always be evaluated; the predicate list which follows assert can be evaluated whenever the precondition is satisfied.]
This section makes use of the relations "same" and "nested" defined in section 4.15. Type constraints take no part in determining type compatibility but do give rise to additional proof obligations. The exception to this is where a constrained type is used to instantiate a templated type, in which case the constraints must be identical for the types to match.
An expression used as an actual parameter is type-compatible with a corresponding undecorated formal parameter if the expression type is nested within the formal parameter type.
An expression used as an actual parameter is type-compatible with a corresponding formal parameter decorated with "!" if the expression type is the same as the formal parameter type, or the expression type is nested within the formal parameter type and the formal parameter type is declared limited..
Where the formal parameter list includes the keyword repeated then the formal parameters that follow may be matched by one or more comma-separated groups of actual parameters, each of which must match all of those formal parameters and the intervening separators. For example, the formal parameter list:
(a: bool, repeated b: int -> string)
could be matched by either of:
(true, 1 -> "one")
(false, 1 -> "one", 2 -> "two")
but not by either of:
(true)
(false, 1 -> "one", 2)
(the first violates the requirement to match the repeated group at least once, the second violates the requirement to match the entire repeated group a whole number of times).
A result expression in a function or operator declaration, or in a selector declaration with a return type declared limited, is type-compatible with the declared result type if the expression type is nested within the declared result type.
A result expression in a selector declaration with a return type not declared limited is type-compatible with the declared result type if the expression type is the same as the declared result type.
Overloading the same name or operator symbol is permissible provided it is not possible to construct a call that could match more than one declaration, regardless of whether such a call actually occurs in the program. "Could" means that we assume all undefined type relations are actually true (see section 4.15.2 for the definition of when type relations are undefined). For example, functions identical except for operands of types "seq of nat" and "seq of int" would not be permitted, since an operand of either type has an undefined match with the other.
Matching a call to a declaration considers only the number of parameters, the separators and the type compatibility rules; no account is taken of the decoration and writability of actual parameters or any constraints in the types of formal parameter.
A Perfect module comprises an import list followed by a sequence of declarations:
Module:
*[ImportList] DeclarationList [";"].ImportList:
import NonEmptyStringLiteral *["," NonEmptyStringLiteral] ";".DeclarationList:
Declaration *[";" Declaration].
The import list identifies other Perfect modules containing declarations referred to in the current module. Each NonEmptyStringLiteral names a file containing such a module.
[TBD: define precise rules for the search path for imported modules],
The declaration list for a module cannot include variable declarations (i.e. there are no global variables). The purpose of this restriction is to ensure that functions cannot depend on anything other than their parameters and the current object, and that schemas cannot modify anything not flagged as modifiable in their signatures.
Perfect Language Reference Manual, Version 7.0, February 2017.
© 2017 Escher Technologies Limited. All rights reserved.