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.
© B-Core
(UK) Limited, Last updated: 22 Feb 2002