Maximum in a tree

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

Short Description

Given: A non-empty binary tree, where every node carries an integer.

Implement and verify a program that computes the maximum of the values
in the tree.

Code

Please base your program on the following data structure signature:

public class Tree {

    int value;
    Tree left;
    Tree right;

}

You may represent empty trees as null references or as you consider
appropriate.

Long Description

Motivation: The challenge was constructed by the organizers to explore how
tools handle heap data structures that are not lists.

Supplementary Materials

This problem was posed as challenge 2 at the COST Verification Competition 2011.
The time for solving this challenge during the competition was 90 minutes.

Submitted by

Sarah Grebing (based on the challenges given in the COST Verification Competition 2011)


Solution

Tool/Method

KeY

Author

Wojciech Mostowski and Christoph Scheben

Code/Specification

Relevant part of the JML* specification:

public class Tree {
 private int value; private /*@ nullable @*/ Tree left, right;
 /*@ ghost \locset fp; invariant fp ==
  \set_union(this.*, \set_union(
   left==null? \empty : \set_union(left.*,left.fp),
   right==null? \empty : \set_union(right.*,right.fp)));
 invariant left != null ==>
   (\disjoint (this.*, left.fp) && left.\inv);
...
 ghost \seq seq; invariant seq ==
  \seq_concat(\seq_singleton(value), \seq_concat(
   left==null? \seq_empty : left.seq,
   right==null? \seq_empty : right.seq));
 accessible \inv : fp \measured_by seq.length; @*/

The heap structure is specified with the ghost field fp, which denotes the set of
locations making up the footprint of the tree, and an invariant that structures this footprint correspondingly. The accessible clause provides a measure proving well-foundedness of the recursively defined invariant.

The integer payload of the tree is packed into a sequence in a natural way: the head of the sequence is the node of the tree, the left sub-tree follows, and then the right. The length of the sequence is the measure proving that the recursive call to the method max terminates.

Solution-problem relationship

In KeY, the solution is based on dynamic frames. Due to the linked structure of the tree and the recursive implementation of the max method, the KeY team chose to specify both the heap structure of the tree, and a flat representation of it. The heap structure definition states that trees cannot be cyclic, while the flat representation of the tree as a finite sequence of integers disallows infinite trees.

Interactivity, effort needed

The boundedness of the invariant and the structure of the footprint is proved automatically and very quickly. The first part of the top-level specification, a universal quantifier stating that the result is greater than or equal to all the elements in the tree is also quite straightforward. Up to this point, the KeY system finds all proofs automatically and within one minute.
However, the system has difficulty with the second main property: the existential
quantifier that states the presence of the result in the tree. In the automated
proof search mode the proof starts to grow uncontrollably regardless of the prover settings used. In the end, substantial manual interaction was required to guide the prover through the important cases (left and right sub-trees being null
or not) and to give it the right instantiations for the existential quantifier. This manual interaction with the prover (over 200 interactions in total) was where most of the time was spent on this challenge. The rest of the proof was done automatically and took less than a minute to finish.

How to reproduce

Published

http://foveoos2011.cost-ic0701.org/verification-competition

Submitted by

Sarah Grebing (based on the Experience report about the competition)


Solution

Tool/Method

Dafny

Author

Julian Tschannen and Nadia Polikarpova

Code/Specification

Solution-problem relationship

Memory footprints of linked data structures are commonly described in Dafny using dynamic frames. According to this idiom, the Tree class is extended with a ghost field Repr, which stores the set of all nodes in the subtree with root this. The ghost field serves multiple purposes: on the one hand, it is used to describe footprints of functions and methods, thus taking care of the frame problem; on the other hand, it serves as a termination measure for any recursion on subtrees. For the latter use, the data structure is required to be acyclic. Dafny does not support class invariants, where the acyclicity property could be stated. Class invariants are simulated by defining a predicate valid, and using it in pre- and postconditions of class methods.
To facilitate functional specifications, another ghost field Values is defined
to denote the set of all values stored in the subtree. Using this field, it is easy to specify that method max returns a value from the tree that is larger than all other values. A straightforward recursive implementation for max was provided; the only auxiliary annotation needed to verify this implementation was the termination measure.
The final version also contains a constructor: a method
that establishes the valid predicate without requiring it. Adding such a method
to any class is important in order to ensure consistency of the class invariant.

Interactivity, effort needed

How to reproduce

Published

http://foveoos2011.cost-ic0701.org/verification-competition

Submitted by

Sarah Grebing (based on the Experience report about the competition)