ClassDeclaration
[deferred | final ] class Identifier [ of FormalTemplateParameters] [RequirePart] "^=" [inherits TypeExpr5 | storable] ClassBody end.ClassBody:
AbstractPart [ InternalPart] [ ConfinedPart] [ InterfacePart];
ConfinedPart [ InterfacePart];
InterfacePart.AbstractPart:
abstract [ AbstractMember *[ ";" AbstractMember] [";"] ].InternalPart:
internal [ InternalMember *[ ";" InternalMember] [";"] ].ConfinedPart:
confined [ ConfinedMember *[ ";" ConfinedMember] [";"] ].InterfacePart:
interface [ InterfaceMember *[ ";" InterfaceMember] [";"] ].AbstractMember:
MemberDeclaration;
ClassInvariant;
HistoryInvariant.InternalMember:
MemberDeclaration;
InternalRedeclaration ;
InternalReimplementation;
ClassInvariant.ConfinedMember:
[define | redefine] MemberFunctionEtcDeclaration ;
DeferredDeclaration;
AbsurdDeclaration;
ConfinedOrInterfaceRedeclaration.InterfaceMember:
ConfinedMember;
[ghost] operator "=" "(" Identifier ")";
[total] operator "~~" "(" Identifier ")" [decrease RecursionVariant] OperatorBody.
MemberDeclaration:
ConstantDeclaration;
ConstructorDeclaration ;
VariableDeclarations ;
HeapDeclaration ;
MemberFunctionEtcDeclaration;
PropertyDeclaration;
AxiomDeclaration;
ClassDeclaration;
TypeDeclaration.ClassInvariant:
invariant PredicateList.HistoryInvariant:
"!" invariant PredicateList [ exempt IdentifierList ].InternalRedeclaration:
function Identifier "^=" Expression .InternalReimplementation:
function Identifier [ "(" FunctionParameterList ")" ] Implementation;
operator RedefinableOp [OperatorParameter] Implementation;
operator OperatorParameter RevRedefinableOp Implementation;
operator "=" "(" Identifier ")" Implementation;
selector SelectorName [ "(" FunctionParameterList ")" ] Implementation;
schema ["!"] Identifier [ "(" SchemaParameterList ")" ] Implementation;
schema "!" RedefinableOp OperatorParameter Implementation ;
build "{" [ConstructorParameterList] "}" Implementation.ConfinedOrInterfaceRedeclaration:
function IdentifierList;
selector IdentifierList.MemberFunctionEtcDeclaration:
[final | early] FunctionEtcDeclaration;
nonmember FunctionDeclaration;
nonmember SchemaDeclaration.FunctionEtcDeclaration:
FunctionDeclaration;
SelectorDeclaration ;
OperatorDeclaration ;
SchemaDeclaration .DeferredDeclaration:
deferred FunctionEtcHeader [pre PredicateList] [decrease Variant] [Assertion].AbsurdDeclaration:
absurd FunctionEtcHeader.FunctionEtcHeader:
FunctionHeader;
SelectorHeader;
OperatorHeader;
SchemaHeader.
The class specification comprises the optional inherit list, abstract, confined and interface member declarations. The internal declarations are implementation detail.
Whenever a function, operator, schema, property or axiom class member is declared, there is an implied "current object" parameter. The definition of the member may refer to unqualified members of the current object, and may also refer to the entire current object using the self keyword. However, if the nonmember modifier is used, the definition is not declaring a member and there is no "current object". Properties and axioms involving more than one value of the class type should normally be declared as nonmembers for clarity.
The optional inherits part specifies a class or class template instantiation whose attributes are to be inherited. It is forbidden to inherit from a final class or instantiation of a final class template.
The abstract member declarations and invariants describe the model of the class as seen by its clients. The list of declarations is prefixed by the keyword abstract. The list may include constant, variable, function, selector, operator, schema, property, axiom, constructor and class declarations (function and schema declarations are not common in this context and are only used as an aid to expressing the interface specification). Implementations are not permitted within abstract function, selector, operator, schema and constructor declarations. Member variables may be made conditional using the when...end construct.
Any invariants in the abstract section specify relationships between abstract members which must be true for any object of the class; it is an implicit part of the postcondition for all constructor and schema members in all sections of the class following the invariant.
The optional internal member declarations describe how the class is implemented. The internal member declarations may include constant, variable, function, selector, operator, schema, property, axiom and class declarations.
Internal members serve the following purposes:
[SC] Within the internal section, abstract variable members of the class may be redeclared as function internal members. In such redeclarations, the usual ": TypeExpression" is omitted since the type has already been specified; no parameters are permitted in the declaration. Redeclaration as a function indicates that the abstract member may be computed from internal variable members according to the function body. The implied precondition of such a function comprises the following elements:
Abstract member redeclarations may not be recursive (i.e. internal members referred to in an abstract member redeclaration may not be described directly or indirectly in terms of that abstract member).
Abstract members which are functions, operators, selectors, schemas or constructors may be reimplemented. In such a reimplementation, no result type, precondition, postcondition, result value or specification variant is given; however, a parameter list is given if required (the parameter names must match the ones in the original declaration).
In a final class, interface and confined functions and operators whose return type is the type of the class may be reimplemented as schemas. The implied specification for the schema is that self has changed to be equal to the result value of the function or operator. These reimplementations may be used for more efficient implementation of postconditions which require this state change.
Any abstract variables which are not redeclared as internal functions are represented directly. If the internal section is absent all abstract variables will be represented directly.
Any invariants in the internal section describe restrictions on the values of the internal members.
[SC: each Identifier within an InternalRedeclaration is the name of an abstract variable member.]
The confined and interface declarations comprise the published interface to the class. A confined or interface declaration may be a function, selector, operator, schema, property, axiom or constructor declaration, or a redeclaration of an abstract variable or constant member.
Confined members are only accessible to derived classes; interface members are available to the public at large.
The specifications of confined and interface members may only refer to abstract members and to other interface and confined members (including inherited confined and interface members). The implementations of confined and interface members may refer to internal members as well.
Redeclaring the name of an abstract variable or constant member as an interface function member makes the member accessible but "read-only" to clients of the class. Such a redeclaration consists of the keyword function and the abstract member name; no type is specified (since the type was given in the abstract member list), no parameters are declared and no body is given (if the abstract member was redeclared as an internal function member, then the body has already been given, otherwise the abstract member is being implemented as a variable member and a body is constructed which just returns its value). If the abstract variable is declared in a when clause, the corresponding guard becomes the implied precondition of the interface function.
Redeclaring the name of an abstract variable member as an interface selector member makes the member completely accessible to clients of the class. Such a redeclaration consists of the keyword selector and the abstract member name; again, no type is specified and there are no parameters or body. The abstract data member concerned may not have been redeclared in the internal section as a function, nor may any class invariant in the current class or any derived class directly or indirectly depend on it. If the abstract variable is declared in a when clause, the corresponding guard becomes the implied precondition of the interface selector.
Redeclaring the name of an abstract variable as a confined function or selector has a similar effect except that accessibility is limited to members of the current class and derived classes.
A class declared in the abstract member declaration section may not be used as the type of a parameter or the result of a confined interface member (because the class declaration is not visible to clients of the class).
The interface section may also include declarations for the rank and equality operators. In a declaration of rank or equality, neither the parameter type or return type are stated (these are always implicitly defined as the type of the class and rank or bool respectively).
Equality is always implicitly defined as equality of the abstract data members; so no result value may be declared in an equality operator declaration. The explicit declaration of an equality operator serves to specify whether equality can actually be evaluated at run-time (i.e. whether equality is ghost).
If equality is declared as a non-ghost operator in some class C, then equality in C and all its descendents is not ghost. Similarly, if equality is declared ghost in class C, then equality in C and all its descendents is ghost.
If a class C contains no equality operator declaration and neither do any of the ancestors of C, then C has non-ghost equality by default. However, decendents of C are still permitted to declare ghost equality. Therefore, equality on objects of type from C is treated as ghost to allow for this possibility. If you require the type from C to have non-ghost equality, then you must declare a non-ghost equality operator explicitly in C or in one of its ancestors.
A rank (i.e. comparison) operator may be declared and defined in any way that, for all values x, y, z of the class in which the rank operator is being defined, satisfies the following properties:
If a rank operator has already been declared in one of the class's parents then it is also required that the new rank operator does not change any of the existing ordering, it merely refines it. If we use ~~c to represent the rank operator in the child class and ~~p to represent the rank operator in the parent class, then the condition to be satisfied is:
Note that the system is at liberty to further refine any user definition of rank that is not already total. In particular, where the user-defined rank would cause objects of different classes to rank same, the system will refine the definition so that this is not the case.
In the absence of an explicit declaration of the rank operator in a class, the system will generate one. The definition may be trivial (e.g. all instances of the class rank same with each other), or more complex; but it is guaranteed to respect any inherited rank operator.
A function, schema or property declaration within the abstract, internal, confined or interface section of a class declarations may be declared nonmember to indicate that the declaration is not a member of the class and does not have the "current object" parameter. Nonmember declarations are not considered to be class members even though they are declared within the body of a class. The nonmember keyword may be not be applied to an operator or selector declaration, neither may it be applied to a method that is declared within an implementation or is declared at file scope.
For each confined or interface nonmember function or schema declared, either the result type (if a function member) or at least one parameter should be of the class type, or a union involving the class type, or a template instantiation involving the class type in its parameters; otherwise the declaration does not belong inside the class definition.
An interface nonmember function or schema may be called from outside the class by following its name with the "@" symbol and the class name, then the parameter list, if any, as in myNonmemberMethod@MyClass(aParameter).
An abstract constant may be redeclared as a nonmember confined or interface function using the same syntax as for the redeclaration of an abstract variable, save that the nonmember keyword must be used.
It is permissible for a class declaration to be recursive, i.e. it may have data members (abstract and/or internal) which involve its own type, provided such recursion is finite. In practice this means that in a declaration of class X it is permissible to declare members of types X || Y (where Y does not refer to X), seq of X, set of X and bag of X (provided an empty collection is permitted), and other types which have conditional members of type X (provided the condition is not always true).
A class invariant is a predicate (i.e. a Boolean expression) declared in the abstract or internal section of a class, whose purpose is to constrain the values of the member variables to combinations for which the invariant yields true. To this end, a class invariant is:
An invariant logically precedes a declaration D if and only if D is declared later in the text than the invariant but within the same abstract or internal section, or D is declared within the confined or interface section of the same class.
A class invariant may not refer to any declaration that it logically precedes; neither may an invariant declared in the abstract section refer to a declaration in the internal section.
A class invariant may not depend on any variable whose value can be accessed (in whole or in part) by means of a call to an interface selector and thereby altered such that the invariant is violated. This restriction ensures that any modification of an object other than self by means of selector access is bound to preserve the invariant.
The only explicit or implicit references to self permitted in a class invariant are references of the form "self.x" where x is the name of a member variable, or one of "self .f (...)", "self op ..." or "... op self" where f or op is the name of a member function or operator whose declaration logically precedes the class invariant or which is inherited from an ancestor class in which it is declared early. This ensures that an invariant cannot be defined in terms of members that assume the invariant is satisfied.
In the abstract section, constructors can only be declared after all invariants in that section. Similarly, if an abstract constructor is re-implemented in the internal section, then that re-implementation must be after any and all invariants have been declared in the internal section.
Multiple comma-separate invariants may be declared following the invariant keyword.
A method or constructor need not respect any invariant that does not logically precede its own declaration. A method or constructor postcondition or body may temporarily break a class invariant that does logically precede the method or constructor declaration, provided that the invariant is satisfied both on completion of the postcondition or body and at the point of every call to a method whose declaration the invariant logically precedes.
Whereas a class invariant places a constraint on the values that the abstract variables of a class may take, a history invariant places constraints on the ways in which the abstract variables may be changed. Declaring a history invariant in a class is equivalent to declaring a corresponding postassertion on every member schema that modifies the current object and is declared textually later than the history invariant.
A history invariant is distinguished from a class invariant by the initial "!" symbol before the keyword invariant. Each expression in a history invariant must refer to at least one instance of self ' or to a primed abstract member variable. Unliike class invariants, history invariants may only appear in the abstract of a class and not in the internal section.
The optional exempt clause lists the names of schemas that are exempted from having to comply with the history invariant. This provides a means to specify that some sorts of changes (i.e. those that do not satisfy a history invariant) may only be made by certain named schemas.
When class inheritance is used, any history invariants declared in a parent class apply not only to schemas declared textually later in the parent class, but also to all modifying schemas declared in any descencent class, apart from schemas whos names appear in the exemption list.
A class or class template declaration is termed storable if it has no inherits part but includes the keyword storable after the "^=" symbol, or if it inherits a storable class. If the declaration for class X is storable, all objects of types X, from X, ref X and ref from X are storable, meaning they may be written to and read from external storage or communication channels.
Within the declaration of a storable class, all variable members of the class (other than abstract variables redeclared as internal functions) must have storable types.
Objects of type X of (A, B...), from X of (A, B ...) and ref X of (A, B...) are storable if and only if the declaration of class template X of (Y, Z ...) is storable and objects of types A, B... are all storable. A united type is storable if and only if all the types in the union are storable. Adding a constraint to a type does not affect its storability.
Predefined types bool, byte, char, int, real and void, and template types seq, set, bag, pair, triple and map are storable, as are all enumeration and tag types.
Constructor declarations provide the means to build values of the class. The syntax is:
ConstructorDeclaration:
[opaque | ghost ] build "{ " [ConstructorParameterList] "}" [ExceptionSpecification] [RequirePart] [pre PredicateList] [decrease Variant] [ConstructorBody] [PostAssertion].ConstructorParameterList:
ConstructorParameters [repeated FunctionParameters];
repeated FunctionParameters.ConstructorParameters:
ConstructorParams *[Separator ConstructorParams].ConstructorParams:
["!"] Identifier *[Separator ["!"] Identifier] ":" TypeExpression;
["!"] Identifier ":" AbbrevTypeExpression.ConstructorBody:
"^=" Expression [Implementation];
inherits Expression;
[inherits Expression] post Postcondition [Implementation ].
The first form of ConstructorBody is used to define the result of a constructor in terms of an expression yielding a value belonging to the class (typically the expression invokes another constructor for the class). The second form defines the result in terms of the value of the parent object (the expression following the inherits keyword) and the values of the abstract variable members (which must be defined in the postcondition).
Where a formal parameter name is prefixed by the symbol "! ", the parameter name must match the name of an abstract data member of the class and the body (if present) must have the " post Postcondition" form (not the "^= Expression" form). The type of the parameter must be equal to, or a subtype of, the type of the abstract data member. Postcondition is implicitly expanded to include the condition that the final value of the abstract data member is equal to the value of the actual parameter. Thus, using the form "!name" in the parameter list is a shorthand for using instead the form "name2" in the parameter list and appending ", name! = name2" to the postcondition which follows post (where "name" is an abstract data member and "name2" is not).
Where the constructor has an implementation, assignments are also added to the start of the implementation for every "! " parameter corresponding to a data member which has not been re-implemented as an internal function. Where the constructor itself appears in the internal section, the same rules apply, but the " !" parameter name must match either an internal data member or an abstract data member which is not re-implemented.
The optional post-assertion specifies additional properties of the returned object that are expected to hold. These properties should be provable from the postcondition or result expression. Within the post-assertion of a constructor declared using "^=" and a result expression, the predefined identifier result refers to the returned object, and each expression in the post-assertion must refer to result. Within the post-assertion of a constructor declared with a postcondition, the returned object is denoted by self ', and each expression in the post-assertion must refer to self ' or to a primed member variable.
[SC] Every abstract class declaration containing member declarations must include at least one constructor declaration that does not use the "^= Expression" form of body (otherwise it would be impossible to construct objects of the class).
[SC] A constructor for a derived class must have a body, using either the "^= Expression " syntax or including an "inherits Expression" part.
[SC] A constructor that does not use the "^= Expression" syntax must define the values of all its data members, except for members declared within a when clause if the corresponding guard is false (if the "^= Expression " syntax is used, all the data members are bound to be defined anyway).
[SC] If the opaque keyword is used, the constructor does not uniquely define the object. Note that if the class includes one or more reference members and the constructor creates new values on the heap for the reference member(s) to address, the object cannot be uniquely defined so this is one instance where opaque must be used.
When an abstract class declaration inherits from another abstract class then all the confined and interface members of that class are inherited by the new class. The abstract and internal members are inherited at an implementation level but are not directly accessible by the inheriting class. Additional abstract, internal, confined and interface members may be declared.
It is not permitted to inherit from a class that was declared final, neither is the type from T permitted if T is a class declared final.
Provided certain restrictions are obeyed, confined and interface function, selector, operator and schema members of the inherited class may be overridden by new declarations. The new declaration must be in the same section (confined or interface) as the old, have the same parameter and result types as the old and must be preceded by the keyword redefine to indicate that the overriding is deliberate. The specification of the overriding declaration must conform to the specification of the overridden declaration as follows:
Declarations that were declared final or early may not be overridden. Overriding declarations may also be declared final or early.
When a class overrides a non-deferred member, the corresponding member in the parent class can be accessed by prefixing its name with the keyword super. It is not permissible to apply more than one super to a member name. If the member being invoked is a schema that modifies the current object, the "!" symbol precedes super.
It sometimes happens that we wish to have a client invoke some operation on a class without understanding the effect of the operation on the class. Typically, the operation will correspond to some real-world action which may vary greatly between objects of different classes derived from a base class. In this situation we may use a base class which includes one or more named and typed but undefined members.
A deferred base class is declared in exactly the same way as a normal non-inheriting abstract class except that the entire declaration is prefixed with deferred and one or more of its interface function, operator, selector or schema member declarations may be a deferred declaration.
No variable, parameter or result may be declared as having a type which is a deferred class. A deferred class name may only appear within an inherits part in an abstract class declaration or after the from keyword in a type expression.
Whenever a class declaration inherits a deferred class without defining all of the deferred members, or has one or more declarations of deferred members, it is itself deferred and its declaration must be preceded by deferred.
Whenever a class member declaration overrides an inherited member declaration that was originally declared deferred and has not already been overridden, the keyword define must be used in place of redefine .
The constructors for a deferred class may only be invoked by the inherits parts of the constructors for classes derived from it.
Constructors for deferred classes may not call any member functions, operators, selectors or schemas on the current object apart from such members that were declared early. Member functions, operators, selectors and schemas that are declared early may not call any other member functions, operators, selectors or schemas unless they too are declared early. The purpose of these rules and the early keyword is to prevent the possibility of calling a deferred member.
Those abstract and internal functions, operators, selectors and schemas which precede one or more invariants are automatically considered early, and in addition are not allowed to call members declared in the current class with fewer following invariants. It is not permitted to apply the early keyword to their declarations.
A class may be declared with one or more template parameters, representing unspecified types that will be instantiated whenever an object of the class is created. By default the only methods available on objects of template type are the rank operator and a ghost equality; the optional RequirePart specifies other methods that should also form part of the interface of any class with which we instantiate the template.
The full grammar for the require part is as follows:
RequirePart
RequireItem *["," RequireItem].RequireItem:
Identifier within TypeExpression;
Identifier has PrototypeList end.PrototypeList:
PrototypeItem *[";" PrototypeItem] [";"].PrototypeItem:
FunctionEtcHeader [ pre PredicateList] [ assert Assertion];
build "{ " [ConstructorParameterList] "}" [pre PredicateList] [assert Assertion];
operator "=" "("Identifier ") ";
total operator "~~" "(" Identifier ") ".
The Identifier in each RequireItem must bind to one of the class's template parameters. The within item specifies a common base class that all types used to instantiate that parameter must inherit from. The has item specifies a list of methods together with preconditions and assertions for the verifier.
The requirements are statically checked whenever the template is instantiated.
Perfect Language Reference Manual, Version 5.0, September 2011.
© 2001-2011 Escher Technologies Limited. All rights reserved.