Amortized Queue

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

Short Description

An applicative queue with a good amortized complexity can be implemented using two linked lists. Verify such a queue.

Code

The queue structure supports the operations (pseudocode to follow)

  • Enqueue(item: T): Place an element at the rear of the queue
  • Tail(): Return the queue without the first element
  • Front(): Return the first element of the queue.

The queue is implemented as a record with two fields: front and rear which are linked lists. The Front operation returns the first element in the list front. Tail returns a new queue where the head element of the front list has been removed (i.e., the new front is the linked-list tail of the original front list). The Enqueue operation teturns a new queue by inserting an element at the head of the list rear.

Intuitively, the queue can be understood as the front list concatenated with the reverse of the rear list.

Also, whenever a client wants to remove an element from the queue and the front list is empty, the content of the rear list has to be moved to the front list (in reverse order).

Specification

  • You have to show that the implementation maintains the invariant that queue.rear.length <= queue.front.length.
  • You also have to show that a client invoking these operations observes an abstract queue given by a sequence.

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

Code/Specification

The progam is written in Holfoot's imperative programming language. This language does not support object orientation. Therefore, the program consists of a number of
procedures that explicitly get a pointer to the object and modify the object somehow.

Solution-problem relationship

Since Holfoot does not support object-orientation, the program does only loosely connect to the original problem. Holfoot is a separation logic tool and build to work on date-structures like single-linked lists. Therefore,
auxiliary procedures about lists can be proved very easily. Amortized queues are a bit trickier. In order to attack this problem, a predicate for amortized queues is added to Holfoot. This can be done by the user. However, the definition in HOL syntax is lengthy:

val holfoot_ap_amortized_queue_def = Define `
   holfoot_ap_amortized_queue strong tl q dta data =
   asl_exists f r f_data r_data. asl_bigstar_list holfoot_separation_combinator
      [holfoot_ap_points_to q (LIST_TO_FMAP [				   
           (holfoot_tag "front", var_res_exp_const f);
           (holfoot_tag "rear", var_res_exp_const r);
           (holfoot_tag "front_length", var_res_exp_const (LENGTH f_data));
           (holfoot_tag "rear_length", var_res_exp_const (LENGTH r_data))]);
       holfoot_ap_data_list tl (var_res_exp_const f) [(dta, f_data)];
       holfoot_ap_data_list tl (var_res_exp_const r) [(dta, r_data)];
       var_res_bool_proposition DISJOINT_FMAP_UNION 
           ((data = f_data ++ (REVERSE r_data)) /\
            (strong ==> (LENGTH r_data <= LENGTH f_data)))]`

This definition defines a predicate "holfoot_ap_amortized_queue(strong, q, data)" to hold, if q points to a record in the heap with entries

  • front: f
  • rear: r
  • front_length: fl
  • rear_length: rl

such that

  • f points to a single linked list of length fl with data f_data
  • r points to a single linked list of length rl with data r_data
  • data = APPEND f_data (REVERSE r_data)
  • strong ==> rl <= fl

This new predicate is given to the pretty printer and parser. The parser recognised now amortized_queue(q, data) where strong is true and weak_amortized_queue(q,data) used for the normalize procedure where strong is false.

Interactivity, effort needed

In order to have nice, readable specifications, the parser and pretty printer were extended. This took 30 minutes. The proof itself is mainly automatic. It consists of expanding the definition of amortized queues, calling the automation and in the case of the dequeue procedure to a manual case split on whether the front is empty. It took less than 5 minutes to write these proof scripts.

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

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

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

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 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 "AmortizedQueue.java" which can be run with the tool.

Published

http://www.vscomp.org/

Submitted by

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


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

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

This Problem delivered a more interesting experience as theories of sequences and heap allocation were required. These were not difficult to specify but were quite labor-intensive. However, once these theories have been written, it is possible to solve a whole range of similar problems, so the effort is not wasted.

Our theory of sequences developed for this problem contains several examples of proofs by induction as well as an example of proof by contradiction (lemma Sequence.zero_count_empty) which may be of interest to the reader.
When dealing with linked data structures, one typically needs to define inductive properties. We noticed that in order for Z3 to handle them effectively it is important to use induction on structure instead of induction on integers.

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 "queue.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

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

Solution-problem relationship

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)