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/maximum.dfy.expect | |
| 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/maximum.dfy.expect')
| -rw-r--r-- | Test/tutorial/maximum.dfy.expect | 7 |
1 files changed, 7 insertions, 0 deletions
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 |