Executable speciﬁcations 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 clariﬁed and
completed by hands-on experience with the executable
speciﬁcation.

execution of the speciﬁcation 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 speciﬁcations
on the required level of abstraction.

Executable speciﬁcations are constructive, i.e. they do not only
demand the existence of a solution, they actually construct it.

Non-executable speciﬁcations which are constructive can be
transformed into executable ones on almost the same level of
abstraction. The resulting executable speciﬁcations are often
based on search. It is not necessary to introduce new algorithms
to achieve executability.

Executable speciﬁcations 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.

Veriﬁcation of an implementation against the speciﬁcation
becomes superﬂuous if one uses the transformational approach.

Example [Slide 180]

Consider the following ITL formula

Example 56.

M = 4∧N = 1∧halt(M = 0)∧MgetsM − 1∧Ngets2 ∗ 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: