How to auto-derivate sequential iterative programs from a mathematical specification?

I had to derivate, by hand, sequential iterative programs at school using an unified Hoare-Dijkstra-Hehner programming theory.

First, write down the formal specification as a Hoare triple and figure out invariants for loops. Second, apply logic rules and theorems to find an implementation that satisfies completely the specification ensuring total correctness. Actually not an easy job.

How to automate this process? is it feasible?

• There is quite a lot of work on ideas like that and most often it is referred to as "synthesis". Starting from Hoare triples, I am not too familiar with the literature, but you can, for example, use temporal logics to specify a system and then use synthesis methods to derive a system. There are nice introductions to the field written by Wolfgang Thomas. – Markus Nov 7 '12 at 10:10
• It is incredible how long this research topic has taken. Maybe factoring and reuse issues has limited its expansion towards an industrial acceptance or even costs of getting coders making good specifications is higher than testing. I have found very good resources and papers since you put the magic word on, thanks. – Carlos Uribe Nov 7 '12 at 21:57

Long answer: No, because the synthesis problem is in general undecidable once you allow for a modest amount of expressive power in the assertions (pre- and post-conditions).

The specification for your synthesizer $S$ would look something like this. Its type would be $S:\mathit{Assn}^2\rightarrow\mathit{Prog}$, that is, given two assertions (a pre- and a post condition) it would return a program. Its functionality would be given by $\{\phi\}S(\phi,\psi)\{\psi\}$, for all $\phi,\psi\in\mathit{Assn}$. I understand your question as "is $S$ computable?"

Before we need to get technical, note that we've been a bit sloppy. $S$ can hardly be a total function for we could feed it an infeasible spec such at $[\mathit{true},\mathit{false}]$. Consequently, the best we could hope for is a partial function that works for all implementable specifications.

What expressive power would we need in the assertion language?

Firstly, assuming that we're living in a simple world where we only deal with integers, we require the usual operations from integer arithmetic.

Secondly, we need a mechanism to refer in the post-condition to the value of a program variable in the pre-condition. Without such a mechanism, we cannot even specify an increment-by-one function. Various such mechanisms exist. Let us here use one borrowed from the Z specification language: in the post-condition primed occurrences $x'$ of a variable $x$ refer to its value after the program has terminated whereas unprimed occurrences denote its value in the pre-condition. With this convention the increment-$x$-by-one function is specified by $[true,x'=x+1]$.

Thirdly, we'd also want quantifiers so we can at least specify simple examples such as

1. a primality checker

$[x > 0, x=x'\land(p\Leftrightarrow x>1\land\forall k(k>1\land \exists j(kj=x)\Rightarrow k=x))]$, and

1. a sorter that takes arrays of arbitrary size as inputs

$[\mathit{true},\mathit{length}(a)=\mathit{length}(a')\land\mathit{elements}(a)=\mathit{elements}(a')\land\forall i(1\leq i <\mathit{length}(a')\Rightarrow a'[i]\leq a'[i+1])]$.

With those ingredients, we have quite some power at our disposal, too much as it turns out. Even the domain of $S$ is undecidable because we would need to say whether a spec $[\mathit{true},\phi]$ is implementable or not, for arbitrary formulas $\phi$ of Peano arithmetic, before worrying about how to synthesize implementations. But that is already undecidable.

• Thanks @Kai for taking time on this explanation. It's very reasonable. – Carlos Uribe Jun 20 '13 at 4:44