diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-09-11 10:29:24 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-09-11 10:29:24 -0700 |
| commit | b25e8fa5503332ae469c9f7a50409d038fcc69cd (patch) | |
| tree | 25d316c72a2775b1496931b97e79f049dd0ddabd | |
| parent | 6f4e149d040697133d0886efafc74568ce0d9eee (diff) | |
Dafny: added Flatten example to test suite
| -rw-r--r-- | Test/dafny1/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny1/MoreInduction.dfy | 63 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 2 |
3 files changed, 68 insertions, 1 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 8457e1be..0a99ca95 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -87,6 +87,10 @@ Dafny program verifier finished with 29 verified, 0 errors Dafny program verifier finished with 137 verified, 0 errors
+-------------------- MoreInduction.dfy --------------------
+
+Dafny program verifier finished with 8 verified, 0 errors
+
-------------------- Celebrity.dfy --------------------
Dafny program verifier finished with 10 verified, 0 errors
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy new file mode 100644 index 00000000..efba0963 --- /dev/null +++ b/Test/dafny1/MoreInduction.dfy @@ -0,0 +1,63 @@ +datatype List<X> = Nil | Cons(Node<X>, List<X>);
+datatype Node<X> = Element(X) | Nary(List<X>);
+
+function FlattenMain<X>(list: List<X>): List<X>
+ ensures IsFlat(FlattenMain(list));
+{
+ Flatten(list, Nil)
+}
+
+function Flatten<X>(list: List<X>, ext: List<X>): List<X>
+ requires IsFlat(ext);
+ ensures IsFlat(Flatten(list, ext));
+{
+ match list
+ case Nil => ext
+ case Cons(n, rest) =>
+ match n
+ case Element(x) => Cons(n, Flatten(rest, ext))
+ case Nary(nn) => Flatten(nn, Flatten(rest, ext))
+}
+
+function IsFlat<X>(list: List<X>): bool
+{
+ match list
+ case Nil => true
+ case Cons(n, rest) =>
+ match n
+ case Element(x) => IsFlat(rest)
+ case Nary(nn) => false
+}
+
+function ToSeq<X>(list: List<X>): seq<X>
+{
+ match list
+ case Nil => []
+ case Cons(n, rest) =>
+ match n
+ case Element(x) => [x] + ToSeq(rest)
+ case Nary(nn) => ToSeq(nn) + ToSeq(rest)
+}
+
+ghost method Theorem<X>(list: List<X>)
+ ensures ToSeq(list) == ToSeq(FlattenMain(list));
+{
+ Lemma(list, Nil);
+}
+
+ghost method Lemma<X>(list: List<X>, ext: List<X>)
+ requires IsFlat(ext);
+ ensures ToSeq(list) + ToSeq(ext) == ToSeq(Flatten(list, ext));
+{
+ match (list) {
+ case Nil =>
+ case Cons(n, rest) =>
+ match (n) {
+ case Element(x) =>
+ Lemma(rest, ext);
+ case Nary(nn) =>
+ Lemma(nn, Flatten(rest, ext));
+ Lemma(rest, ext);
+ }
+ }
+}
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index 50bf20e0..15bd28a1 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -21,7 +21,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy SchorrWaite.dfy
Cubes.dfy SumOfCubes.dfy FindZero.dfy
TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy
- Induction.dfy Rippling.dfy
+ Induction.dfy Rippling.dfy MoreInduction.dfy
Celebrity.dfy
UltraFilter.dfy) do (
echo.
|