diff options
| -rw-r--r-- | Chalice/examples/refinement/FiniteDiff.chalice | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/Chalice/examples/refinement/FiniteDiff.chalice b/Chalice/examples/refinement/FiniteDiff.chalice index 725d5961..ba9dfeb3 100644 --- a/Chalice/examples/refinement/FiniteDiff.chalice +++ b/Chalice/examples/refinement/FiniteDiff.chalice @@ -1,3 +1,7 @@ +// 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:int) returns (v: int) requires n >= 0; @@ -17,8 +21,8 @@ class Cube1 { v := 0; w := 1; } else { - call v,w := compute(n-1); // rely on stronger post-condition - v := v + w; + call v1,w1 := compute(n-1); // rely on stronger post-condition + v := v1 + w1; assume w == 3*n*n + 3*n + 1; // simplify and guess next step } } @@ -29,17 +33,17 @@ class Cube2 { requires n >= 0; ensures v == n*n*n; ensures w == (n+1)*(n+1)*(n+1)-n*n*n; - ensures x == (n+1)*(n+1); + ensures x == (n+1)*(n+1); // stop it here; \delta w is messy { if (n == 0) { v := 0; w := 1; x := 1; } else { - call v,w,x := compute(n-1); - v := v + w; - w := 3*x + 3*n + 1; - x := x + 2*n + 1; + call v1,w1,x1 := compute(n-1); + v := v1 + w1; + w := 3*x1 + 3*n + 1; + x := x1 + 2*n + 1; } } } |