diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-22 13:44:42 -0700 |
---|---|---|
committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-22 13:44:42 -0700 |
commit | 5623306213e01e8d667a7893cb0c3275ecfbf065 (patch) | |
tree | 9eb9ef6ba9068ce3397e4f9d99797ed3a2934499 /Test/tutorial | |
parent | e33ab2dea7b3a367d2bb5c0d3926fa6fcc790ed4 (diff) |
Add a 'tutorial' folder to the distribution, with an initial example.
It would be nice to gather neat Dafny examples there; each new feature could
have its own small file that demoes it, and we could also have examples that
showcase stuff that we think is impressive.
I'm adding this as a test folder, because it's important to check that these
cool examples don't break, but the focus probably shouldn't be on exhaustively
testing the features being demoed.
Diffstat (limited to 'Test/tutorial')
-rw-r--r-- | Test/tutorial/maximum.dfy | 32 | ||||
-rw-r--r-- | Test/tutorial/maximum.dfy.expect | 7 |
2 files changed, 39 insertions, 0 deletions
diff --git a/Test/tutorial/maximum.dfy b/Test/tutorial/maximum.dfy new file mode 100644 index 00000000..81faa219 --- /dev/null +++ b/Test/tutorial/maximum.dfy @@ -0,0 +1,32 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This file shows how to specify and implement a function to compute the +// largest element of a list. The function is fully specified by two +// preconditions, as proved by the MaximumIsUnique lemma below. + +method Maximum(values: seq<int>) returns (max: int) + requires values != [] + ensures max in values + ensures forall i | 0 <= i < |values| :: values[i] <= max +{ + max := values[0]; + var idx := 0; + while (idx < |values|) + invariant max in values + invariant idx <= |values| + invariant forall j | 0 <= j < idx :: values[j] <= max + { + if (values[idx] > max) { + max := values[idx]; + } + idx := idx + 1; + } +} + +lemma MaximumIsUnique(values: seq<int>, m1: int, m2: int) + requires m1 in values && forall i | 0 <= i < |values| :: values[i] <= m1 + requires m2 in values && forall i | 0 <= i < |values| :: values[i] <= m2 + ensures m1 == m2 { + // This lemma does not need a body: Dafny is able to prove it correct entirely automatically. +} diff --git a/Test/tutorial/maximum.dfy.expect b/Test/tutorial/maximum.dfy.expect new file mode 100644 index 00000000..70768304 --- /dev/null +++ b/Test/tutorial/maximum.dfy.expect @@ -0,0 +1,7 @@ +maximum.dfy(11,10): Info: Selected triggers: {values[i]} +maximum.dfy(18,14): Info: Selected triggers: {values[j]} +maximum.dfy(28,27): Info: Selected triggers: {values[i]} +maximum.dfy(29,27): Info: Selected triggers: {values[i]} +maximum.dfy(15,2): Info: decreases int(|values|) - int(idx) + +Dafny program verifier finished with 4 verified, 0 errors |