A DSL for Integer Range Reasoning: Partition, Interval and Mapping Diagrams

Abstract

Expressing linear integer constraints and assertions over integer ranges—as becomes necessary when reasoning about arrays—in a legible and succinct form poses a challenge for deductive program verification. Even simple assertions, such as integer predicates quantified over finite ranges, become quite verbose when given in basic first-order logic syntax. In this paper, we propose a domain-specific language (DSL) for assertions over integer ranges based on Reynolds’s interval and partition diagrams, two diagrammatic notations designed to integrate well into linear textual content such as specifications, program annotations, and proofs. We extend intervalf diagrams to the more general concept of mapping diagrams, representing partial functions from disjoint integer intervals. A subset of mapping diagrams, colorings, provide a compact notation for selecting integer intervals that we intend to constrain, and an intuitive new construct, the legend, allows connecting colorings to first-order integer predicates. Reynolds’s diagrams have not been supported widely by verification tools. We implement the syntax and semantics of partition and mapping diagrams as a DSL and theory extension to the Why3 program verifier. We illustrate the approach with examples of verified programs specified with colorings and legends. This work aims to extend the verification toolbox with a lightweight, intuitive DSL for array and integer range specifications.

1 Introduction

Deductive program verification is the activity of establishing correctness by mathematically proving verification conditions (VCs) extracted from a program and its specification. If all VCs are proved, the program is guaranteed to terminate in a state satisfying its postcondition for all inputs satisfying the precondition. While much of the mechanics of program verification is automated by VC generators and automatic theorem provers, the construction of correct programs by this method remains a largely interactive task. In the case of total correctness verification of sequential programs, VC generation relies on supplying a pre- and postcondition specification of each subroutine (procedure, method), and verification of a subroutine in turn requires intermediate assertions and loop invariants to be inserted into the routine. Producing these assertions requires both familiarity with a formal state description language and the ability to express the assertions in it succinctly. Such languages are usually based on first- or higher-order logic, and like programming languages general-purpose. While concise at expressing basic mathematical relations, constraints over arrays and integer ranges tend to require verbose expressions, obfuscating the original notion. Indeed, for array constraints, pictures often provide a more intuitive grip on the problem. For instance, given the textbook verification exercise of specifying the loop invariant of a binary search routine that determines the presence of the value x in a sorted array a (indexed from 0 to $n-1$), we may start by jotting down a box diagram similar to the following:

This diagram captures the pertinent assertions over the mutable state of binary search: that the loop variables l and u partition the array into three disjoint subarrays, and that the value x is not present in the leftmost or rightmost subarray. Once these relationships have been understood, we may then refine the diagram into a logic formula. A possible rendition of the above in first-order predicate logic is:

$$ 0\le l\le u+1\le n\;\wedge \;\forall i(0\le i<l\vee u<i<n\Rightarrow a[i]\ne x) $$

It is easy to see that the formula lacks the legibility of the diagram, but is it actually more formal, as to make us accept this tradeoff? If we stipulate that the juxtaposition of the indexes (0, l, u and n) and the vertical lines denotes order constraints, and that the propositions written inside the shaded ranges are universally quantified over the corresponding subarrays, the diagram becomes semantically equivalent to the predicate logic formula. Hence, if the diagram incurs no loss of information, but appears more closely connected to our understanding of the domain, reasoning with the diagram directly could benefit both precision and legibility. As Dijkstra notes, “the purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise” [8]. However, unlike diagrams, predicate logic carries with it a collection of formula manipulation rules. Only given similar rules for diagrams like the above, may we consider them a worthy alternative to predicate logic for writing specifications and proofs. This is precisely the motivation behind Reynolds’s interval and partition diagrams, introduced 40 years ago [16] together with a set of abstractions for reasoning about arrays. Reynolds argues “Of course, an equivalent assertion can be given in the predicate calculus, but this sacrifices the intuitive content of the diagram [...] A better approach is to formalize and give rigorous meaning to the diagram itself.”

Approaching diagrams as formal specifications in their own right rather than as stepping stones, we do observe some rough edges in the box diagram: multiple occurrences of the expression $a[i]\ne x$ and the ad hoc assumption that i is quantified over the indexes of the shaded subarrays, while a and x, on the other hand, are free. To avoid the redundancy and clarify variable binding in the shaded subarrays, we redraw the diagram as follows:

