diff options
author | kyessenov <unknown> | 2010-08-10 23:26:41 +0000 |
---|---|---|
committer | kyessenov <unknown> | 2010-08-10 23:26:41 +0000 |
commit | 7c0ae7d3fcf53750937bdc56ba2192dfcbcfb5f9 (patch) | |
tree | 5399c6eadb6706595aa4fa6039915c0e45ae17b3 | |
parent | c0ea623c69419edbc94a6739a7d4f903bde74778 (diff) |
Chalice: finite differences with recursion instead of loops
-rw-r--r-- | Chalice/examples/refinement/FiniteDiff.chalice | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/Chalice/examples/refinement/FiniteDiff.chalice b/Chalice/examples/refinement/FiniteDiff.chalice new file mode 100644 index 00000000..725d5961 --- /dev/null +++ b/Chalice/examples/refinement/FiniteDiff.chalice @@ -0,0 +1,45 @@ +class Cube0 { + method compute(n:int) returns (v: int) + requires n >= 0; + ensures v == n*n*n; + { + assume v == n*n*n; + } +} + +class Cube1 { + method compute(n:int) returns (v: int, w:int) // introducing recursion-local state? + requires n >= 0; + ensures v == n*n*n; + ensures w == (n+1)*(n+1)*(n+1)-n*n*n; // strengthen post-condition + { + if (n == 0) { + v := 0; + w := 1; + } else { + call v,w := compute(n-1); // rely on stronger post-condition + v := v + w; + assume w == 3*n*n + 3*n + 1; // simplify and guess next step + } + } +} + +class Cube2 { + method compute(n:int) returns (v: int, w:int, x:int) // more state + 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); + { + 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; + } + } +} |