Verifast Concurrency Verification Library for Java

A few examples are also available, readwrite counters, concurrent queues, and a toy webserver.

Download.

Example

import java.util.concurrent.*;
import java.util.concurrent.locks.*;
import java.util.concurrent.locks.ReentrantReadWriteLock.*;
/*@

predicate_ctor CCounter_shared_state (RWCounter c) () =
   c.N |-> ?v &*& v >= 0 &*& c.MAX |-> ?m &*& m > 0 &*& v <= m;


predicate_ctor CCounter_nonzero (RWCounter c) () =
   c.N |-> ?v &*& c.MAX |-> ?m &*& v > 0 &*& m > 0 &*& v <= m; 

predicate_ctor CCounter_nonmax (RWCounter c) () =
   c.N |-> ?v &*& c.MAX |-> ?m &*& v < m &*& m > 0 &*& v >= 0; 
   
predicate inv(RWCounter c) =  
         c.rl |-> ?rl &*& rl!=null &*& rlck(rl,1,CCounter_shared_state(c))
     &*& c.wl |-> ?wl &*& wl!=null &*& wlck(wl,1,CCounter_shared_state(c))
     &*& c.notzero |-> ?cc &*& cc !=null &*& cond(cc,CCounter_shared_state(c),CCounter_nonzero(c))
     &*& c.notmax |-> ?cm &*& cm !=null &*& cond(cm,CCounter_shared_state(c),CCounter_nonmax(c));
 
@*/

public class RWCounter {

  int N;
  int MAX;
  ReentrantReadWriteLock mon;
  ReadLock rl;
  WriteLock wl;
  Condition notzero; 
  Condition notmax; 

public RWCounter(int max)
//@ requires max > 0;
//@ ensures inv(this);
{
 MAX = max;
//@ close CCounter_shared_state(this)();
//@ close enter_rwlck(CCounter_shared_state(this));
mon = new ReentrantReadWriteLock();
rl = mon.readLock();
wl = mon.writeLock();
 //@ close set_cond(CCounter_shared_state(this),CCounter_nonzero(this));  
notzero = wl.newCondition();
 //@ close set_cond(CCounter_shared_state(this),CCounter_nonmax(this));  
notmax = wl.newCondition();
//@ close inv(this);
}

public void inc() 
//@ requires inv(this);
//@ ensures inv(this);
  {
   try {
  //@ open inv(this);
   wl.lock();
   //@ open CCounter_shared_state(this)();
   while (N == MAX)
   /*@ invariant N |-> ?v &*& v >= 0 &*& MAX |-> ?m &*& m > 0 &*& v <= m &*& 
                 notmax |-> ?cm &*& cm !=null &*&
                 cond(cm,CCounter_shared_state(this),CCounter_nonmax(this));
     @*/
   {
     //@ close CCounter_shared_state(this)();
     notmax.await();
     //@ open CCounter_nonmax(this)(); 
   }
   N++;
   //@ close CCounter_nonzero(this)(); 
   notzero.signal();
  } catch (java.lang.InterruptedException e){} 
   wl.unlock();
  //@ close inv(this);
}

public int get() 
//@ requires [?f]inv(this);
//@ ensures [f]inv(this);
  {
  //@ open [f]inv(this);
   rl.lock();
  //@ open [?q]CCounter_shared_state(this)();
   int v = N;
   //@ close [q]CCounter_shared_state(this)();
   rl.unlock();
  //@ close [f]inv(this);
  return v;
}

public void dec()
//@ requires [?f]inv(this);
//@ ensures [f]inv(this);
{
  try {
  //@ open inv(this);
    wl.lock();
  //@ open CCounter_shared_state(this)();
  while(N==0)
   /*@ invariant N |-> ?v &*& v >= 0 &*& MAX |-> ?m &*& m > 0 &*& v <= m &*& 
                 [f]notzero |-> ?cc &*& cc !=null &*&
                 [f]cond(cc,CCounter_shared_state(this),CCounter_nonzero(this));
   @*/
    {
      //@ close CCounter_shared_state(this)();
      notzero.await();
      //@ open CCounter_nonzero(this)();
      //@ assert N>=0;
    }
    N--;
  } catch (java.lang.InterruptedException e){} 
//@ close CCounter_shared_state(this)();
    wl.unlock();
//@ close [f]inv(this);
  } 
}