Pictorial languages, while intuitive and descriptive, are rarely used as the primary reasoning language in program verification due to lack of precision. In this paper, we introduce a precise pictorial language for specifying array invariants that preserves visual perspicuity. The language extends Reynold's partition diagrams with the notion of a coloring, allowing assertions over portions of an array to be expressed by color-coding. The semantics of a coloring is given by a legend, mapping a colored partition of an array into a universally quantified predicate over the array. The pictorial syntax is an extension toinvariant diagrams, transition graphs where preconditions, postconditions and invariants, rather than the program code, determine the main program structure. We demonstrate the approach with three examples, verified using the Why3 theorem prover frontend.
展开▼
