Inverting an Injection

July 1, 2012 – 4 years, 9 months ago, by vladimir

Short Description

Invert an injective array A on N elements in the subrange from 0 to N − 1, i.e., the output array B must be
such that B[A[i]]=i for 0<=i< N.

Code

int A[];
for (i=0; i<N; i++){
  B[A[i]] = i
}

Specification

Show that the resulting array is also injective. For bonus points, you can demonstrate other properties, e.g., that A and B are inverses.

You can assume that A is surjective.

Long Description

Supplementary Materials

Test: If A is 9, 3, 8, 2, 7, 4, 0, 1, 5, 6, then output B should be 6, 7, 3, 1, 5, 8, 9, 4, 2, 0.

This problem was posed at the VSTTE'10 verification competition by Peter Müller <Peter.Mueller@inf.ethz.ch> and Natarajan Shankar <shankar@csl.sri.com>.

If you want to attach a file, please attach to this page and post a link here.

Submitted by

Vladimir Klebanov <verifythis@cost-ic0701.org>


Solution

Tool/Method

KeY. A developer version was used, which contains bugfixes that will be part of the upcoming 1.6 release. In the meantime, the particular version can be accessed via web start here.

Code/Specification

Straight-forward JML specification.

Solution-problem relationship

Preconditions worth mentioning: injectivity and surjectivity of the source array.

Postconditions proved: injectivity of the target array, inverse relationship between source and target, assignable clause.

Interactivity, effort needed

The problem was solved by the KeY team during the VSTTE'10 competition.

Two quantifiers were instantiated interactively.

Z3 was used to discharge 5 goals.

How to reproduce

You can load the evidence files (*.proof) into the web start version of KeY linked above. This will provide you with a complete proof script in dynamic logic.

Published

http://www.vscomp.org/home/

Submitted by

Vladimir Klebanov <verifythis@cost-ic0701.org>


Solution

Tool/Method

Holfoot / partial correctness proof using separation logic inside HOL 4

Code/Specification

The code is written in Holfoot's imperative programming language, which is a tiny subset of C. The specification requires procedure specifications as well as a specification of the loop. Since this tiny subset does not support for-loops, it is replaced by a while-loop. Moreover, an auxiliary variable is used to hold the value of A[i].

Solution-problem relationship

The solution translates the program into a functional program on lists. For this purpose, a function
VSCOMP2_FUN is defined, that captures the behavior of the program exactly.

val VSCOMP2_FUN_def = Define `
  (VSCOMP2_FUN l i [] = l) /\
  (VSCOMP2_FUN l i (n::ns) =
      VSCOMP2_FUN (REPLACE_ELEMENT i n l) (SUC i) ns)` 

It is simple to prove that the code implements this function. The interactive proof-script basically calls the automation and the rewrites with the definition of VSCOMP2_FUN. Then, interesting properties are proved as lemmata on VSCOMP2_FUN, i.e. in a purely functional setting. The inversion property is for example stated by the following HOL 4 - theorem (notice i = 0 in the postcondition of the procedure specification):

val VSCOMP2_FUN___EL = prove (
``!l1 i l2.
  EVERY (\x. x < LENGTH l2) l1 /\
  ALL_DISTINCT l1 ==>

  (!n. n < LENGTH l1 ==>
   (EL (EL n l1) (VSCOMP2_FUN l2 i l1) = n+i))``,
...

Interactivity, effort needed

Most of the effort was in fact interactive. Translating the program to a functional specification is straightforward and required perhaps 10 minutes. Then you can spend as much time and efford as you want to prove interesting properties of VSCOMP2_FUN. I spend perhaps 30 minutes and proved the above statement on injection, some similar lemmata and some rewrite rules.

How to reproduce

The example is available with Holfoot. It is easiest to use the Webinterface to run the example. However, one can download the sources and run the example inside HOL 4 as well.

Published

Submitted by

Thomas Tuerk


Solution

Author

Rosemary Monahan and Nadia Polikarpova

Tool/Method

Boogie2

Code/Specification

Boogie2 is an intermediate verification language designed to accommodate the encoding of verification conditions for imperative, object-oriented programs.

Solution-problem relationship

Proving that one array is an inversion of another simply requires the addition of an obvious loop invariant. Proving that an array is injective is more complicated. The main difficulty was making Boogie instantiate the surjectivity precondition.

Instead, we introduced a ghost set mirroring all seen values of the array and loop invariants stating that the set cardinality is exactly k (k being the loop counter) and that all elements are in [0;N).
To this end, we formalized a small theory of sets.

We did not prove termination for any of the problems as Boogie2 does not directly support termination measures.

Interactivity, effort needed

The problem was solved for the experience report in the aftermath of the VSTTE'10 competition.

How to reproduce

The solution can be found on the webpage. It includes the file "problem2.bpl" which can be run with the Boogie2 tool.

Published

http://www.vscomp.org/

Submitted by

Sarah Grebing (based on the competition experience report published on the webpage)


Solution

Author

K. Rustan M. Leino

Tool/Method

Dafny

Code/Specification

Dafny is an object-based language with built-in specification constructs.
To a first approximation, it is like Java (but without subclasses) with Eiffel- or JML-like specifications. Language features that are especially useful when writing specifications include sets and sequences, ghost variables, and user-defined recursive functions.
Dafny uses mathematical integers (implemented by big-nums), which avoids overflow errors.

Solution-problem relationship

The difficulty with problem lies in getting the SMT solver to make use of the given surjectivity property. The general trick is state a lemma, an assert statement whose condition supplies the reasoning engine with a stepping stone in the proof. In particular, the lemma will mention terms that trigger reasoning about quantifiers that also mention those terms. In this problem, the surjectivity property does not contain any terms that can be used in a lemma, so I introduced a dummy function for that purpose.

Interactivity, effort needed

The problem was solved for the experience report in the aftermath of the VSTTE'10 competition.

How to reproduce

The solution can be found on the webpage. It includes a file "VSComp-Leino-2.dfy" which can be run with the Dafny tool.

Published

http://www.vscomp.org/

Submitted by

Sarah Grebing (based on the competition experience report published on the webpage)