diff options
| author |  leino <unknown> | 2015-05-10 08:28:54 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-05-10 08:28:54 -0700 |
| commit | 2e88568000690f3b5e79069e0fdcba5fef8f5ca9 (patch) | |
| tree | a63330579dc56f1117acc3ca2d3f34c2d7b28704 /Test/dafny4/NipkowKlein-chapter7.dfy.expect | |
| parent | 9e999ccbf8581acf181ff00a529de96e12c690d5 (diff) | |
Added to the test suite a Dafny encoding of Chapter 7 from the Nipkow and Klein book on semantics.
It includes many uses of inductive predicates and inductive lemmas.
Diffstat (limited to 'Test/dafny4/NipkowKlein-chapter7.dfy.expect')
| -rw-r--r-- | Test/dafny4/NipkowKlein-chapter7.dfy.expect | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/dafny4/NipkowKlein-chapter7.dfy.expect b/Test/dafny4/NipkowKlein-chapter7.dfy.expect new file mode 100644 index 00000000..e08b3632 --- /dev/null +++ b/Test/dafny4/NipkowKlein-chapter7.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 54 verified, 0 errors
|