diff options
| author |  Unknown <leino@leino5.redmond.corp.microsoft.com> | 2011-04-04 18:45:15 -0700 |
|---|---|---|
| committer | Unknown <leino@leino5.redmond.corp.microsoft.com> | 2011-04-04 18:45:15 -0700 |
| commit | bff446fb46898a2ef6222e957baef8ea5f788513 (patch) | |
| tree | 86d7ea7281d3d6baf3c37dd346f621dbd391202d /Test/dafny1/pow2.dfy | |
| parent | 6e93acd001f5d23c08b02c162dc2111e531f3d5d (diff) | |
Dafny: fixed bug in induction over integers
Dafny: added pow2 example
Diffstat (limited to 'Test/dafny1/pow2.dfy')
| -rw-r--r-- | Test/dafny1/pow2.dfy | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy new file mode 100644 index 00000000..52cddaac --- /dev/null +++ b/Test/dafny1/pow2.dfy @@ -0,0 +1,54 @@ +// This is a Dafny adaptation of a Coq program by David Pichardie.
+
+function IsEven(n: int): bool
+ requires 0 <= n;
+ ensures IsEven(n) ==> n == (n/2)+(n/2);
+{
+ (n/2)*2 == n
+}
+
+function Square(n: int): int { n * n }
+
+function pow2(n: int): int
+ requires 0 <= n;
+ ensures 0 <= pow2(n);
+{
+ if n == 0 then
+ 1
+ else if IsEven(n) then
+ Square(pow2(n / 2))
+ else
+ 2*pow2(n-1)
+
+}
+
+function pow2_slow(n: int): int
+ requires 0 <= n;
+{
+ if n == 0 then
+ 1
+ else
+ 2*pow2_slow(n-1)
+}
+
+ghost method Lemma(n: int)
+ requires 0 <= n && IsEven(n);
+ ensures pow2_slow(n) == Square(pow2_slow(n/2));
+{
+ if (n != 0) {
+ call Lemma(n-2);
+ }
+}
+
+ghost method Theorem(n: int)
+ requires 0 <= n;
+ ensures pow2(n) == pow2_slow(n);
+{
+ if (n == 0) {
+ } else if (IsEven(n)) {
+ call Lemma(n);
+ call Theorem(n/2);
+ } else {
+ call Theorem(n-1);
+ }
+}
|