Status (sts)

This option is invoked from the Main Environment and is applicable to all machines, refinements and implementations.

It allows the user to determine the current state of a construct under configuration; status information comprises:

whether or not the construct is currently analysed; if so, the following information is provided:
- the number of proven/unproven proof obligations associated with the construct at each proof level
- whether or not the construct is currently marked-up
- in the case of an implementation, whether or not it is currently translated
- a list of dependent constructs
- a list of subordinate constructs
- the abstraction/refinement/implementation list

(A construct A is `dependent' on a construct B if A SEES, USES, INCLUDES, IMPORTS or REFINES B; in those cases B is said to be a `subordinate' construct to A).

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