Executable specifications allow demonstrating the behaviour of a system
before it is actually implemented. This has three positive consequences for
system development:
executable components are much earlier available than in
traditional life cycle therefore validation errors can be corrected
immediately without incurring costly redevelopment.
requirements that are initially unclear can be clarified
and completed by hands-on experience with the executable
specification.
execution of the specification supplements inspection and
reasoning as means for validation. This is especially important
for the validation of non-functional behaviour.
Declarative languages, especially logic languages,
combine high expressiveness with executability. They allow writing both
property-oriented and model-oriented executable specifications on the
required level of abstraction.
Executable specifications are constructive, i.e. they do not only demand
the existence of a solution, they actually construct it.
Non-executable specifications which
are constructive can be transformed into executable ones on almost the
same level of abstraction. The resulting executable specifications are
often based on search. It is not necessary to introduce new algorithms
to achieve executability.
Executable specifications do not necessarily constrain the choice
of possible implementations because only minimal design and
implementation decisions are necessary to get executability. In addition,
these decisions are revisable.
Verification of an implementation against the specification becomes
superfluous if one uses the transformational approach.
Example [Slide 180]
Consider the following ITL formula
Example 56.
M = 4 ∧ N = 1 ∧halt(M = 0) ∧ M gets M − 1 ∧ N gets 2 ∗ N
Interval:
State 0: M=4 N=1
State 1: M=3 N=2
State 2: M=2 N=4
State 3: M=1 N=8
State 4: M=0 N=16
Tempura interpreter [Slide 181]
Tempura interpreter:
Given a executable ITL (Tempura) formula
Generate a satisfying interval
A formula is executable if
it is deterministic,
the length of the satisfying interval is known.
the values of the variables (of the formula) are known throughout the
satisfying interval.
Tempura interpreter:
takes a Tempura formula and constructs the satisfying sequence of states, i.e.
interval, using the following rewrite technique: