© 1996-2019







VI.2 Justification

Justification [Slide 177]

  • 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:

f present_state what_remains

Example 57.  

f
more f
f
f f

Example 58.  

Some examples of executable formulae:

skip I = 0 (I = 1)
len(3) (I = 2)
len(4) I = 0 I gets I + 1

Example 59.  

Some examples of non-executable formulae:

empty (I = 0 I = 1)
I = 0 ; I = 1
len(4) I gets I + 1







2019-05-10
Contact | Home | ITL home | Course | Proofs | Algebra | FL