Chalice/refinements/TestRefines.chalice


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

class A {
  var x:int;
  function f():int {1}
  method m(i:int) returns (j:int) {
    var j [j > 0];    
  }
}

class B refines C {}
class C refines D {}
class D refines A {
  transforms m(i:int) returns (j:int, k:int) 
  {
  *
  } 
}

class X {
  method m() returns (c: bool) 
  {
    c := true;
  }
}

class Y refines X {
  refines m() returns (c: bool, d: bool)
  {
    c := false;
  }
}