Chalice/tests/refinements/LoopSqRoot.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

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

class A1 refines A0 {
  transforms sqroot(n) returns (x)
  {
    replaces x by {
      var l := 0;
      var r := n + 1;
      while (l + 1 != r) 
        invariant l >= 0 && r > l;
        invariant l*l <= n && n < r*r;
      {
        var k [l < k && k < r];
        if (k*k <= n) {
          l := k;
        } else {
          r := k;
        }
      }
      x := l;      
    }
  }
}

class A2 refines A1 {
  transforms sqroot(n) returns (x)
  {
    _
    while {
      replaces k by {
        var k [2*k <= l+r && l+r < 2*(k+1)]        
      }
      *
    }
    _
  }
}