Runtime consistency checking
Instructor's Guide
intro,
methods,
objects,
contracts,
formal,
summary,
Q/A,
literature
Debugging is a hopelessly time-consuming and unrewarding
activity.
Unless the testing process is guided by clearly
specified criteria on what to test for,
testing in the sense of looking for errors
must be considered as ordinary debugging,
that is running the system to see what will happen.
Client/server contracts, as introduced
in section [contracts] as a method for design,
do offer such guidelines in that they enable the programmer
to specify precisely the restrictions characterizing
the legal states of the object,
as well as the conditions that must be satisfied
in order for legal state transitions to occur.
See slide [4-contracts].
Assertions -- side-effect free
contracts
- require -- test on delivery
- promise -- test during development
Object invariance -- exceptions
- invariant -- verify when needed
Global properties -- requirements
- interaction protocols -- formal specification
slide: Runtime consistency checking
The Eiffel language is the first (object-oriented)
language in which assertions were explicitly
introduced as a means to develop software
and to monitor the runtime consistency of a system.
Contracts as supported by Eiffel were primarily
influenced by notions concerning the construction
of correct programs.
The unique contribution of [Meyer88] consists
of showing that these notions may be employed operationally
by specifying the pragmatic meaning of pre- and post-conditions
defining the behavior of methods.
To use assertions operationally, however, the
assertion language must be restricted to
side-effect free
boolean expressions
in the language being used.
Combined with a bottom-up approach to development,
the notion of contracts gives rise to the following
guidelines for testing.
Post-conditions and invariance assertions should
primarily be checked during development.
When sufficient confidence is gained in the reliability
of the object definitions, checking these assertions
may be omitted in favor of efficiency.
However, pre-conditions must be checked
when delivering the system to ensure that
the user complies with the protocol specified by the contract.
When delivering the system, it is a matter of contractual
agreement between the deliverer and user
whether pre- and/or post-conditions will be enabled.
The safest option is to enable them both,
since the violation of a pre-condition
may be caused by an undetected violated post-condition.
In addition, the method of testing for identity transitions
may be used to cover higher level invariants,
involving multiple objects.
To check whether the conditions with
respect to complex interaction protocols are
satisfied, explicit consistency checks need to be inserted
by the programmer. See also section [global-invariants].