class Cell {
  var x: int;
  
  // dispose a read permission to x
  method dispose_rd()
    requires rd(x);
    ensures true;
  {
  }
  
  // return read permission
  method void()
    requires rd(x);
    ensures rd(x);
  {
  }
  
  // multiple calls to method that destroys rd(x)
  method a1()
    requires rd(x);
    ensures true;
  {
    call dispose_rd();
    call dispose_rd();
  }
  
  // call to method that destroys rd(x) really removes permission
  method a2()
    requires rd(x);
    ensures rd(x);
  {
    call dispose_rd();
    // ERROR: should fail to verify postcondition
  }
  
  // forking and method calls of dispose_rd
  method a3()
    requires rd(x);
    ensures true;
  {
    fork dispose_rd();
    call dispose_rd();
    fork dispose_rd();
    call dispose_rd();
  }
  
  // forking and method calls of dispose_rd
  method a4()
    requires rd(x);
    ensures rd(x);
  {
    fork dispose_rd();
    // ERROR: should fail to verify postcondition
  }
  
  // forking and method calls of dispose_rd
  method a5()
    requires rd(x);
    ensures rd(x,1);
  {
    fork dispose_rd();
    // OK: giving away an epsilon permission however should work
  }
  
  // forking and method calls of dispose_rd
  method a6()
    requires rd(x);
    ensures rd*(x);
  {
    fork dispose_rd();
    // OK: giving away a 'undefined' read permission however should work
  }
  
  // multiple forks of dispose_rd
  method a7()
    requires rd(x);
    ensures true;
  {
    fork dispose_rd();
    fork dispose_rd();
    fork dispose_rd();
    fork dispose_rd();
    fork dispose_rd();
    fork dispose_rd();
  }
  
  // joining to regain permission
  method a8(a: int)
    requires rd(x);
    ensures rd(x)
  {
    fork tk := void();
    join tk;
  }
  
  // joining to regain permission
  method a9(a: int)
    requires rd(x);
    ensures rd(x)
  {
    fork tk := dispose_rd();
    join tk;
    // ERROR: should fail to verify postcondition
  }
  
  // joining to regain permission
  method a10(a: int)
    requires rd(x);
    ensures a == 3 ==> rd(x)
  {
    fork tk := void();
    if (3 == a) {
      join tk;
    }
  }
  
  // finite loop of method calls, preserving rd(x)
  method a11()
    requires rd(x);
    ensures rd(x);
  {
    var i: int;
    i := 0;
    while (i < 1000)
      invariant rd(x);
    {
      call void();
      i := i+1;
    }
  }
  
  // forking dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
  method a12(a: int)
    requires rd(x);
    ensures rd*(x);
  {
    var i: int;
    i := 0;
    while (i < a)
      invariant rd*(x);
    {
      fork dispose_rd();
      i := i+1;
    }
  }
  
  // forking dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
  method a13(a: int)
    requires rd(x);
    ensures rd(x);
  {
    var i: int;
    i := 0;
    while (i < a)
      invariant rd*(x);
    {
      fork dispose_rd();
      i := i+1;
    }
    // ERROR: should fail to verify postcondition
  }
  
  // calling dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
  method a14()
    requires rd(x);
    ensures true;
  {
    call dispose_rd();
    
    var i: int;
    i := 0;
    while (i < 1000)
      invariant rd*(x);
    {
      call dispose_rd();
      i := i+1;
    }
  }
  
  // return unknown permission
  method a15()
    requires rd(x);
    ensures rd*(x);
  {
    call dispose_rd();
  }
  
  // rd in loop invariant
  method a16()
    requires rd(x);
    ensures rd*(x);
  {
    call dispose_rd();
    
    var i: int;
    i := 0;
    while (i < 1000)
      invariant acc(x,rd);
    {
      call void();
      i := i+1;
    }
  }
  
  // rd in method contracts
  method a17()
    requires acc(x,rd);
  {
    call dispose_rd();
    call a17();
  }
  
  // multiple rd in method contracts
  method a18()
    requires rd(x);
    ensures rd(x)
  {
    call a18a()
    call a18b()
  }
  method a18a()
    requires acc(x,2*rd);
    ensures acc(x,rd+rd);
  {
  }
  method a18b()
    requires acc(x,rd+rd);
    ensures acc(x,rd*2);
  {
  }
  
}