The revised diagram consists of two components: a legend asserting $a[i]\ne x$ over a single shaded element at index i, and a box diagram specifying the constraints on l, u and n as well as the extent of the shading. Following Reynolds, we also place the partition bounds inside the boxes rather than below them, as this convention both conserves space and increases legibility of a bound’s position relative to its adjacent vertical line. Our intention with this example so far has only been to demonstrate that box diagrams are sufficiently precise for formal specification. As we will see through examples in the sequel, legends extend naturally to properties involving multiple indexes, such as sortedness (which we omitted for brevity in the above example). We give a detailed syntax and semantics of these diagrams, and present tool support for verifying programs specified with such diagrams.

Reynolds’s Diagrams as a DSL. Domain-specific languages (DSLs), mini-languages tailored for a particular application, are commonly used in software engineering to raise the level of abstraction. The degree of sophistication range from substitution macros to rich high-level languages. A DSL should be easy to both use and opt out of if not deemed beneficial. Following the DSL approach, we decided to add diagram support to an existing language satisfying the following desiderata:

• Established in the verification community and supported by state-of-the-art, open-source tooling for VC generation and automatic theorem proving.

• Able to lexically combine box diagrams with the language’s own syntax.

• Able to represent diagrams as data types, avoiding error-prone lexical translation stages and enabling use of diagrams in proofs.

• Tooling supports automatic reduction of VCs containing diagrams into their logical equivalences, e.g., by rewrite rules.

Consequently, we chose Why3 [11], an open-source platform¹ for deductive program verification consisting of a specification language, an ML-like programming language, and a common interface to multiple automatic theorem provers—including SMT solvers, the workhorses of modern program verification.

Contribution. We generalize Reynolds’s interval diagrams to mapping diagrams, formally partial functions from a set of disjoint integer intervals to any type. Colorings constitute a subset of mapping diagrams, labeling intervals from a finite set (“palette”) of colors. We introduce the legend construct for attaching interpretation to colorings. Intuitively, colorings specify labeled selections, e.g., “all integers between 0 and l are red” and “all indexes in the array are green”, while legends express quantified predicates like “x is not among the red elements”, “all red elements are greater than all green elements” and “all green elements are sorted”. We show that colorings and legends are automatically reducible to universally quantified predicates. We have implemented an extension to the Why3 theorem prover to support diagrams similar to those shown in the introduction. The extension consists of a DSL allowing partition and mapping diagrams to be used in Why3 theories and programs, and a Why3 theory encoding partition and mapping diagrams as a data type together with the functions and predicates defining their semantics. The diagram syntax is character-based and does not require sophisticated editor support. All properties have been mechanically proved in Why3 using its underlying theorem provers. We demonstrate the DSL by verified code examples.

Notational Conventions. We give the semantics of diagrams in first-order predicate logic with partial expressions. While the Why3 logic is total and requires a parametric data type ($\texttt {option}$) for expressing partiality, we describe the general semantics using partial expressions for brevity. We denote by the operator $\mathsf {def\;}$ definedness of a partial expression, and by $=_{\exists }$ the existential equality relation between two partial expressions $e_{1}$ and $e_{2}$ satisfying

$$ e_{1}=_{\exists }e_{2}\hat{\equiv }\mathsf {def\;}e_{1}\wedge \mathsf {def\;}e_{2}\wedge e_{1}=e_{2} $$

In syntax definitions we adopt the convention that the meta-variables A and B stand for integer expressions, Q stands for Boolean expressions (predicates), E and F stand for expressions of other types, and X stands for identifiers. Subscript variables (e.g., $A_{1}$, $A_{2}$) are considered separate meta-variables of the same class. For sequences of identifiers, we write $\bar{X}$. We write $E^{?}$ to indicate that an expression may be omitted in a syntactic context, and we semantically handle absence by partiality. We indicate by E[X] that X is a free variable in E. When E[X] occurs as a subexpression we assume that adjacent subexpressions do not contain free occurrences of X; for instance, in the syntax definition $Q_{1}[X]\wedge Q_{2}$, the Boolean expression $Q_{1}$ may contain free occurrences of X whereas $Q_{2}$ may not. We write $\lambda X(E[X])$ for the anonymous function of variable X to value E. Other logic and arithmetic operators are the standard ones.

