Perl’s motto “There’s more than one way to do it” applies to verification too. The proliferation of formal methods may seem haphazard to greenhorns; the claimed differences between variants of the same technique exaggerated. Granted, not every improvement is a groundbreaking breakthrough (anyway, not most of the time). But the space of solutions to the verification problem is huge and the theoretical limits outstanding; hence the interesting trade-offs are many, each sensible given different constraints. One size does not fit all.

Nadia‘s guest post about dimensions in verification covered the big picture. The follow-up point I’d like to make is that there’s a significant variability also between variants of the same verification technique. Francesco Logozzo‘s post about abstract interpretation triggered these thoughts of mine; in fact, I’m going to build on his example to illustrate my point.

Francesco presents the example of a routine that computes the maximum element in an array, using a `for`

loop that scans the array from its first to its last element, to show that his CodeContracts static checker — based on abstract interpretation — is not limited to dealing with “simple” properties such as nonnullness: it is capable of inferring the complete functional postcondition of `max`

, namely (using a more readable syntax):

This is remarkable, but let's try to modify the example to see where we can go from here. First, encode `max`

as a function that operates on an attribute `a`

by scanning it from last to first. (The following code is C#.)

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 |
class MaxList { int[] a; int max_downward() { Contract.Requires(a != null); Contract.Requires(a.Length > 0); var i = a.Length - 1; var Result = a[i]; while (0 < i) { i--; if (a[i] > Result) { Result = a[i]; } } return Result; } } |

Function `max_downward`

and the original one `max`

have the very same input/output behavior, and indeed they implement two variants of the same simple algorithm. Ran on `max_downward`

, the CodeContracts checker correctly infers that `Result`

is an element of `a`

(the existentially quantified postcondition above), and that it is greater than or equal to `a`

's last element, but it falls short of the complete functional postcondition (it misses the universally quantified postcondition).

I don't know the details of CodeContracts checker's implementation of an abstract interpreter, and hence I cannot track down precisely the source of this behavior. However, there is no reason to be surprised about this restriction: any sound verification technique edges on intractability; as users, it normally is not difficult to push it until undecidability rears its ugly head and, in this case, spills some precision. If anything, we should be surprised whenever a verification technique *works* flexibly in different conditions!

To continue our example, we accept to give up some automation in exchange for more flexibility. We turn to deductive verification; more precisely, *auto-active* verifiers. Rustan Leino and Michał Moskal introduced the term "*auto-active*" to denote tools that are partly *auto*matic and partly inter*active*. (By the way, my proposal to call them "inter-matic" has yet to catch on.) They are automatic in that they do not require interactive guidance while they try to verify an input program. But they still indirectly interact with users through *annotations*, such as pre- and postconditions, invariants, and suggestions such as intermediate assertions, which are an additional burden to write and crucially influence their capabilities and performance.

Even among auto-active verifiers, there is room for considerable variations in terms of flexibility and simplicity. Let's first consider Dafny, a state-of-the-art verifier mainly developed by the SMT whisperer — a.k.a. Rustan Leino. Dafny has a relatively simple input language, with built-in support for specification models such as mathematical sequences, of which we're going to take advantage in our example. Here's a variant of the example that verifies in Dafny: have a glance at the code, and then I'll point out the interesting parts.

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 |
class PSList { var sorted: bool; var a: array<int>; predicate is_sorted(s: seq<int>) { forall i, j :: 0 <= i <= j < |s| ==> s[i] <= s[j] } predicate Valid() reads this, a; { a != null && (sorted ==> is_sorted(a[..])) } method max_ps() returns(Result: int) requires Valid() && a.Length > 0; ensures Valid(); ensures forall k :: 0 <= k < a.Length ==> a[k] <= Result; ensures exists k :: 0 <= k < a.Length && a[k] == Result; { var i := a.Length - 1; Result := a[i]; if sorted { assert forall j :: 0 <= j < a.Length ==> a[..][j] == a[j]; return; } while 0 < i invariant 0 <= i < a.Length; invariant forall k :: i <= k < a.Length ==> a[k] <= Result; invariant exists k :: 0 <= k < a.Length && a[k] == Result; { i := i - 1; if a[i] > Result { Result := a[i]; } } } } |

Besides the array `a`

, class `PSList`

("Possibly Sorted" List) includes a Boolean attribute `sorted`

, whose role is storing whether the content of `a`

is sorted. One can imagine a complete implementation were this flag is set whenever the array is processed by a sorting algorithm or is populated by elements in order. The new variant of maximum, called `max_ps`

, takes advantage of this additional piece of information: if `sorted`

is true, it immediately returns the value `a[a.Length - 1]`

which is initially assigned to `Result`

. Indeed, the maximum of a sequence that is sorted in increasing order is its last element. The correctness of `max_ps`

relies on this fact; which we encode, following Dafny's idiomatic approach to representation invariants, as part of predicate `Valid`

: if `sorted`

is true then the content `a[..]`

of `a`

is sorted in increasing order. `Valid`

is supposed to be an invariant property, which methods of class `PSList`

can rely on and have to preserve. In fact, method `max_ps`

lists `Valid`

in its pre- and postcondition; and Dafny uses its clause about sortedness in the proof of branch `if sorted { ... }`

. (In case you're wondering: the `assert`

there is needed to help Dafny convert between `a`

's content and its sequence representation `a[..]`

.)

This example worked smoothly thanks to Dafny's transparent syntax, which explicitly represents all salient features of the code and its annotations. But suppose we make the example more realistic (and more complex) by adding `max_ps`

to the interface of a full-fledged general-purpose list data structure. In this case, we may prefer an auto-active tool with more options and control knobs, which gives additional flexibility in exchange for a steeper learning curve. AutoProof is a verifier that tries to offer such a trade off; thus, the last version of our maximum example is in Eiffel — AutoProof's input language.

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 |
class PS_LIST inherit FULL_FLEDGED_LIST [INTEGER] feature sorted: BOOLEAN is_sorted (s: MML_SEQUENCE [INTEGER]): BOOLEAN -- Is `s' sorted? note status: functional, ghost do Result := across 1 |..| (s.count - 1) as i all s [i.item] <= s [i.item + 1] end end max_ps: INTEGER require count > 0 local i: INTEGER do i := count Result := item (i) if sorted then check inv_only ("when_sorted") end else from invariant 0 <= i and i <= count across i |..| count as k all sequence [k.item] <= Result end across 1 |..| count as k some sequence [k.item] = Result end until i = 1 loop i := i - 1 if item (i) > Result then Result := item (i) end end end ensure across 1 |..| count as k all sequence [k.item] <= Result end across 1 |..| count as k some sequence [k.item] = Result end end invariant when_sorted: sorted implies is_sorted (sequence) end |

Class `PS_LIST`

builds its functionalities by extending those of some verified library implementation of a list with all the bells and whistles. In practice, `FULL_FLEDGED_LIST`

could be some list implementation among those in EiffelBase2. A couple of hints should suffice to explain the example's (imperfectly highlighted) syntax: `across`

expressions represent universal (`across ... all`

) and existential (`across ... some`

) quantification over integer intervals `x |..| y`

; `sequence`

is an inherited *model* attribute that describes the list's content as a mathematical sequence (indexed from 1, unlike the C# and Dafny examples).

We encode the sortedness property as part of the *class invariant*, in a clause named `when_sorted`

, which appears at the bottom of `PS_LIST`

's text. Remember that we are inheriting all of the functionalities of a full-fledged list, including a detailed, complex class invariant to which we *add* clause `when_sorted`

. Dealing with the kind of full functional specifications that are needed to reason about realistic implementations has some practical consequences: since the invariant is a lot of specification, carrying it around in the proof of every routine of the class is likely to bog down the verifier and to render the proof of even trivial properties a challenge. AutoProof, however, has been developed with these situations in mind. Routine `max_ps`

can recall the only invariant element that is needed precisely where it is needed in the proof, using the assertion `check inv_only ("when_sorted") end`

in the conditional branch `if sorted then ... `

. The many other consistency properties inherited with the invariant are simply ignored to the benefit of a straightforward, agile proof.

We've had a glance at two auto-active verifiers of functional correctness to get an idea of how they target different sweet spots in the sweeping landscape of verification techniques and their implementations. Stay tuned for more posts about AutoProof. In the meanwhile, you can check out its project page or try it out in your web browser. AutoProof's main developers, Nadia Polikarpova and Julian Tschannen, welcome feedback about the tool — especially in the form of comments to this post! ðŸ™‚