Transformationelle Programmentwicklung

• Beweise in herkömmlicher Mathematik:

(a + b)^{2} = (a + b)(a + b) = a(a + b) + b(a + b) = a^{2} + 2ab + b^{2} • Äquivalenzumformung, evtl. mit Bedingungen

• … oder Implikation.

• Transformationelle Programmentwicklung: Umformung von Programmen

C. Lüth  Korrekte Software durch Formale Methoden  45

Transformationelle Programmentwicklung: Ein Beispiel

fib n   == if n<= 1 then 1 else fib(n-1) + fib(n-2)

⇓

fib n   == f n 1 0
f n a b == a*(fib n)+ b*(fib (n+1))

⇓ Unfolding

f n a b == a*(fib n)+ b*(if n+1<= 1 then 1 else (fib n)+(fib (n-1)))

⇓

f n a b == if n+1<= 1 then a*(fib n)+b
                      else a*(fib n)+ b*((fib n)+(fib (n-1)))

⇓

f n a b == if n<= 0 then a+b else b*(fib (n-1))+(a+b)*(fib n)

⇓ Folding

fib n   == f n 1 0
f n a b == if n= 0 then a+b else f (n-1) b (a+b)

Transformationelle Programmentwicklung: Grundlagen I

• SP_{1} ⇝ SP_{2} ⇝ … ⇝ SP_{n} SP_{i} Spezifikationen, ⇝ Verfeinerungsrelation:

• Korrektheitserhaltende Verfeinerung: SP_{1} ⊧ P ⇒ SP_{2} ⊧ P

• Modelinklusion: Mod (SP_{2}) ⊆ Mod (SP_{1})

• SP_{i} ⇝ SP_{i+1} durch Anwendung von Transformationsregeln.

C. Lüth  Korrekte Software durch Formale Methoden  47

Transformationelle Programmentwicklung: Grundlagen II Eine Transformationsregel ∀ P_{1}, …, P_{n}. A ⇒ I ⇝ O besteht aus

• Parametern P_{1}, …, P_{n},

• Eingabemuster I,

• Ausgabemuster O,

• Anwendungsbedingungen A

C. Lüth  Korrekte Software durch Formale Methoden  48

Transformationelle Programmentwicklung: Grundlagen III

Anwendung einer Transformationsregel ∀ P_{1}, …, P_{n}. A ⇒ I ⇝ O auf Spezifikation SP

1. Instantiierung der Parameter (durch Benutzer)

2. Eingabemuster wird auf Subterm T in SP = C[t] gepaßt: Substitution σ mit σ(I) = T

3. Neue Spezifikation ist SP′ =^{def} C[σ(O)] mit SP ⇝ SP′

4. Instantiierte Anwendungsbedingungen σ(A) werden Beweisverpflichtungen Verschiedene Transformationsregeln

• Logische Regeln: Fold, Unfold

A = B ⇒ A ⇝ B A = B ⇒ B ⇝ A

• Designregeln: Spezifikationen ausführbar(er) machen:

Einbettung (Embedding), Endliche Differenz (Finite Differencing), Nachbedingungsspaltung (Split of Postcondition), Dekomposition, … (siehe Partsch, Specification and Transformation of Programs)

Transformationsregeln: Einbettung

∀ E, K.

fun f x == ?H x

      ⇓  { y= ?H x --> y= K x E

fun f x   == g x E
fun g x y == K x y
f :: M ==> N
H :: M ==> N
g :: M* Y ==> N
E :: Y
K :: M* Y ==> N

Beispiele: Fibonacci, Fakultät.

Transformationsregeln: Einbettung, generalisiert

∀ E, K, i, j.

fun f x == ?H x

      ⇓  { y= ?H x --> y= j (K (i x) E)

fun f x   == j (g (i x) E)
fun g x y == K x y
f :: M ==> N
H :: M ==> N
g :: X* Y ==> Z
E :: Y
K :: X* Y ==> Z
i :: M ==> X
j :: Z ==> N

Transformationsregeln: Fallunterscheidung

∀ P.

@y. ?R x y

⇓

if P x y then @y. ?R x y else @y. ?R x y

∀ Z.

if ?P then ?X else ?Y
      ⇓  { ?P & (z= X) --> z= Z
if ?P then ?Z else ?Y

∀ Z.

if ?P then ?X else ?Y
      ⇓  { ~ ?P & (z= Y) --> z= Z
if ?P then ?X else Z

Transformationsregeln: Dekomposition

∀ Q, c′.

@y. ?P (?c x) y

      ⇓  \{ \begin{matrix}Q x z --> ?P (?c x) (c' z) \\ ? y. ?P (?c x) y --> ? z. Q x z \end{matrix}

c' (@z. Q x z)
c  :: M ==> N
P  :: (N* P) set
c' :: R ==> P
Q  :: (M* R) set