Type casting

This example shows how a binary tree with internal <code>Node</code> and <code>Leaf</code>s can be specified if access is by means of casting rather than through a visitor pattern.

General Information

Backend: Silicon
Language: Java
Features: Trees
Path to Example File: type-casts/CastExample.java
Should Verify: Yes
Date: 2017-06-21
Lines of Code: 62 (comments not included)
Lines of Specification: 25 (40.3% of total)
Computation Time: 24.2 seconds

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases CastExample
//:: tools silicon
//:: verdict Pass

/**
  This example shows how a binary tree with internal <code>Node</code>s
  and <code>Leaf</code>s can be specified if access is by means of casting
  rather than through a visitor pattern.
*/
class Node {
  int key;
  Object left;
  Object right;
  
  //@ requires Test.state(left) ** Test.state(right);
  //@ ensures Test.state(this);
  public Node(int key,Object left,Object right){
    this.key=key;
    this.left=left;
    this.right=right;
    //@ assert this instanceof Node;
    //@ assert !(this instanceof Leaf);
    //@ fold Test.state_rec(this);
  }
  
}

class Leaf {
  int other;
}

class Test {

/*@
  static inline resource state(Object t) = t != null ** state_rec(t);
    
    
  static resource state_rec(Object t) = t != null **
    (t instanceof Leaf || t instanceof Node) **
    (t instanceof Leaf ==> Perm(((Leaf)t).other,1)) **
    (t instanceof Node ==>
       Perm(((Node)t).key,1) **
       Perm(((Node)t).left,1) ** state(((Node)t).left) **
       Perm(((Node)t).right,1) ** state(((Node)t).right)) ;
@*/

/*@
    requires state(tt);
  @*/
  int find(Object tt,int key){
    Object t=tt;
    /*@
      loop_invariant state(t);
    @*/
    while(t instanceof Node){
      Node n=(Node)t;
      //@ unfold state_rec(n);
      if (key < n.key){
        t=n.left;
      } else {
        t=n.right;
      }
    }
    //@ unfold state_rec(t);
    Leaf l=(Leaf)t;
    return l.other;
  }

}

Language: