Simple model abstraction

Very simple verification example with model-based abstraction. A process algebraic model is created that is able to perform a single action: "step", which increments some shared variable by one. We verify that this is a valid abstraction of a program that increases some shared value by one.

General Information

Backend: Silicon
Language: PVL
Features: Futures
Path to Example File: futures/TestFuture.pvl
Should Verify: Yes
Date: 2017-06-16
Lines of Code: 57 (comments not included)
Lines of Specification: 20 (35.1% of total)
Computation Time: 24.8 seconds

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: case TestFuture
//:: tool silicon
//:: option --check-history

// begin(future)
class `Future` {
  int x;
  
  modifies x;
  ensures x==\old(x)+1;
  process step();
}
//end(future)

class Test {

int y;

requires Perm(f.x,1);
  requires t==f.x+1;
  ensures HPerm(f.x,1) ** Future(f,1,f.step()) ** AbstractState(f,x==t);
  static void start(`Future` f,int t){
    create f,f.step();
  }

requires HPerm(f.x,1) ** Future(f,1,f.step());
  ensures  HPerm(f.x,1) ** Future(f,1,empty);
  static void work(`Future` f){
    action(f,1,empty,f.step(),x,write){
      f.x=f.x+1;
    }
  }

requires HPerm(f.x,1) ** Future(f,1,empty) ** AbstractState(f,x==t);
  ensures Perm(f.x,1) ** f.x==t;
  static void stop(`Future` f,int t){
    destroy f;
  }

// begin(main)
  static void main(){
    `Future` f=new `Future`();
    f.x=1;
    create f,f.step();
    assert AbstractState(f,x==2);
    action(f,1,empty,f.step()){
      f.x=f.x+1;
    }
    destroy f;
    assert f.x==2;
    refute false;
  }
// end(main)

static void main2(){
    `Future` f=new `Future`();
    f.x=1;
    start(f,2);
    work(f);
    stop(f,2);
    assert f.x==2;
    refute false;
  }
  
}

Language: