{... other generalities about Isabelle ...}
The remainder of this paper is now organised as follows. In Section 2, the language used to communicate specifications to the Isabelle technique is presented, and, in Section 3, the language used by Isabelle to express the synthesised algorithms is introduced. Section 4 is about the synthesis technique proper, and I illustrate Isabelle at work by means of a sample synthesis in Section 5. Next, in Section 6, a critical evaluation of Isabelle is given by relating it to other state of the art techniques. I then propose, in Section 7, some directions for future work around Isabelle, and develop one of them in detail. Finally, Section 8 concludes.
{... other details about the specification language ...}
This language is [a subset of first / second-order] logic / algebraic / ... . The axioms / examples / ... are written in relational / functional form, which means that {...}. Recursive axioms / ... are [not] allowed / needed, because {...}.
This specification language is [in]expressive / [un]readable / with[out] implementation bias, because {...}. Using this language, it is [im]possible to write specifications that are totally correct / partially correct / complete with respect to the intentions, and that are minimal / internally consistent / unambiguous / non-redundant, because {...}. The assumption for synthesis is that a submitted specification is {...}, because {...}.
{... other details about the target language ...}
Such expressions can be seen as algorithms, rather than [logic] programs, because {...}. Isabelle itself provides [no] support for implementing such algorithms into programs (written in {...}). By the way, the Isabelle system is itself written in {...}, and [but] it has [not] been used to synthesise [parts of] itself [Reddy 94].
{... other details of the synthesis technique,
preferably illustrated by a "small" and "easy" example ...}
This synthesis technique is [not] proven to be sound, that is to {...} [Reddy 94]. Moreover, it is [non]deterministic, because {...}. It is [semi-]automatic, because {...}. The combinatorial explosion of the search space is tackled by {...}.
The synthesised algorithms / programs reflect a divide-and-conquer / generate-and-test / ... strategy, because {...}. Algorithms / Programs that are a composition of algorithms / programs of different strategies can[not] be synthesised, because {...}.
{In case it is a divide-and-conquer strategy:} The induction parameter is selected by {...}. Compound induction parameters (i.e. induction parameters that {...}) can[not] be handled, because {...}. The minimal forms of the induction parameter (that is the values of the induction parameter where {...}) are determined by {...}. There can / must thus be an arbitrary / constant (namely m) number of minimal forms. The non-minimal forms of the induction parameter (that is the values of the induction parameter where {...}) are determined by {...}. There can / must thus be an arbitrary / constant (namely n) number of non-minimal forms. The induction parameter can be decomposed intrinsically (in a way reflecting {...}), because {...}. The induction parameter can also / cannot be decomposed extrinsically (in a way reflecting {...}), because {...}. Minimal cases (cases where the induction parameter is of a minimal form) and non-minimal cases (cases where the induction parameter is of a non-minimal form) can[not] be further split into sub-cases, because {...}. Discrimination between such sub-cases is then achieved by {...}. Useless recursion in non-minimal cases is [not] detected, because {...}. Auxiliary parameters (parameters that {...}) are detected / declared via {...}. Algorithms / Programs for appearing auxiliary problems are designed by re-use and/or re-invocation of the synthesiser, namely {...}.
{In case it is a divide-and-conquer strategy:} The synthesised algorithms / programs may thus feature intrinsic [as well as extrinsic] decomposition of the induction parameter, complete [as well as incomplete] traversal of the induction parameter, and single loops [as well as multiple nested loops]. The synthesised algorithms / programs may be deterministic / fully deterministic / non-deterministic / finite / infinite, given ground values of the induction parameter and of the auxiliary parameter(s), because {...}. Structural manipulation problems (problems where {...}) [as well as semantic manipulation problems (problems where {...})] may be handled, because {...}.
{... specification of the compress/2 problem ...}
The synthesis of an algorithm / program from this formal specification
is a piece of cake for Isabelle, and goes as follows:
{... details of the synthesis ...}
Finally, the synthesised algorithm / program is as follows:
{... algorithm / program for the compress/2 problem ...}
This algorithm / program features {... use the vocabulary defined in Section 4 ...}. Alternative algorithms / programs can be obtained by {...}. The chosen sample problem turns out [in]significant, because {...}.
Synthesis is [not] knowledge-based. Indeed, algorithm design knowledge (knowledge about {...}) is {...}. Efficiency / complexity knowledge (knowledge about {...}) is {...}. Domain knowledge (knowledge about {...}) is {...}. Meta-knowledge (knowledge about {...}) is {...}.
There is [no] support for evolving intentions and specifications, because {... history mechanism ... re-play ...}.
Compared to Periwinkle / Cypress / KIDS {respectively: DIALOGS / SMART / Progol}, the Isabelle approach {...}.
{... details about my brilliant ideas about what to do with Isabelle ...}
The Isabelle system is actually much larger in scope than what has been examined in this paper, as it also provides support for specification elaboration / specification validation / specification maintenance / algorithm transformation / algorithm implementation (into Prolog / ... programs) / program optimisation.
I believe the Isabelle technique is a[n] [in]significant contribution to the state of the art in program synthesis, because {...}. Isabelle has [not yet] reached the break-even point, where {...}, because {...}. {... my other conclusions ...}.