1. Introduction

1.1 Purpose of this manual

This manual is the definition document for the Perfect Developer Language (Perfect). Newcomers to Perfect should use it in conjunction with a tutorial such as the one to be found on the Escher Technologies Ltd. web site.

1.2 Status of this edition

The syntax and semantics given in this edition of the Perfect Developer Language Reference Manual are intended to be final except for the following areas which need to be completed:

Various items flagged [TBD] are subject to review
Further Static Constraints [SC] and Verification Conditions [PO] need to be documented
Further clarification may be needed in some areas

1.3 Organization

This manual is structured such that each chapter builds upon the syntax described in previous chapters, with minimal need for forward reference.

Notes enclosed in square brackets have various purposes, as follows:

[TBD] - indicates an area of the language design subject to review.

[SC] - indicates a static constraint which the compiler must check; it must report an error if the condition is not satisfied.

[PO] - indicates a verification condition (or proof obligation) which must be generated by the compiler and passed to the theorem prover for proving.

[IMP] - implementation note.

1.4 Syntax used to describe the grammar of Perfect

Character sequences appearing in bold are keywords of the language and represent themselves.

Character sequences appearing in italics represent nonterminal symbols of the language.

Strings of one or more punctuation characters within double quotes represent themselves.

Where a construct appears within square brackets, the construct is optional. If the opening square bracket is preceded by an asterisk, the construct may appear zero or more times in sequence at that point.

Two or more constructs separated by a vertical bar indicates that the constructs are alternatives. Round brackets may be used to delimit the scope of the vertical bar.

The colon separates the left hand side of a production from the right hand side. The semicolon separates multiple alternate right-hand sides from each other (i.e. it is similar to a vertical bar but has a lower precedence).

Comments in the grammar are introduced by a hyphen and terminated by end-of-line.

For example, the lexical form of a Perfect identifier can be described as:

Identifier :
(letter | "_") *[letter | digit | "_" ].