Overview of Paper. The rest of the paper is structured as follows. Section 2 describes interval and partition diagrams. Section 3 generalizes interval diagrams to mapping diagrams and colorings. Section 4 introduces the legend notation for assertions over colored intervals. Section 5 describes a tool extension allowing diagrams to be used in Why specifications. We illustrate use of this tool by example in Sect. 6. We review related work in Sect. 7 and conclude the paper with a discussion of lessons learned so far and possible future research directions in Sect. 8.

2 Interval and Partition Diagrams

Reynolds [16] introduces two interpretations for the pictogram : as an interval diagram, standing for the (possibly empty) integer interval $\{x\mid A_{1}<x\le A_{2}\}$, and as a partition diagram, standing for the predicate $A_{1}\le A_{2}$. This dual interpretation reflects the close semantical relationship between intervals and partitions. As diagrams are formulas, the intended meaning can in practice always be determined from the context: in a set-theoretic context it is an interval diagram, whereas in a logical context it is a partition diagram. Note that when $A_{1}=A_{2}$ the partition diagram is universally true and the interval diagram represents the empty interval.

The form is called the normal form of an interval or partition diagram, where both bounds are written to the left of the corresponding adjacent vertical lines, called dividing lines. Alternatively, either or both bounds of a diagram may be written to the right of the dividing line to offset the bound by 1. This means that the bound “$A-1|$” can be equivalently written as “|A”. Below we list the alternative forms together with the corresponding normal forms and meanings as interval and partition predicate:

Note that when interpreted as partition diagrams, and are equivalent, whereas when interpreted as interval diagrams, they represent different intervals. As a shorthand, we may write to denote the singleton interval containing only A:

When considered a partition diagram, is a tautology. However, the singleton form is still useful as a component of general partition diagrams. These consist of multiple chained partition diagrams that share dividing lines so that the right bound of the predecessor becomes the left bound of the successor. The following definition formalizes this notion.

Definition 1

A general partition diagram is a sequence of n (where $n\ge 1$) component partition diagrams, with $n+1$ integer bounds $A_{0},\dots ,A_{n}$, asserting that these partition the total interval into n disjoint and connected component intervals:

(Here the fragment is meta-syntax standing for any number of intermediate component intervals; it is not part of the actual diagram syntax).

While each component diagram in Definition 1 is given on normal form (where each component interval bound is written to the left of the dividing line), as with the basic partition diagrams, a bound may be written on the opposite side of the dividing line to offset it by 1. We illustrate this with two examples.

Example 2.1

The partition diagram corresponding to the partial binary search invariant discussed in Sect. 1, , has the equivalent normal form and stands for the predicate $0\le l\le u+1\le n$ (equivalently $-1\le l-1\le u\le n-1$).

Example 2.2

The partition diagram has the equivalent normal form and stands for the predicate $0\le k\le n$ (equivalently $-1\le k-1\le k\le n$).

We note that Definition 1 is stricter than Reynolds’s original definition, which considers the diagram true also when $A_{0}\ge A_{1}\ge \dots \ge A_{n}$. I.e, in the original notation an empty partition may be specified with a left bound exceeding the right bound (i.e., $A_{i}>A_{i+1}$). Reynolds calls such diagrams irregular representations of the empty interval. Our definition allows only for what Reynolds refers to as regular representations of empty intervals (i.e., $A_{i}=A_{i+1}$), and a partition diagram is always false if any $A_{i}>A_{i+1}$. The stricter interpretation has the advantages that the basic partition diagram with two bounds constitutes a meaningful assertion by itself (rather than a tautology), and that the cardinality of an interval diagram is $A_{2}-A_{1}$ when its corresponding partition diagram is true. Unlike for partition diagrams, Reynolds does not define a chained form for interval diagrams.

3 Mapping Diagrams and Colorings

Next we introduce mapping diagrams, a generalization of interval diagrams to partial functions from the integers. A mapping diagram consists of a sequence of mapping components. A mapping component , where E is a total expression over the integer parameter X to some type T, stands for the function $\lambda X(E)$ from the domain to the range T.

Definition 2

A general mapping diagram is a sequence of mapping components that stands for the union of the corresponding functions:

We note that when the corresponding partition diagram is true, the union of tuples is a partial function (as the domains of the component functions are disjoint). This is a side condition of the definition that we always verify when introducing a mapping diagram. In the diagram, an expression $E_{i}$ may be omitted to indicate that the mapping is undefined on the interval .

Property 3.1

