Witnesses: Magic wand

Demo verification example that shows how magic wands can be used in verification.

General Information

Backend: Chalice
Language: Java
Features: Witnesses, Loop invariants, Magic wands
Path to Example File: witnesses/WandDemo.java
Should Verify: Yes
Date: 2017-06-21
Lines of Code: 54 (comments not included)
Lines of Specification: 31 (57.4% of total)
Computation Time: 9.6 seconds

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases WandDemo
//:: tools chalice
//:: option --explicit

/**
  The command line to verify with the VerCors Tool is:
  
  vct --chalice --explicit WandDemo.java
  
  The expected result is Pass.
*/
class WandDemo {
  int x;

/*@
    resource readonly()=Perm(x,25);
    resource writeonly()=Perm(x,100);
  @*/
  
  //@ requires r:readonly();
  public /*@ pure */ int get(){
    //@ unfold r:readonly();
    return x;
  }
  
  //@ ensures w:writeonly();
  WandDemo(){
    //@ fold w:writeonly();
  }

/*@
    requires w:writeonly();
    ensures  r:readonly();
    ensures  wand:(readonly()-*writeonly());
  @*/
  void set(int v){
    //@ unfold w:writeonly();
    x=v;
    //@ fold r:readonly();
    /*@
      create {
        unfold r:readonly();
        use    Perm(this.x,75);
        fold   w:writeonly();
        qed    wand:((r:readonly())-*(w:writeonly()));
      }
    @*/
  }
  
  void demo(){
    //@ witness wand:(readonly()-*writeonly());
    //@ witness w:writeonly();
    //@ witness r:readonly();
    WandDemo d=new WandDemo() /*@ then { w=w; } @*/;
    int i=1;
    //@ loop_invariant ww:d.writeonly();
    while(true)
    //@ with { ww = w ; }
    {
        d.set(i) /*@ with { w = ww ; } then { r=r; wand=wand; } */;
        i=(d.get()/*@ with { r=r; } @*/)+(d.get()/*@ with { r=r; } @*/);
        //@ apply wand:((r:d.readonly())-*(ww:d.writeonly()));
    }
  }
}

Language: