Like traditional programming languages, Perfect provides a rich set of operators for constructing expressions. Perfect operators can be overloaded (i.e. the meaning of the operator depends on the types of its operands). To avoid ambiguity, no conversions between classes are automatically applied to operands, apart from widening conversions where the parameter is declared with a union type (note that from types are unions) and the actual parameter is of a type nested in that union.
However, when binding an occurrence of a function or operator to the correct definition, any operand of a type which is not a complete class will be treated as if it belongs to the complete class. For example, an operand of type nat will be treated as if it were of type int. Likewise, if the type naming is used to give a name to some original type with an added constraint, the operand will be treated as belonging to the original type (unless that type is also a type-naming, in which case this rule is applied recursively). Where necessary, verification conditions are generated to the effect that any constraints on the formal parameters are satisfied (this is the only place where the compiler generates an implicit type narrowing).
The full grammar for expressions is as follows:
Expression:
PrimableExpression;
UnprimableExpression.PrimableExpression:
PrimableExpr8;
PrimableCastExpression.UnprimableExpression:
UnprimableCastExpression;
TypeWideningExpression;
TypeEnquiryExpression;
TypeAssertionExpression;
SubjunctiveExpression;
ChooseExpression;
QuantifiedExpression;
TransformExpression.Expr0:
Expr0 BooleanImplicationOperator Expr1;
Expr1.Expr1:
Expr1 "|" Expr2;
Expr2.Expr2:
Expr2 "&" Expr3;
Expr3.Expr3:
Expr3 ComparisonOperator *[Expr3 ComparisonOperator] CompareExpr;
CompareExpr.CompareExpr:
Expr4 "~~" Expr4;
Expr4 ["~"] [in | like] Expr4;
Expr4.Expr4:
Expr4 AddingOperator Expr5;
Expr5.Expr5:
Expr5 MultiplyingOperator Expr6;
Expr6.Expr6:
Expr6 "^" Expr7;
Expr6 ".." Expr7;
Expr7.Expr7:
UnaryPrefixOperator Expr7;
AllowedOverOperator over Expr7;
TypeOp TypeName;
PrimableExpr8;
UnPrimableExpr8.UnPrimableExpr8:
UnprimableBracketedExpression;
UnPrimableExpr8 "[" Expression "]";
UnPrimableExpr8 "." value;
PrimableExpr8 "'";
UnPrimableExpr8 "." IdentifierOrSuper [ActualParameterList];
ref Expression on Identifier;
ConstructorExpression;
Literal;
"?".PrimableExpr8:
PrimableBracketedExpression;
PrimableExpr8 "[" Expression "]";
PrimableExpr8 "." value;
PrimableExpr8 "." IdentifierOrSuper [ActualParameterList];
GeneralIdentifierOrSuper [ActualParameterList];
self;
result;
it.IdentifierOrSuper:
[super] Identifier.GeneralIdentifierOrSuper:
ClassName Identifier;
IdentifierOrSuper.ActualParameterList:
"(" Expression *[Separator Expression] ")".ConstructorExpression:
ClassName "{ " [Expression *[Separator Expression]] "}".Literal:
IntegerLiteral;
RealLiteral;
StringLiteral;
CharacterLiteral;
BooleanLiteral;
VoidLiteral.BooleanLiteral:
true;
false.VoidLiteral:
null.AllowedOverOperator:
AddingOperator;
MultiplyingOperator;
"^"; "..".BooleanImplicationOperator:
"==>"; "<=="; "<==>".AddingOperator:
"+"; "++"; "-"; "--".MultiplyingOperator:
"*"; "**"; "/"; "%"; "%%"; "#"; "##".UnaryPrefixOperator:
"/"; "%"; "#"; "*"; "+"; "-", "<"; ">"; "^"; "~".
Perfect provides three variations of the concept of function, together with constructors. All share the property of having no side-effects, i.e. they behave like mathematical functions.
A function takes one or more parameters and yields a result (in the case of a class member function, it is permitted for a function to take no parameters). An operator is identical to a function except that it is written as a symbol and takes exactly one or two parameters.
A selector is similar to a function except that it must be a member of a class, its return value must be a sub-object of the current object and a selector expression may appear primed in a postcondition; that is, the selector provides a mechanism to access a sub-object in such a way that it may be modified.
A constructor is used to build objects of a given class. It is a special form of function declared within a class and returning an object of that class.
Definitions of predefined global functions, and of functions, selectors and constructors declared by predefined classes are given in the Library Reference, which is Appendix A of this document.
A function or selector is called by writing its name followed by its parameter list in brackets, if the function has any parameters; if there are no parameters, no brackets are required. Where there is more than one parameter, adjacent parameters are separated using any of the separators ",", "->", "<-" and "<->". The separators used in the actual parameter list must match those given in the formal parameter list (overloading of functions with identical argument types by using different separators is possible). For details of type compatibility of the parameters, and how to match repeated parameter groups, see section 6.11.
As an alternative to being given a name, a selector may be represented by square brackets, in which case it must take a single parameter. In this case it is called by following an expression of the type that the selector is a member of by the parameter enclosed in square brackets.
A constructor for a class is called by following the name of the class (including any template parameters) by a parameter list enclosed in curly brackets "{...}". The curly brackets are always used in a constructor call, even if the parameter list is empty (unlike the parameter list for function and selector calls). As with function and selector calls, a constructor may be declared with repeated parameters, see section 6.11.
Definitions of operators declared by predefined classes are given in the Library Reference, which is Appendix A of this document.
The following unary operator symbols are available.
| Symbol | Typical use | Redefinable? | Comments |
| * | Yes | ||
| / | Yes | ||
| % | Yes | ||
| # | Count | Yes | |
| + | Convert to integer | Yes | |
| - | Negation | Yes | |
| < | Predecessor | Yes | May be represented by ↓ (down-arrow) if the character set allows |
| > | Successor | Yes | May be represented by ↑ (up-arrow) if the character set allows |
| ^ | Yes | ||
| ~ | Logical negation | No |
A unary operator is invoked by prefixing the operand symbol to the parameter.
The following binary operator symbols are available.
| Symbol | Priority | Typical use | Prefix with "~"? | Redefinable? | Comments |
| [ ] | 9 | Indexing | No | Yes | Second operand is placed inside the brackets |
| ^ | 8 | Exponentiation | No | Yes | |
| .. | 8 | Make sequence | No | Yes | Defined automatically for enumeration classes |
| * | 7 | Multiplication | No | Yes | |
| / | 7 | Division | No | Yes | |
| % | 7 | Remainder | No | Yes | |
| # | 7 | Count | No | Yes | |
| ** | 7 | Intersection | No | Yes | |
| %% | 7 | No | Yes | ||
| ## | 7 | Disjoint | No | Yes | |
| + | 6 | Addition | No | Yes | Defined automatically for enumeration classes |
| - | 6 | Difference | No | Yes | |
| ++ | 6 | Union, concatenation | No | Yes | |
| -- | 6 | Set difference | No | Yes | |
| ~~ | 5 | Comparison | No | Yes | Must return type rank and be defined so as to have the correct symmetry and transitivity properties. May be declared total in which case additional restrictions apply. Defined automatically (and total) for all enumeration classes. |
| in | 5 | Inclusion | Yes | Yes | |
| like | 5 | Type equality | Yes | No | Returns true if and only if the exact types of the operands are the same at run-time |
| = | 4 | Equality | Yes | No | |
| < | 4 | Less-than | Yes | No | Defined automatically from the definition of "~~" |
| > | 4 | Greater-than | Yes | No | Equivalent to "<" with operands reversed |
| <= | 4 | Less-than-or-equal | Yes | No | Defined automatically from the definition of "~~" provided that the definition of "~~" is declared total |
| >= | 4 | Greater-then-or-equal | Yes | No | Equivalent to "<=" with operands reversed |
| << | 4 | Strict inclusion | Yes | Yes | |
| >> | 4 | Strict reverse inclusion | Yes | No | Equivalent to "<<" with operands reversed |
| <<= | 4 | Inclusion | Yes | Yes | |
| >>= | 4 | Reverse inclusion | Yes | No | Equivalent to "<<=" with operands reversed |
| & | 3 | Logical 'and' | No | No | "a & b" is equivalent to "([~a]: false, []: b)" |
| | | 2 | Logical 'or' | No | No | "a | b" is equivalent to "([a]: true, []: b)" |
| ==> | 1 | Implication | No | No | "a ==> b" is equivalent to "(~a) | b" |
| <== | 1 | Reverse implication | No | No | "a <== b" is equivalent to "a | ~b" |
| <==> | 1 | Equivalence | No | No | Same as "=" on Booleans but lower priority |
A binary operator is invoked using infix notation; except that when invoking the "[]" operator, the first operand is placed on the left and the second operand is placed within the square brackets.
Where the column "Prefix with ~?" reads "Yes", the operator has a Boolean result and the operator may be prefixed by "~" to yield a similar operator producing the inverse result. For example, "a ~< b" has the same meaning as "~(a < b)".
The comparison operators (i.e. all the operators with priority 4) may share operands in expressions. Such expressions are expanded by duplicating the shared operand(s) and inserting "&" between each comparison. For example, the expression "a < b <= c < d" means the same as "(a < b) & (b <= c) & (c < d)".
The "[]" symbol may also be used to declare a selector.
The equality operator is treated specially in three ways:
The rank operator "~~" defines a partial ordering and is automatically defined by the system for all classes which do not have a user-defined relative rank operator.
Any declaration of the rank operator in some class C must ensure that the following relations hold for all expressions e1, e2 and e3 having type C:
The system also defines the binary operator "<" in terms of the rank operator using the following identity:
Where the rank operator has been defined as total then only equal values may return same@rank, and the system will define the binary operator "<=" using the following identity:
The like operator compares the types of its operands at run-time and returns true if the actual types are the same, otherwise false. Both operands should be of united types (note that a from type expression is a united type), and the types of both operands must have a common subtype (so that a type match is possible).
The relative precedence of operators in many programming languages is difficult to remember, leading to over-use of brackets. With this in mind, the precedence structure of Perfect has been kept simple. Operators are evaluated in the following order:
Unary operators group right-to-left (the only order which makes sense, e.g. "- # x"). All binary operators group left-to-right, except for the comparison operators, for which there is no grouping (because compound operators are formed instead).
When reading Perfect text, it is helpful to have a standard pronunciation of the more unusual operators and member names. Suggested pronunciations are:
| Operator | Suggested pronunciation |
| # | "count" (or optionally "length" for the unary form with a sequence operand) |
| ## | "disjoint" |
| ^ | "to-the-power-of" (or "exp") |
| .. | "up-to" |
| ++ | "join" (optionally "cat" for sequences) |
| -- | "diff" |
| ** | "intersect" |
| > (unary) | "next" or "successor" |
| < (unary) | "previous" or "predecessor" |
| % | "modulo" |
| >> | "contains" |
| >>= | "includes" |
| << | "is contained in" |
| <<= | "is included in" |
| ~~ | "compared with" |
The operators highest and lowest may be applied to char or any enumeration type. Also, lowest may be applied to any tag type, and highest may be applied to any finite tag type. The highest operator yields that value such that there are no greater values in the type. The lowest operator yields that value such that there is no lesser value of that type. The syntax is:
TypeOperatorExpression:
TypeOperator Identifier.TypeOperator:
highest;
lowest.
Bracketed expressions may be used for the following purposes:
The syntax for bracketed expressions is:
PrimableBracketedExpression:
"(" *[LetDeclarationAssertionOrTrace] PrimableExpression ")".UnprimableBracketedExpression:
"(" *[LetDeclarationAssertionOrTrace] PossMultipleExpressionOrChoice ")".LetDeclarationAssertionOrTrace:
let Identifier "^=" Expression ";";
Assertion ";";
TraceStatement ";".Assertion:
assert PredicateList [Proof].TraceStatement:
trace Expression *[Separator Expression];
trace Guard Expression *[Separator Expression].PossMultipleExpressionOrChoice:
PossMultipleExpression;
Choices.PossMultipleExpression:
Expression *["," Expression].Choices:
GuardedExpression *["," GuardedExpression] ["," ElseExpression];
opaque GuardedExpression "," GuardedExpression *["," GuardedExpression].GuardedExpression:
Guard Expression.Guard:
"[" Predicate "]" ":".Predicate:
Expression.ElseExpression:
EmptyGuard Expression.EmptyGuard:
"[" "]" ":".
Identifiers introduced using let are in scope from the declaration until the closing bracket. A let declaration captures the value of the given expression and names that value.
An assertion states a condition which must hold at that point. Every assertion generates a corresponding proof obligation.
A trace statement causes the expressions following the keyword trace and the optional guard to be output in some way. The expressions are output in the order in which they appear. If the guard is present, then the expressions are only output if the guard is true. Expressions of type seq of char are output as-is. The toString member function is called on expressions of other types to convert them to a suitable form.
The data that is output by a trace statement is not considered part of the program output, and is therefore not mentioned in the specification or reasoned about. However, the expressions in a trace statement must be well-formed and the corresponding verification conditions are generated.
Trace output is intended for diagnostic purposes only. A code generator for Perfect may provide an option to ignore trace statements, in order that they may be left in the specification without giving rise to generated code in a production build of the system.
The choice expression replaces the conventional "if" and "case" constructs. To evaluate the expression, the guards are evaluated in the given order, until one is found to be true. The corresponding expression is then selected for evaluation. If none of the guards is true and an else part is present, the else part is selected; if no else part is present, the precondition of the construct is not satisfied.
For example, to compute the maximum of two expressions e1 and e2 we can use:
( [e1 >= e2]: e1, [e2 >= e1]: e2 )
At least one of the guarded expressions must be of a type that matches or contains the types of all the other guarded expressions. The result type of a choice expression is that type.
Normally, the expression following the first guard that evaluates to true is chosen and any following guards are not evaluated. However, if the first guard is preceded by opaque then the semantics are those of nondeterministic choice between those expressions whose guards are true. In this case, no else-part (i.e. empty guard) is allowed.
[PO: if no else-part is present, at least one guard evaluates to true. If opaque was used: each guard can be evaluated; each expression can be evaluated if its guard is true. If opaque was not used: each guard can be evaluated if the preceding guards are false; each expression can be evaluated if its guard is true and the previous guards were false].
A set, bag or sequence can be subjected to a filtering operation using the notation:
ChooseExpression:
ChoiceType Identifier ":" TypeExpr2 ":-" Predicate;
ChoiceType Identifier "::" Expr4 ":-" Predicate;
ThatOrAny Expression.ChoiceType:
that;
any;
those.ThatOrAny:
that ;
any.
The meaning when the any choice type is used is: any value of the specified type or from the specified expression (which must be a set, bag or sequence) such that Predicate is true. There must be at least one such value. The meaning when that is used is similar, except that we are asserting that there is exactly one such value. The result in both cases is a value belonging to the TypeExpr2 or the base type of which the Expr4 is a collection. If the form without ":- Predicate" is used, it is equivalent to the full form with true substituted for Predicate.
The meaning when the those choice type is used is the set, bag or sequence (depending on whether TypeExpr2 or Expr4 is a class or set, a bag or a sequence respectively) comprising those values in TypeExpr2 or Expr4 for which Predicate is true.
A transform takes values from one collection and maps them onto a another collection (possibly of a different type) on an element-by-element basis.
TransformExpression:
for Identifier "::" Expr4 yield Expression;
for those Identifier "::" Expr4 ":-" Predicate yield Expression.
The Expr4 must in either case have a type which is a set, bag or sequence; the result is a set, bag or sequence (respectively) of elements of the type of the Expression. In the second form, only those elements of the Expr4 which satisfy Predicate are chosen. If the Expr4 is a sequence, the result is a sequence whose elements are in the same order as the elements in the Expr4 from which they were generated.
Note that if the first form is used (i.e. without those keyword), then when the operand is a bag or sequence, the result has the same number of elements as the operand; however, if the operand is a set, the result may have fewer elements (because multiple elements in the operand may yield the same result value, and the result is condensed into a set).
A quantified expression has the form:
QuantifiedExpression:
(forall | exists) BoundVariableDeclarations ":-" Predicate.BoundVariableDeclarations:
BoundVariableDecl *["," BoundVariableDecl].BoundVariableDecl:
IdentifierList ":" TypeExpr2;
IdentifierList "::" Expr4.IdentifierList:
Identifier *["," Identifier].
The result type is Boolean. If the form containing ":: " is used, the Expr4 which follows "::" must yield a set, bag or sequence.
When the universal quantifier forall is used the meaning is "For all permitted values of the declared identifiers, Predicate is true". If there are no permitted values (because the type of one of the declared identifiers is an empty set or type), the expression yields true.
When the existential quantifier exists is used the meaning is "There exists a combination of permitted values of the declared identifiers such that Predicate is true".
The two types of quantifier are related in the following manner:
(forall x:t :- p(x)) <==> ~(exists x:t :- ~p(x))
The cast expression is used to assert that some value whose static type is a union (expressed explicitly or using the keyword from) is known to be of a narrower type, and to cast it to that type.
PrimableCastExpression:
PrimableExpr8 is TypeExpression.UnprimableCastExpression:
CompareExpr is TypeExpression.
If a cast expression is used as an operand, it must be enclosed in brackets.
[SC] Type TypeExpression must be a type contained in the type of the PrimableExpr8 or CompareExpr.
[PO] Each use of a cast expression expr is type gives rise to the verification condition expr within type.
The type widening expression is used to treat a value of some class as a value of a union (expressed explicitly or using the keyword from) which includes that class. It may also be used to explicitly remove constraints from a type (e.g. to cast an object of type nat to int).
PrimableCastExpression:
PrimabeExpr8 as TypeExpression.UnprimableCastExpression:
CompareExpr as TypeExpression.
If a type widening expression is used as an operand, it must be enclosed in brackets.
[SC] Type TypeExpression must be a type containing the type of CompareExpr. That is, it must be a union containing the type, or a type with fewer constraints. If the types are identical a warning is generated.
It is possible to enquire whether a value of a union type (including a union type generated using the from keyword) is a member of one of the types from which the union type is formed, or a member of a subset of the union (including a subset expressed using the from keyword). The syntax is:
TypeEnquiry:
CompareExpr ["~"] within TypeExpression.
The result has type bool.
If a type enquiry expression is used as an operand, it must be enclosed in brackets.
Note that the types of two expressions can be compared using the like operator (see section 5.3.5).
The subclass selector is used to assert that a value whose type is a union belongs to a subclass of that union, or that a value known to be derived from some base class type is actually of a particular derived class, and in either case to yield a value of that subclass or derived class. Its main use is to form operands of the correct type for passing to functions and operators. It can also be used to assert that a particular constraint is satisfied by a value.
SubclassExpression:
CompareExpr is TypeExpression.
If a subclass expression is used as an operand, it must be enclosed in brackets.
[SC] In this construct, either Expression has a union type and TypeExpression is a member of that type or a subset of a member or a union of some (but not all) members of that union, or Expression has type "from Classname" and TypeExpression is the name of a class derived from Classname. The compiler will report an error if this condition is not satisfied (i.e. it is statically impossible for Expression to have type TypeExpression at runtime). The compiler will report a warning if the type of Expression is statically the same as TypeExpression.
The subjunctive expression yields the value which an object would have if a schema which modifies it were to be invoked. It does not actually modify the object concerned (a typical implementation might take a copy of the object, modify the copy and yield the modified copy as the result). The syntax is:
SubjunctiveExpression:
CompareExpr after Postcondition.
[SC] Postcondition must be a postcondition which modifies the pronoun it and nothing else.
The subjunctive expression should only be used where the alternative means of specifying the value required are cumbersome. For example, if a variable x is a class with abstract variable members a, b, c .. z and we wish to express a value of the same type whose members all have the same values as the members of x except for a, we might write:
x after it.a! = newa
instead of explicitly stating the values of all the members. Similarly, if y is an object of a class that includes a modifying member schema normalize, we could write:
y after it!normalize
The postcondition following after is permitted only to modify the object denoted by the pronoun it (which is a copy of the expression to the left of after). It may not modify objects addressed through references, since such modifications might affect other objects.
The subjunctive expression provides the sole mechanism for specifying functions in terms of schemas. Subjunctive expressions used as operands must be enclosed in brackets.
The full syntax for postconditions is described in section 6.8.2.
The over expression "op over s", where "s" is a non-empty set, sequence or bag, and "op" is a binary operator whose operand and return types are all equal to the type of the elements of "s", is defined in the case of a sequence as follows:
([#s = 1]: that s, []: (op over s.front) op s.last)
In the case of a set or bag the definition is:
([#s = 1]: that s, []: (let tmp ^= any s; (op over s.remove(tmp)) op tmp))
[SC] The operator must not have any precondition.
[SC] If "s" is a set or bag, the operator must have been declared associative and commutative (see section 6.6.3).
[PO: The collection "s" is non-empty, unless a left identity has been declared for the operator].
The heap expression creates a value on a named heap and yields a reference to that value.
HeapExpression:
ref Expression on Identifier.
Here, Identifier must be the name of a heap. The type of the expression is a reference to the type of Expression.
The value selector UnprimableExpr8 "." value returns the value of an object on a heap. The expression must be of type ref X on H, where X is some type, and H some heap, and returns the object of type X.
When an expression is used as an operand of a function or operator, the only type conversions that may be invoked implicitly are widening conversions from a class to a union which includes that class (which includes converting X to from X, X to from Y, or from X to from Y, where Y is an ancestor of X), and conversions between types which are equal once all constraints have been removed (even if this involves adding new constraints, for example int to nat). Other type conversions must be performed explicitly using constructors, subclass expressions, operators and functions.
To specify the class in which a non-member function or enumeration value is to be found, the name of the function or value may be preceded by the name of the class, with the class name and function or value name separated by white space only (i.e. class-name function-or-value-name). Enumeration values are treated as non-members of the enumeration class, so must be referred to in this way. No scope resolution is required to refer to non-members declared in the current class or one of its ancestors.
Note: older versions of Perfect Developer used the syntax function-or-value-name @ class-name. This syntax is still supported, but deprecated.
This represents an expression whose value 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.
Any expression belongs to one of three categories: writable, limited-writable and non-writable. The category of an expression is relevant within postconditions and implementations. A writable expression (sometimes called an lvalue) may be changed in any way that conforms to its type (for example, it may be re-assigned). A limited-writable expression may only be modified by calling a member schema of the type to which it belongs, and its actual run-time type can never be changed by such an operation. A non-writable expression cannot be written at all.
A writable expression is one of the following:
A limited-writable expression is one of the following:
To "prime an expression" means to place a prime (single quotation mark) after it. Only writable and limited-writable expressions may be primed, and only in contexts where the expression has potentially a final value that differs from its initial value (e.g. postconditions, schema post-assertions, and implementations). In such contexts, a primed expression refers to the final value of that expression; an un-primed equivalent expression refers to the initial value of the expression.
In the context of a multithreaded environment, the term "initial value" is misleading and an unprimed expression is taken instead to refer to "the value the expression would have had if the current thread had not modified it".
Perfect Language Reference Manual, Version 7.0, February 2017.
© 2017 Escher Technologies Limited. All rights reserved.