Sub-specifications

Consider a simple example: computing the Fibonacci numbers. The specification for this function is pretty simple:

Inductive Fib : nat -> nat -> Prop :=
| fib0 : Fib 0 1
| fib1 : Fib 1 1
| fib_plus : Fib n x -> Fib (S n) y -> Fib (S (S n)) (x + y)

Then you go ahead and implement some function fib and prove that it works by proving Fib n (fib n).¹ [¹ Maybe you also go and prove some facts about the spec, like making sure that Fib is a functional relation.] This works,² [² The induction principle might be a little tricky.] and you can now ignore fib and reason directly about the Fib specification.

But consider that there are lots of ways to implement the Fibonacci function: plain recursion, memoization, an array, a two-variable loop, the matrix method, the implicit matrix method, or a number field method. The specification I proved above tells us that we correctly implemented the Fibonacci function, but it doesn't tell us that we correctly implemented, say, the implicit matrix method.

What can be confusing here is that the implicit matrix method satisfies the same end-to-end specification as even the naive Fibonacci function.³ [³ It has different asymptotics, but this isn't enough to distinguish, say, the implicit matrix from the number field methods.] Instead, it has a different specification at a different layer: an implementation of implicit matrix Fibonacci has a data structure for representing implicit matrices (the representation can be verified), for adding and multiplying them (the operations can be verified), for implementing fast exponentiation (perhaps verified against the specification for multiplication), and so on. And of course you would also need to prove that the matrices chosen correctly implement the Fibonacci function.

These intermediate specifications are probably not accessible to callers of the Fibonacci function, but they are accessible to different parts of the Fibonacci implementation. In fact this implicit matrix Fibonacci function has a rich internal structure, with a lower level implementing implicit matrices and a higher level implementing Fibonacci, and the lower level ought to be opaque to the higher level.

Given this richly-structured set of specifications, verification can offer many tools even when it cannot do anything for the highest-level goals like attractiveness: lower-level specifications can often be formalized even the high-level ones can't. A good example of this is the Neutrons project at UW,⁴ [⁴ Done by my very talented colleagues Stuart Pernsteiner, now at Galois, and Calvin Loncaric, now at Oracle, with a lot of the UW PLSE faculty advising them.] the goal of which was to formally verify the software that control's UW Medicine's neutron therapy machine. No one knows enough about the world to prove that the machine cures cancer,⁵ [⁵ Let alone “often enough”.] but it is definitely possible to prove that the beam turns on and off when it's supposed to, and that's definitely part of the plan the neutron therapy machine's designers developed for how the machine ought to work. Neutrons combines multiple formally-verified static analysis tools with a very domain-generic Alloy framework for combining these tools together. Here Alloy plays the role of allowing less-formal reasoning where each sub-specification an be proven not only using different tools but using different models of the world and different assumptions.

In web page layouts, the same pattern occurs. The overall goal of the page involves things like attractiveness, usability, certain functionality, and accessibility. This is the high-level, end-to-end specification—unfortunately, it is, as far as we know now, unformalizable. To meet that specification, the designer makes certain decisions, like the choice to have a two-column layout with toolbars and a footer. These decisions aren't yet a program: they are a new, more refined specification. To implement them, there are yet further lower-level specifications: the footer has links on the left in three columns and the address and contact info on the right; there are three toolbars, corresponding to "store-wide", "department-wide", and "item-specific" actions; and so on. These levels go lower and lower, until you have specifications like "enticing color" and a concrete implementation like a particular shade of blue from a color palette. Again, even when the highest-level decisions are difficult to review or understand, the lower-level ones can be verified, and mistakes often caught.

A useful perspective is to think of writing a program (whether manually or using program synthesis) as the task of developing finer and finer sub-specifications, until the specifications get as granular as "increment x". This perspective explains how even large programs can be synthesized by humans, even though there are a near-infinite number of even 100-line programs, let alone the million-line monstrosities frequently written by teams: instead of writing a million lines of code at once, people write a dozen lines of specification at a time, thousands of times.

This idea is being pursued more and more in automated program synthesis as well. N. Polikarpova and I. Sergey's recent SuSLik paper is a good example: to synthesize mutating, heap-manipulating programs, SuSLik starts with a high-level specification for the behavior of the program, and then transforms the specification using a variety of rules. Some of those rules add code to the program; others don't. N. Polikarpova's earlier Synquid project did something similar, except instead of Separation Logic for specifying heap-manipulating imperative code, it used Refinement Types for specifying functional programs.

I've been reading classic AI papers that separate planning into “plans as execution” and “plans as communication”. When you think of plans as execution, you think about plans as programs, and using a plan as automatic. Then a plan has to have a complete model of the outside world in it, in order to respond to the complexity of the outside world, and a plan is usually very large to account for the unpredictability of the world. When you think instead of plans as communication, you stop believing that executing a plan must be purely mechanical. Since the executor is allowed to improvise and use domain-specific knowledge, the plan itself can be simpler and shorter, in an asymptotic sense.

As I read these papers, more and more I am thinking about these synthesis tools not as ways of synthesizing programs, but as ways of synthesizing useful sub-specifications. These sub-specifications are not executable—they might require further synthesis—but they communicate important information about how to accomplish a task and how to organize information. I try to imagine: what if the synthesis task was interrupted half-way through. What information could it "hand off" to a human, so as to pass along as much useful information as possible.

Now, what useful means there is tricky. It is always possible to refine a specification into “do the thing, then do nothing”. In purely-enumerative synthesis approaches the only measure of usefulness might be implicit, with useless specifications just failing to eventually produce a program. But in a more directed tool like SuSLik, there are a variety of ways to tell that a specification is more useful, like if it operates on sub-heaps, or less useful, like if the input heap provably does not the information necessary to produce the output heap. It might be possible to have SuSLik return, even when it fails to synthesize a program, a set of sub-specifications that it believes are possible to satisfy, for a human to fill in.⁶ [⁶ Note that this is the opposite of sketching, where the human decomposes the high-level specification into low-level specifications and leaves the computer to do the final bit of synthesis.]

I'd like to spend some more time thinking about how to tell whether a sub-specification has usefully decomposed the parent specification, or whether it has simply hidden the problem elsewhere. It's tricky. For one, there has to be some notion of termination: if the sub-specification requires solving the overall problem, it probably didn't help (though what if it established a useful precondition?). Then, there's some notion of well-foundedness: you can't turn a specification about lists of length \(n\) into special cases for length 1, length 2, and so on forever (but it can be helpful to have a few). There is a informational challenge: each sub-specification has to have enough information in its precondition to establish its post-condition. What else is there?

I think there is also an interesting challenge in how to represent specifications. Even when high-level specifications are concise, lower-level specifications often include steps like “come up with a data structure to represent X”. Those steps are hard to represent in simple logics.