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

State ) constitutes a sub-type in RAISE. Because of their importance in testing, both
approaches are considered here.

5.1 Invariants

System invariants can be thought of as generalising algebraic laws. They are strictly
more general: a property may hold after an operation is invoked even though it may not
be captured in a law. As has just been seen, Webbo contains both explicit and implicit
invariants. A further type of implicit invariant holds not from the expansion of a depen-
dent type but from a property that holds initially and is maintained by all operations. An
example is the nonemptiness of A . In principle each invariant provides an important test
(if it can be achieved in the web-based implementation). This is something the specifier
is in a position to provide, and will typically have considered either making explicit in
the specification, or proving is a consequence of it.
An example of a restriction on testing imposed by the web-based interface is in
testing the (explicit) invariant

∀ u : U · log ( u ) . no ≤ 3 .

That cannot be tested directly without access to the internal variable that records the
number of consecutive failed logins (something the web-based interface does not al-
low). For instance, in most applications we cannot directly test if log ( u ) . no has the
value 2 after two unsuccessful logins. Thus the invariant must be changed, to incorpo-
rate

log ( u ) . lock ⇒ LoginFail(u,_) .

This can be tested at the state where the lock is first set (when log ( u ) . no equals 3). At
this point any attempt to invoke Login on that user account should fail. The fact that the
account is locked can be obtained in most implementations.
Another kind of invariant is that subtypes are used in a consistent manner: if an
operation with inputs or states in a subtype is supposed to preserve that subtype (in the
sense that outputs or state after also lie in the subtype), then it actually does so.
Less comprehensive invariants, nonetheless important for testing, are typically
conveniently expressed in temporal logic. It has been shown [17] that in some circum-
stances such temporal formulae can replace the model-based specification for the pur-
poses of testing. But in general just as a state-based specification can be complemented
by algebraic laws—or refinements, i.e. one-sided laws—so too it can be complemented
by temporal properties that the specifier is in a position to posit.

5.2 Confidence Conditions

Confidence conditions 2 are certain kinds of condition on a specification whose failure,
it has been found by experience, often indicate error. They need be neither necessary

2

The term was coined in the RAISE project [20,21].