Formal Software Development

A quick course in Transformational Programming

Transformational Programming is a programming methodology that is suitable when correctness of the software is more important than development time (software for space missions, for example). Here you don't write programs by your intuition and test them for bugs afterwards. Instead you start from a given specification and derive the program by transforming the specification with several fixed rules which have been proven to be correct before. The following trivial example illustrates the idea.

Given

funct add (nat a, nat b) nat:           { executable program }
  if b=0 then a else add(a,b-1)+1 fi

funct sub (nat a, nat b: b<=a) nat:     { descriptive specification }
  that nat k: add(k,b) = a

Focus: Function sub
Goal: Derivation of executable program
Strategy: Unfold, Rearrange & Fold

Derivation

that nat k: add(k,b) = a

1. Unfold add in sub

that nat k: if b=0 then k else add(k,b-1)+1 fi = a

2. Distributivity of "= a" over conditional

that nat k: if b=0 then k = a else add(k,b-1)+1 = a fi

3. Distributivity of that-operator over conditional

if b=0 then that nat k: k = a else that nat k: add(k,b-1)+1 = a fi

4. Simplification of then-branch: "that nat k: k = a" simplifies to "a"

if b=0 then a else that nat k: add(k,b-1)+1 = a fi

5. Arithmetic simplification of else-branch

if b=0 then a else that nat k: add(k,b-1) = a-1 fi

6. Fold: According to the given specification of sub "that nat k: add(k,b-1) = a-1" simplifies to "sub(a-1,b-1)"

if b=0 then a else sub(a-1,b-1) fi

Result

funct add (nat a, nat b) nat:           { executable program }
  if b=0 then a else add(a,b-1)+1 fi

funct sub (nat a, nat b: b<=a) nat:     { executable program }
  if b=0 then a else sub(a-1,b-1) fi