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

class SumCubes0 {
  method compute(n)
    requires n >= 0;
  {
    var i := 0;
    var s := 0;
    while (i < n)
      invariant i <= n;
    {
      i := i + 1;
      s := s + i*i*i;
    }
  }
}

class SumCubes1 refines SumCubes0 {
  transforms compute(n)  
  {    
    _
    var t := 0;    
    while    
      invariant s == t*t;
      invariant 2*t == i*(i+1);
    {    
      _         
      t := t + i;
    }
  }
}