TY - GEN

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

AU - Eriksson, Johannes

AU - Parsa, Masoumeh

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-39197-3_13

DO - 10.1007/978-3-030-39197-3_13

M3 - Conference contribution

SN - 978-3-030-39196-6

T3 - Lecture Notes in Computer Science

SP - 196

EP - 212

BT - Practical Aspects of Declarative Languages

PB - Springer

ER -