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

where e 0and e 1 are general expressions, then the confidence condition that one might
generate is that there is a non-empty intersection between the possible sets of values for
e 0and e 1. But when the left-hand side of the equality is x !or x ,where x is a variable
whose type is a subtype, the equality can be regarded as an explicit specification of an
assignment in the implementation, in which case the stronger check can be introduced
that the value of the expression on the right-hand side lies within the variable's subtype.

5.6 Guide to Implementers

A number of checks can therefore be generated to apply as optional code in the final
implementation. However their execution requires:

- Equality functions on all types are needed. Since, as mentioned elsewhere, the fi-
nally implemented types are typically richer, an abstract equality needs to be im-
plemented which is obviously defined in terms of the (abstract) equalities on the
components
- In general, the constituents of the specification need to be implemented, or some
means found to express the conditions in terms of the implementation.
For example, the relation post is unlikely to be held as a set: it will be calculable (in
theory) as such a relation from, perhaps, individual mail boxes for recipients like
one which associates to each receiver a set consisting of pairs comprising a sender
and a message

postbox : U → P ( U × Mess )

subject to the coupling invariant

post = { ( u , r , m ) : U × U × Mess | u ∈ U ∧ ( r , m ) ∈ postbox ( u ) } .

Then the assertion that a message exists with someone as recipient is easy to imple-
ment. The assertion that some message exists with a given sender would be harder
(unless the implementation followed a design in which each user kept an analogous
outbox of sent post).
- Following from the previous point, it is clear that the code used to implement these
checks will often break properties such as security that need to be imposed on
user-accessible functions. How to deal with this is unclear. For example one user
ought not to be able to access another's post (except perhaps the sender, if the
outbox design is used). Yet to test the operations of AdminPost and UserMail ,just
such probing is necessary. However this treatment has stopped short of security and
other such properties.

6 Boundaries

Boundary value testing is an important technique that has been adopted in MBT [24]:
each operation is tested at each state that is (reachable and) extreme in a sense defined
by the tester. In Webbo , boundary testing focuses on the extreme values of the Loginfo