This document will build up a proposal for a possible new way to generate strong program templates from minimal specifications:
Abstract Example
Concrete Example
```
(| P |)
*
(| Q |)
```
```
(| x > 0, x0 := x |)
*
(| a == s(x0) - x0 |)
```
This is how we would like to be able to specify programs: with just a precondition `P`, a postcondition `Q`, and the freedom to generate any number of instructions in place of `*`. However, it does not work to naively perform a search for the whole program at once, as this is too computationally intensive.
The example here specifies a program computing the _abundance_ of a positive integer `x`, i.e. by how much the sum of `x`'s proper divisors, `s(x)`, exceeds `x`. When its abundance is 0, `x` is called a _perfect number_. Of course, when we try to run this specification, it just takes a very long time, and we eventually lose patience.
```
(| P |)
*
while (*):
*
end_while
*
(| Q |)
```
```
(| x > 0, x0 := x |)
*
while (*):
*
end_while
*
(| a == s(x0) - x0 |)
```
The reduce the search space, we could predetermine some of program's structure. This could be done automatically by iterating on the number of while loops at the top level of the program, for example. Many interesting programs will have 0 top-level loops, and many more will have 1, with fewer having 2 or more. Controlling the search in this manner benefits the synthesis time of simple programs, but it is still not enough for complicated programs.
```
(| P |)
*
while (G):
var: V
*
end_while
(| R |)
*
(| Q |)
```
```
(| x > 0, x0 := x |)
*
while (a < x):
var: x - a
*
end_while
(| s == s(x0), x == x0 |)
*
(| a == s(x0) - x0 |)
```
Specifying a loop guard `G`, a loop variant `V` (which must be positive while the loop is running, and decrease strictly on each iteration), and a _loop postcondition_ `R`, will allow some further structures to be automatically determined.
However, the question of how to obtain these parameters is not fully answered. The current approach is to have the user give them, but it seems like it might be possible to infer them in some way and/or iterate on their possible values or solve for them using ASP.
In the example of the right, a loop guard has been arbitrarily chosen based on our understanding of the problem domain; a sensible loop variant is in this case easily derived from the guard; and the postcondition says what we expect to be achieved directly after the loop terminates, that is the calculation of the sum of x's proper divisors.
```
(| P |)
*
(| ¬G -> R |)
while (G):
(| G, V0 := V |)
*
(| ¬G -> R,
V<=0 -> ¬G2,
V
```
(| x > 0, x0 := x |)
*
(| a>=x -> s==s(x0) |)
while (a < x):
(| a < x, v0 := x-a |)
*
(| a>=x ->
(s==s(x0),
x == x0),
x-a<=0 -> a>=x,
x-a
The information previously added to the template was carefully chosen to be minimal, but sufficient to allow the derivation of enough information to set some strong requirements on the termination and of the loop, and the correctness of the program with respect to the earlier specification:
We know that `R` must hold as soon as the guard `G` is false, so we can assert that `¬G -> R` in the two places where we might go past the loop. We also know that the guard must hold at the beginning of the loop, so we can put `G` there. Finally, we formalise the properties of the variant `V` by requiring it to decrease monotonically, and the guard to be false by the time the variant has reached 0.
This does, however, not work with the current method of example-drive synthesis, as our process lacked insight into the nature of the intermediate computation required by the specification, and the loop precondition is too weak to fully represent the behaviour of an actual loop solving this problem: for example, it accepts starting states where the variable `x` has been changed from its initial value, making it impossible to complete the calculation.
Two ways to solve this have been considered:
1. Allowing the user to strengthen the precondition (and possibly also the postconditon) of the loop based on their knowledge of the problem domain. This could take the form of a _loop invariant_, as are classically used to reason about program correctness. This is effective if the user knows what invariant to give, but is not very satisfying, as the synthesiser isn't doing much work.
2. Noting that if we only provided actual input examples produced by a correct (sub)program to the loop precondition and postcondition it is likely to be satisfiable for all of them even if in principle it is unsatisfiable for some values that never occur, we could try to learn all subprograms in parallel in a similar manner to how it is currently done, but instead of generating arbitrary counterexamples, only use input examples produced by the precondition, or produced as correct output from a midcondition prior to the subprogram of interest.
This document will build up a proposal for a possible new way to generate strong program templates from minimal specifications:
After further discussion, it has been decided that this isn't currently the best direction in which to take the project.