A mapping diagram with bounds $A_{0},\dots ,A_{n}$ and expressions $E_{0},\dots E_{n-1}$ is well-defined in each point of each interval i where $E_{i}$ is present, and undefined in each point on each interval j where $E_{j}$ is absent as well as in each point outside of the total interval .

Example 3.1

The mapping diagram stands for the following partial piecewise defined function: $\lambda k{\left\{ \begin{array}{ll} -k &{} \text {if }a<k\le b\\ k &{} \text {if }c<k\le d \end{array}\right. }$. The function is undefined on the interval .

Definition 3

A coloring is a mapping diagram where each component interval is either unmapped, or mapped to a member of a set of labels (colors) C:

In the above, each $E_{i}\in C$ if $\mathsf {def\;}E_{i}$.

The term coloring reflects the use of colors for marking intervals of interest in box diagrams. In particular, we will use colorings to assert a given predicate (specified with the legend construct described in the next section) over one or more intervals.

Property 3.2

A coloring $col$ with component bounds $A_{0},\dots ,A_{n}$ maps each point in an interval with a defined color to that value. That is, for each interval j, $0\le j<n$:

$$ \forall k\left( A_{j}<k\le A_{j+1}\wedge \mathsf {def\;}E_{j}\Rightarrow col(k)=E_{j}\right) $$

Example 3.2

The coloring stands for the following piecewise defined partial function: .

4 Legends

A legend defines the interpretation of a coloring by a parametric, universally quantified assertion over all intervals colored in accordance with the legend.

Definition 4

A legend is a binding expression over a sequence of integer variables $\bar{X}$ associating a coloring with bounds $A_{0}[\bar{X}],\dots ,A_{n}[\bar{X}]$ and colors $E_{0},\dots ,E_{n-1}$ of type C to a predicate $Q[\bar{X}]$:

It stands for the following parametric predicate where the parameter $r\in \mathbb {Z}\rightarrow C$:

Informally put, the legend states that Q is true for a partitioning if the parameter function r returns the prescribed color value in every point of each colored component (on uncolored component intervals, the value of r is ignored).

Example 4.1

The legend “” stands for the following parametric predicate over r:

Example 4.2

The legend “” is equivalent to the following parametric predicate over r (the predicate has been simplified):

Informally, Example 4.1 states that x is not among the elements of the array a colored , while Example 4.2 states that the elements of a at ordered index pairs i, j colored are sorted in nondecreasing order (regardless of coloring of interjacent indexes). To use a legend in expressing a state assertion, we apply it to a coloring function over the state space of the program we are specifying.

Example 4.3

Applying the legend given in Example 4.1 to the coloring reduces to an assertion that the subarray $a[0],\dots ,a[l-1]$ does not contain the value x:

An important design consideration has been that using legends and colorings when writing assertions should not result in formulas that make automatic verification more difficult compared to equivalent assertions written in traditional quantifier notation. As the inner quantification in the legend definition and the color type C are syntactic artifacts of the DSL, they should preferably be eliminated from the correctness formula before applying SMT solvers or other ATPs. To achieve this, our tool applies to each formula an elimination rule that rewrites terms of the form $lgd ( col )$, where $lgd$ is a legend and $col$ is a coloring. The following proposition formalizes the elimination rule.

Proposition 1

Given the legend

and the coloring

the following equivalence holds for the application $lgd (col)$:

$$ lgd (col)\equiv \forall \bar{X}\left( \bigwedge _{j=0}^{n-1}\left( A_{j}\le A_{j+1}\wedge (\mathsf {def\;}E_{j}\Rightarrow \mathsf {contains\;}(A_{j},E_{j},A_{j+1}, col ))\right) \Rightarrow Q\right) $$

where $\mathsf {contains\;}$ is defined recursively on the structure of mapping diagrams:

Proof

$\Leftarrow$ by structural induction on $col$ and Property 3.2, $\Rightarrow$ by transitivity of $\mathsf {contains\;}$ and induction over an integer interval.

Note that the definition of $\mathsf {contains\;}$ involves only Boolean connectives, integer comparison, and color terms of the form $e=_{\exists }E$. When e and E are literal color values (or absent), the equality $e=_{\exists }E$ can be immediately evaluated, reducing the inner quantification of the legend to a propositional formula where the atoms are linear integer constraints.

5 Diagram Extension to the Why3 Verification Platform

We have developed a prototype extension Why3 supporting mechanically proving meta-properties like Proposition 1 as well as specifying programs with partition and mapping diagrams. We first briefly present relevant features of the Why3 platform and then describe our implementation. The implementation is available in source form at https://gitlab.com/diagrammatic/whyp.

The Why3 Platform. The Why3 specification language is a first-order logic extended with polymorphic types and algebraic data types. Theorems can be proved using over a dozen supported automatic and interactive theorem provers. Users interact with Why3 in batch mode through a command-line interface, or interactively through a graphical IDE. In addition to the purely logical specification language, programs with loops, mutable variables, and exceptions can be written in the WhyML language. Why3 generates VCs from WhyML programs based on weakest preconditions. A good example-driven tour of Why3 is given by Bobot et al. [6]. Why3 provides a set of transformations on verification tasks, including definition inlining, application of rewrite rules and logical inference rules. The Why3 drivers for external theorem provers employ these to transform the sequent into a form amenable to automation, for instance by eliminating language features that are not supported by the target prover (e.g. algebraic data types). Other transformations are intended to be used interactively to reduce a goal into one or more subgoals, e.g., proof-by-cases, instantiation, and induction. Why3 is designed to both be a backend for other tools as well as an extensible verification platform. It comes with a standard library of theories which can be reused through an importing mechanism. The platform itself can be extended with different kinds of plug-ins adding new input formats, prover drivers and other extensions. The core of Why3 is implemented in OCaml and is offered as a software library for programmatic access to all platform functionality, including parsing, typing, transformations, and invocation of external theorem provers.

Extension Architecture. The extension to Why3 consists of two components: a set of Why3 theories formalizing partition diagrams and mappings, and a syntactic preprocessor (written in OCaml) that translates the concrete diagram syntax into Why3 terms. Figure 1 shows the data flow when the user asks the tool to check a theory containing diagrams (indicated by the theory existing in a file with the suffix .whyp). The preprocessor parses the input theory and translates all partition diagrams, mapping diagrams and legends into normal form and then into instances of a data type defined in the theory extension. The resulting AST is dispatched to Why3 for typing, inclusion of standard library theories, task generation, and external theorem prover execution. From here onwards the data flow is identical to that of checking a normal Why3 theory. Next, we describe the concrete diagram syntax and the embedding of the diagrams in the Why3 logic.

Fig. 1.

Processing pipeline of Why3 extension

DSL Syntax and Semantics. The DSL follows the ASCII-based lexical rules of Why3 [5]. A partition diagram must be enclosed in square brackets ‘$\texttt {[}$’ and ‘$\texttt {]}$’, and vertical dividing lines are written as ‘$\texttt {|}$’. The leftmost or rightmost vertical line may be omitted when it would be adjacent to a square bracket. The bounds themselves follow the syntax of Why3 terms. Mapping diagrams must be enclosed in and (the binder may be omitted for colorings). The ellipsis ‘$\texttt {...}$’ separates bounds inside a component, and in mapping diagrams may be followed by ‘$\texttt {\#}$’ and an expression. The following are examples of accepted ASCII partition and mapping diagrams and their diagrammatic equivalents:

Partition and mapping diagrams may occur in a Why3 theory anywhere a term is expected. After parsing, both types of diagrams are translated into instances of the polymorphic data type :

The data type represents partition diagrams in normal form; the preprocessing hence includes a normalization stage, converting each ‘$\texttt {|}e$’-fragment into ‘$e\texttt {-1|}$’ and each ‘$\texttt {|}e\texttt {|}$’-fragment into ‘$e\texttt {-1|}{} \texttt {...}e\texttt {|}$’, before finally converting the result into an instance of the above data type. The data type from Why3s standard library is used to handle partiality. It has two constructors, and . For partition diagrams, the second parameter is always . For mapping diagrams, it is for each interval associated with an expression of type , otherwise . The semantics of partition diagrams is given by the predicate $\texttt {partitioning}$:

and for mapping diagrams by the function $\texttt {mapping}$:

The declarations instruct Why3 to use the above definitions as rewrite rules when transforming a proof task in preparation for sending it to an external theorem prover. The rewrites are applied recursively and exhaustively, viz. $\texttt {partitioning}$ is rewritten into a conjunction sequence and $\texttt {mapping}$ into a nested -expression. This is normally desirable when using diagrams for specification; only when proving meta-theorems about partition and mapping diagrams may we want to suppress automatic rewriting.

A legend is declared with the keyword followed by an identifier, a sequence of parameters and a semicolon-separated list of coloring-to-predicate mappings. The preprocessor translates the legend into a conjunction of universally quantified statements according to Definition 4. For example, the legend:

is translated by the preprocessor into the following Why3 predicate:

For automatic elimination of the inner quantification and color-typed terms in a legend applied to a coloring, as described in Sect. 4, the $\texttt {partitioning}$ theory includes the following lemma declared as a rewrite rule:

Here $\texttt {contains}$ is defined as in Proposition 1. The rewrite is automatically applied (from left to right) by Why3 when executing the $\texttt {compute\_specified}$ and $\texttt {compute\_in\_goal}$ transformations on a goal. The default strategy of the extended Why3 verifier applies these transformations prior to invoking the user’s back-end theorem prover of choice.

6 Verified Code Examples

In this section we present three formally specified and verified procedures where the pre- and postconditions and loop invariants are expressed as diagrams. The procedures are specified in the WhyML language with the diagram extensions described in Sect. 5, and all VCs were proved automatically by a combination of Z3 [7], CVC4 [3] and Alt-Ergo [4] after preprocessing by our tool.

A classical example of using the coloring analogy in verification is the Dutch National Flag problem introduced by Dijkstra [9]. It is a simplified sorting problem: an array containing, in random order, any number of each of the three values blue ( ), white ( ), and red ( ) should be rearranged so that the blue elements precede all the white elements, which in turn precede all the red elements (i.e., the final order is , , ). Listing 1 shows an adaptation of an existing Why3 solution², in which we have replaced the textual postcondition ( clauses) and loop invariant ( clauses) with diagrammatic equivalents. The procedure executes in time linear to the size of the array and mutates the array by pairwise compare and swap. The loop invariant consists of three components: a partition diagram constraining the values of the loop variables , and ; a coloring mapping the intervals , and to , and , respectively; and a (non-diagrammatic) assertion that the modified array is a permutation of the original. The operation and the predicate are imported from the Why3 array library together with the property that the former maintains the latter. The program is atypical in that the color values, represented by the datatype , are not pure specification constructs but also occur in the computation itself. The legend is trivial due to the nature of the program; it simply asserts that is elementwise equal to the coloring on the intervals on which the latter is defined.

Listing 2 shows a verified implementation of binary search with a diagrammatic postcondition and loop invariant similar to the invariant discussed in the introduction. The procedure determines the presence of the value in the sorted input array . It has two exits, one normal and one abnormal. If is found in , the procedure exits normally returning an index containing (in Why3, normal return values are represented by the variable in the postcondition specification). If is not found in , the procedure exits abnormally in the exception carrying the associated postcondition that all elements of are different from . To express the specification and invariants diagrammatically, we introduce two legends for the specification of binary search: , expressing sortedness of the -colored range; and , expressing existence ( ) or absence ( ) of the sought element .

The final example, Listing 3 shows an implementation of a simple sorting algorithm, insertion sort. The procedure sorts the input array by maintaining two partitions, one sorted partition ranging from index to , followed by one unsorted partition ranging from to the end of the array. Each iteration of the outer loop extends the sorted partition by one element, until the whole array is sorted. The outer loop invariant is expressed by the partition diagram and the coloring . The first component of the legend for -colored intervals is identical to the one introduced in Listing 2. In order to achieve sortedness of the first interval after incrementing , the inner loop moves the element at index backwards into its final position in the sorted partition by repeatedly swapping it with its predecessor using the loop counter . During the execution of the inner loop, the outer loop invariant is temporarily invalidated: the interval is almost sorted, but with the exception of a single potential inversion of elements at indexes and . Diagrammatically, this is expressed by the index being colored by , and the second component of the legend specifying that any -colored element followed by an -colored element constitutes a sorted pair.

7 Related Work

Partition and interval diagrams were originally proposed by Reynolds [16], who used them extensively in the specification and verification of several array-manipulating programs in his textbook The Craft of Programming [17]. Notably, Reynolds gives a formal syntax and a set of manipulation rules for the diagrams to facilitate their use as terms in calculational correctness proofs. Reynolds writes universally quantified invariants using the standard $\forall$-operator and gives the quantification domain as an interval diagram, rather than making the quantification implicit in the diagrammatic notation itself. Many textbooks, e.g. [12, 18], use similar box diagrams (termed “array pictures” or “array diagrams”) in the presentation of assertions over both array indexes and array elements, but most of them do not formalize their semantics fully. Astrachan [1] suggests diagram representations for arrays and linked lists, emphasizing the role of diagrams in comprehension. Generating visual representations from textual specifications has been addressed in the context of the Z language [14]. Similar diagrams have also been proposed for visualizing array VCs [13], as an aid to proof and debugging. Wickerson et al. [19] employ partition-like diagrams in the visual proof notation called ribbon proofs for separation logic. Pearce [15] explores through a number of examples how array-based programming is enhanced by languages which support specifications and invariants over arrays. Invariant-based programming [2] is a correct-by-construction formal method aimed at teaching in which programs and their proofs are constructed diagrammatically, often with the aid of partition diagram-like pictures during the initial stages of construction. The idea of colorings and legends also originates from the authors’ previous joint work with R-J. Back [10]. We are not aware of existing work on integrating partition or interval diagrams into a general-purpose program verification platform.

8 Conclusions and Future Work

This paper approaches box diagrams from the viewpoint that they can serve as an expressive formal mini-language—a DSL—rather than being restricted to their traditional role of ephemeral pre-code sketches and post-code visualizations. We have introduced an extension to Reynolds’s original partition and interval diagrams for piecewise definition of partial functions over integer intervals, and a legend construct for asserting a predicate over a sequence of labeled (“colored”) intervals. We have extended Why3 to read diagrammatic syntax and formalized its semantics in a Why3 theory.

We believe that the value of a formal specification is largely dependent on its legibility, as the specification cannot be proved correct (only checked for internal consistency), but is instead subject to human assessment of fitness for purpose (validation). Also, although significant advances have been made in automatically synthesizing invariants from the code, such techniques cannot discover difficult invariants, meaning that the same requirement of legibility applies to these as well. Good notation makes writing readable assertions more tractable, and while notation by itself may not be the primary challenge of verification, it is nevertheless held in high regard among verification practitioners. In particular, we have observed a tendency among the experienced to write integer range and array predicates following idioms that serve similar organizational purposes as the diagrams proposed herein, such as chaining relational operators and maintaining increasing order of bounds from left to right, preferring the relations < and $\le$ over > and $\ge$. Formalizing such idioms is where a DSL and tool support can be of value. However, diagrammatic languages requiring sophisticated tool support and considerable learning investments from users are hard to justify for niche domains. The authors believe that the DSL presented here achieves a sensible compromise between expressive power and ease of integration. During implementation of the tool support, we came to appreciate both the semantically rich Why3 and WhyML languages and the extensibility of the Why3 platform through its API. The one feature we missed was a way to extend the Why3 language in a modular fashion, e.g., by adding new term productions while leaving the rest of the grammar intact, rather than by modifying its parser.

Finally, we emphasize that our goal has not been to address all aspects of array reasoning. The authors have found the DSL useful when writing array invariants that involves partitioning, but do not make further claims regarding its general applicability. There are classes of array invariants for which the DSL is not a sensible choice: clearly, assertions not involving partitions may have little to gain, and assertions with multiple nested quantifications may find the legibility advantage being lost. A lightweight DSL has the advantage that we can restrict its use to specification tasks for which we deem it beneficial, and fall back to standard FOL notation in other cases. Hence we believe the DSL’s primary role is to ease writing of certain classes of array and integer range properties, viz. those that involve partitioning and universal quantification. We surmise that the class of programs involving such properties is large enough that a DSL like the one presented here could justify its place in the modern verification toolbox.

Future Work. There is scope for much further work on partition, interval and mapping diagrams, both in improving tool support and in generalizing the notation itself. The tool is in the first prototype stage and has so far only been tested on a small collection of toy examples. We have identified enhancements and optimizations that will be required to address real-world requirements. For instance, the diagram syntax is currently not supported in the Why3 IDE during interactive proofs. Also, the $\mathsf {contains\;}$ rewrite should be optimized, as it currently expands a diagram into a formula that is exponential in the length of the diagram chain (this has not been an issue in practice with typical diagrams, but prevents larger diagrams from being processed). More experiments will be needed to gain more experience with the notation and identify potential pitfalls, and a comparative study with real users is necessary to experimentally assess the merits of the DSL over regular FOL notation. Finally, we are also looking into extending the diagram notation beyond the domain of integers, in particular to non-linear structures in order to reason about multi-dimensional arrays, trees and graphs.