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

does so explicitly (but by violating the symmetry with CreateClient ). Implicit descrip-
tions are typically more abstract and aimed at establishing properties (for which purpose
symmetry is helpful), whilst explicit descriptions are typically closer to code; most
specification notations permit both styles, for use as appropriate in the development
cycle.
Since an implementation models all the predicates in its specification, it is difficult
to see, of an implicit-style specification, where possible inconsistencies come from: if
a function is defined by a postcondition the confidence condition becomes an assertion
that a result satisfying the postcondition, plus any relevant subtype condition, exists.
This does not tend to be very helpful in discovering errors. But when an explicit style
is used then a test can be run to check that a result lies in the appropriate subtype.
In a notation (like RSL) whose explicit functions may also have postconditions, the
redundancy permits a much stronger confidence condition to be generated. Similarly
with explicit preconditions (like RSL, VDM or the refinement calculus), which permit
a check that the explicit precondition is strong enough to ensure the preconditions of
functions and operators used in the definition. (The calculation of preconditions in Z
provides no redundancy, although it may introduce mistakes in the specification—an
inconsistency 4 between the calculated precondition and the implicit one—to be picked
up in testing [25].)
So it is seen that in Webbo the subtype checks are not so useful as checks on the
specification, although they do provide checks to be included in the implementation.
The checks will probably need to be optional, as some will be computationally expen-
sive, but they can be used in testing and debugging.

5.4 Partial Operators

The appearance of disjoint union, ,in Webbo exhibits the use that can be made of

partiality. It appears in several operations in the form

S = S T

from which follows the precondition that S and T are disjoint. It also appears in the
form

S = S

T

from which follows the postcondition that S and T are disjoint, though that is subsumed
in the more general postcondition which is the whole equality.

5.5 Are Equalities Assignments?

When a specifier in ObjectZ writes

e 0 = e 1

4

Typically because the specifier does not do the calculation carefully enough, relying on intu-
ition for the answer.