Specification for Testing - Formal Methods and Hybrid Real-Time Systems - page 293

nor sufficient for consistency 3 , but their truth provides a degree of confidence in the
specification.
Confidence conditions therefore provide some opportunities for verification activi-
ties. The RAISE tools, for example, allow them to be generated and inspected, to be
generated and proved (in PVS), to be model checked (in SAL), and to be included in
executable code produced by translators. Confidence conditions are used in two ways:
to look for inconsistencies in the specification and also as hints for possible extra code
in the implementation, to be switched on during testing and possibly also to aid in de-
bugging. In this paper it is the second usage that is of particular interest.
In (sequential) RSL the main confidence conditions are:

- subtypes are not empty
- arguments to functions are in subtypes
- results of functions are in subtypes
- assignments to variables are in subtypes
- preconditions of functions are satisfied by invocations
- postconditions of functions are satisfied by invocations
- case expressions are complete.

Here 'functions' include built-in functions and operators, like division (perhaps by zero)
or taking the head of a list (perhaps empty).
Although those conditions might be expressed slightly differently in Z (schemas are
satisfiable, and functions and expressions are well defined at both their points of def-
inition and of use) they are equally important. The same ideas can be applied to any
specification language, but the possibilities will change with the language. In general,
there is a tendency for Z specifications to involve less redundancy than RSL ones, and
so the possibility for generating confidence conditions may be reduced. The next section
applies the idea of confidence conditions to Webbo .

5.3 Confidence Conditions in Webbo

Loginfo , with its three-predicate invariant, forms an RSL subtype. The State definition
has an invariant consisting of one explicit and one implicit predicate (the implicit pred-
icate mng : C

M with an explicit
constraint dom( mng )= C ), and so also forms an RSL subtype. Thus obvious checks
are

→ M expands to the type statement mng : Clients →

- Operations generate states consistent with the State predicate (which includes the
Loginfo predicates on each value in the range of log )
- Outputs of type Loginfo satisfy the Loginfo predicates.

The specification Webbo is written in a largely implicit style. Thus in RemoveClient ,
the condition C = C { defines C implicitly whereas the equivalent C = C c ? } \{ c ? }

3

Lack of sufficiency is obvious. They need not be necessary because of limitations in the static
analysis that generates them; for example the (low-level, but consistent) expression ' if false
then 1/0 else 1 fi ' might generate the confidence condition that the divisor 0 is not 0, which
fails to hold.