The Analyser (anl)

Analysis is the first stage of processing necessary for a MACHINE, REFINEMENT or IMPLEMENTATION and is a prerequisite for the application of the POGenerator (pog) -- and hence the Provers, the Animator (anm) and Documentation Tool (dmu).

The POGenerator automatically invokes the Analyser for a construct which has not been analysed. Thus for a newly-introduced MACHINE, REFINEMENT or IMPLEMENTATION only the Editor, Analyser and POGenerator options are available.

The Analyser (anl) is invoked from the Main Environment, and is applicable to all specifications, refinements and implementations not currently analysed.

Analysis comprises three distinct phases: normalisation, syntax-checking and type-checking. The Normaliser produces an internal form -- the analysed form -- for the construct, expanding subordinate constructs where necessary. The SyntaxChecker performs syntactic checks on the construct, and the TypeChecker performs checks for type correctness.

If the Analyser succeeds, an internal form of the construct is created and stored in the directory ANL, and a summary of the type information (in internal form) is placed in a ``Type File'' in the TYP directory, for use by the other tools.

The dependencies between parent and subordinate constructs are built up and recorded by the Analyser. Any record of such a dependency will be removed when the parent or one of its subordinates has been edited such that the mathematical content is changed, and the change committed (by one of the Commit, Close or Remake tools); the parent's analysed form (and all subsequent processing on the construct) will also be lost (although it may be automatically reconstructed using the Remake tool).

If an error is detected during analysis then the MiniRemake option is offered.

A by-product of Analysis is the creation of a hypertext file for the analysed construct, containing links to all subordinate constructs.

Edited Files

If the Analyser is requested for a construct which is being currently edited, and the edited version (i.e. that version in the SRC directory) differs from that of the committed version (in the system CFG directory), three options are offered:

Proceed after committing
Proceed without committing
Show Difference (between the SRC and CFG files)

Accepting the commit option will have the same effect as that described for the Commit tool.

Subordinate Constructs

The Normaliser will need to access the analysed form for all constructs subordinate to that which is being currently analysed. (A construct `A' is dependent on a construct `B' if `A' SEES, USES, INCLUDES, IMPORTS or REFINES `B.' Conversely, `B' is said to be a subordinate construct of `A'.)

If a subordinate construct is configured but not currently analysed, the subordinate construct will first be analysed; this process is recursive.

If a subordinate construct is not configured, the Normaliser will search first in the SLIB directory (taking account of any `dot rename' prefixes), and then the SRC directory; if found, it will first be introduced and then analysed.

If the above search is not successful, the Normaliser will check to see whether the subconstruct is generated from an ENUMERATION; if the appropriate enumeration is configured, it will be generated. If the enumeration is not configured but exists in the SRC directory, it is first committed and the the machine generated.

Type Determination

Each variable (a state variable, a constant, a quantified variable in a predicate or a local variable within an operation) is given a type by the TypeChecker, i.e. the tool determines to which set within a pool of sets the variable belongs. The pool of sets consists of the sets given in the SETS clause and in the formal parameter list, together with all other sets which can be constructed from the given sets by means of the power set operation (POW) and the Cartesian product operation (*).

For example:

if cc is a constant and if CSET is a given set and the PROPERTIES clause contains

cc <: CSET
then cc is given type POW(CSET)
cc = 7
then cc is given type NAT
cc : NAT --> CSET
then cc is given type POW(NAT*CSET)

if ASET is also given and aa and rel are variables and the INVARIANT clause contains

aa <: ASET
then aa is given type POW(ASET)
aa = cc
then bb is given the same type as cc
rel : ASET <-> CSET
then rel is given type POW(ASET*CSET)

if bb is a local variable and bb := 1 is the first statement encountered by the TypeChecker then bb is given type NAT.

An error is reported if a type of a variable cannot be determined.

Type Checking

Given the type of all variables then all formulae in which they occur are checked for type consistency (so in the expression aa=bb, aa and bb must be of the same type). An error is reported if a formulae does not type check, and an explanation is given.

Often the error is due to an inconsistent use of externally defined variables or operations. The Find facility will provide the type of those externally defined variables or operations.

A full on-line help listing is available in the Contents Page Also available in the form of a complete Index. Blogo