## 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

### 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

### 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

### 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

### Submitted by

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

## Solution

### Author

Rosemary Monahan and Nadia Polikarpova

### Tool/Method

### 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

### 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

### Submitted by

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