Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
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?
Short answer: no.
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.
To answer the refined question we need to answer another first.
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
$[x > 0, x=x'\land(p\Leftrightarrow x>1\land\forall k(k>1\land \exists j(kj=x)\Rightarrow k=x))]$, and
$[\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.
