<p><strong>Short answer:</strong> no.</p>

<p><strong>Long answer:</strong> 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).</p>

<p>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?"</p>

<p>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.</p>

<p>To answer the refined question we need to answer another first.</p>

<p><em>What expressive power would we need in the assertion language?</em></p>

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

<p>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]$.</p>

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

<ol>
<li>a primality checker</li>
</ol>

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

<ol>
<li>a sorter that takes arrays of arbitrary size as inputs</li>
</ol>

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

<p>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 <em>arbitrary formulas $\phi$ of Peano arithmetic</em>, before worrying about how to synthesize implementations. But that is already undecidable.</p>

CC BY-SA 3.0
2013-06-20T04:44:17.793Z
Thanks @Kai for taking time on this explanation. It's very reasonable.
Chuck
CC BY-SA 3.0
2012-11-14T13:50:02.057Z
2012-11-14T13:50:02.057Z
Kai
<p>I had to derivate, by hand, sequential iterative programs at school using an unified Hoare-Dijkstra-Hehner programming theory.</p>

<p>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.</p>

<p>How to automate this process? is it feasible?</p>

CC BY-SA 3.0
2012-11-07T10:10:24.743Z
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
CC BY-SA 3.0
2012-11-07T21:57:38.560Z
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.
Chuck
<lo.logic><pl.programming-languages><formal-methods><automated-theorem-proving>
How to auto-derivate sequential iterative programs from a mathematical specification?
Chuck
# How to auto-derivate sequential iterative programs from a mathematical specification?

(Asked by: username_0 on 2012-11-07)

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?

**Tags:** lo.logic, pl.programming-languages, formal-methods, automated-theorem-proving
> **Comments:**
> **username_1**: 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.  
> **username_0**: 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.  

---

## 1 answers

### Answer by username_2 on 2012-11-14. Score: 6 | Accepted answer

**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

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.

> **Comments:**
> **username_0**: Thanks @Kai for taking time on this explanation. It's very reasonable.  

---

