// Example of a program computing cube using only addition. 
// Step-wise refinement using specification statement. 
// Chalice does not have termination metric for recursive methods.

class Cube0 {
  method compute(n) returns (v)
    requires n >= 0; 
    ensures v == n*n*n;
  {
    var v [v == n*n*n]
  }
}

class Cube1 refines Cube0 {
  transforms compute(n) returns (v, w) 
    // strengthen post-condition based on new output variables
    ensures w == (n+1)*(n+1)*(n+1)-n*n*n; 
  {
    replaces v by {
      if (n == 0) {
        v := 0;
        w := 1;
      } else {
        call v1,w1 := compute(n-1); // rely on stronger post-condition
        v := v1 + w1;
        // simplified form: aha! we need n*n to compute with addition
        var w [w == 3*n*n + 3*n + 1];
      }
    }
  }
}

class Cube2 refines Cube1 {
  transforms compute(n) returns (v, w, x) 
    ensures x == (n+1)*(n+1);   
  { 
    if {
      _
      x := 1;
    } else {
      replaces v1, w1 by {
        call v1,w1,x1 := compute(n-1);
      }
      _
      replaces w by {
        w := 3*x1 + 3*n + 1;
        x := x1 + 2*n + 1;
      }
    }
  }
}