Searching a Linked List

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

Short Description

Given a linked list representation of a list of integers, find the index of the first element that is equal to 0.

Code

jj = ll;
int i = 0;
while (jj != null && jj.head != 0){
  jj = jj.next;
  i++;
}
return i;

Specification

You have to show that the program returns an index i equal to the length of the list if there is no such
element. Otherwise, i'th element of the list must be equal to 0, and all the preceding elements must be non-zero.

Long Description

Supplementary Materials

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

Holfoot / partial correctness proof using separation logic inside HOL 4

Code/Specification

The program 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 requires heap lookups to be separated into single statements, the comparation "jj.head != 0" is not expressible in Holfoot. To solve this problem, auxiliary variables found and tmp are introduced. tmp hols the value "jj.head" and found indicates whether the search value has already been found. There are 4 specifications available:

The first two contain specification using just build in predicates and a loop invariant or specification respectively. The other two define a function FIRST_INDEX in HOL 4 that captures the semantics of this function. Moreover, they use a free, higher order specification variable P to abstract from the concrete search for the first 0.

Solution-problem relationship

Except from introducing auxiliary variables tmp and found the implementation is close the the pseudo code. Using the new function FIRST_INDEX, the specification looks clean and easily readable, especially Loop Specification 2. Holfoot does not prove termination, though.

Interactivity, effort needed

Tiny bit of arithmetic reasoning required. Manual definition of FIRST_INDEX and some rewrites for FIRST_INDEX. Altogether perhaps 20 minutes.

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.

Specifying heap-manipulating programs in Boogie2
requires explicitly defining the heap, so we defined the linked list by
mapping a list cell to its stored value and to the next list
cell.
Our specification included auxiliary functions which calculated
the length of the list, determined if a value was in the list,
and returned the value at a particular position in the list.

Solution-problem relationship

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 during the VSTTE'10 competition.
Solution proves automatically in about 2 seconds.

How to reproduce

The solution can be found on the webpage. It includes the file "problem3.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

To solve this problem, I associated with every linked-list node a ghost variable whose value is the sequence of list elements from that point onward in the list. To state the appropriate invariant about that ghost variable, one must account for which linked-list nodes contribute to the value, which is done using a common ``dynamic frames'' specification idiom in Dafny.

Interactivity, effort needed

The problem was solved during the VSTTE'10 competition.

How to reproduce

The solution can be found on the webpage. It includes a file "VSComp-Leino-3.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)


Solution

Author

Vladimir Klebanov, Mattias Ulbrich and Benjamin Weiß

Tool/Method

KeY. An automated/interactive tool for Java source code verification using dynamic logic.
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

This solution is inspired by the Dafny solution submitted by Rustan Leino. It uses a recursively defined invariant instead of a reachability predicate for dealing with the recursive nature of the linked list datastructure. A "sequence" abstract data type has been implemented in KeYHeap for this example, as well as Dafny's "limited" trick for limiting the automatic unfolding of recursive represents clauses to one level.

Interactivity, effort needed

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

How to reproduce

You can load the problem files into the web start version of KeY linked above. The proof can be done automatically.

Published

http://www.vscomp.org/

Submitted by

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


Solution

Author

Bart Jacobs, Frank Piessens and Jan Smans

Tool/Method

VeriFast
VeriFast is a verifier for single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic.

Code/Specification

Solution-problem relationship

Interactivity, effort needed

The problem was solved during the VSTTE'10 competition.

How to reproduce

The solution can be found on the webpage. It includes a file "VeriFast.java" 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)