Chalice/tests/refinements/RecSqRoot.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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

class A0 {
  method sqroot(n) returns (x)
    requires n >= 0;
  {
    var x [x*x <= n && n < (x+1)*(x+1)];      
  }  
}

class A1 refines A0 {
  transforms sqroot(n) returns (x)
  {        
    replaces x by {call x := rec(n,0,n+1)}    
  }
  
  method rec(n, l, r) returns (x)
    requires l*l <= n && n < r*r;
    requires l >= 0 && r >= 0;
    ensures x*x <= n && n < (x+1)*(x+1);
  {
    if (l+1 == r) {
      x := l;
    } else {
      var k [l < k && k < r];
      if (n < k*k) {
        call x := rec(n,l,k);
      } else {
        call x := rec(n,k,r);
      }
    }
  }
}

class A2 refines A1 {
  transforms rec(n, l, r) returns (x)
  {    
    if {
      *
    } else {
      replaces k by {
        assert l < r;
        var k := l+1;
      }
      *
    }    
  }
}