Witnesses: Predicates

This example shows how reasoning with explicit witnesses works. It is supposed to work with Chalice, but the assertions are not proven.

General Information

Backend: Silicon
Language: Java
Features: Witnesses
Path to Example File: witnesses/predicates.pvl
Should Verify: Yes
Date: 2017-06-21
Lines of Code: 50 (comments not included)
Lines of Specification: 25 (50.0% of total)

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: cases PredicatesAndWitnesses
//:: tools
//:: options --explicit
/*@
  This example shows how reasoning with explicit witnesses works.
  It is supposed to work with Chalice, but the assertions are not proven.
@*/

class predicates {

int val;

resource state(frac p)=Perm(val,p);
  
  given frac p;
  requires req:state(p);
  int get()=val;

ensures  res:state(100) ** get(p:100,req:res)==v;
  predicates(int v){
    val=v;
    fold res:state(100);
    assert get(p:100,req:res)==v;
  }

requires req:state(100);
  ensures  res:state(100) ** get(p:100,req:res)==v;
  void put(int v){
    unfold req:state(100);
    val=v;
    fold res:state(100);
    assert get(p:100,req:res)==v;
  }

given    frac p;
  requires req:state(100) ** ptr!=null ** req_p:ptr.state(p);
  ensures  res:state(100) ** ptr!=null ** res_p:ptr.state(p) ** get(p:100,req:res)==ptr.get(p:p,req:res_p);
  void copy(predicates ptr){
    res_p=req_p;
    unfold req:state(100);
    val=ptr.get(p:p,req:res_p);
    fold res:state(100);
    assert get(p:100,req:res)==ptr.get(p:p,req:res_p);
  }
  
  void main(){
    predicates ptr1;
    predicates ptr2;
    witness st1:state(1);
    witness st2:state(1);
    ptr1=new predicates(37) then { st1=res; };
    assert ptr1.get(p:100,req:st1)==37;
    ptr2=new predicates(12) then { st2=res; };
    assert ptr1.get(p:100,req:st1)==37;
    assert ptr2.get(p:100,req:st2)==12;
  }
}

Language: