summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks
Commit message (Collapse)AuthorAge
...
* Redesigned the encoding of Dafny generics, including the built-in types set ↵Gravatar rustanleino2009-11-06
| | | | | | | | | | | | and seq. Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43). Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed. Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy. Added a space in the pretty printing of Boogie coercion expressions.
* The Dafny call statement now automatically declares left-hand sides as local ↵Gravatar rustanleino2009-11-05
| | | | variables, if they were not already local variables.
* Introduced operator !in in Dafny. An expression "x !in S" is equivalent to ↵Gravatar rustanleino2009-11-05
| | | | | | | "!(x in S)". Changed Dafny test files to use the new operator. Included the file b8.dfy into the VSI-Benchmarks test harness.
* Added loop invariants to make VSI-Benchmarks/b8.dfy verify. (Still to do: ↵Gravatar rustanleino2009-11-04
| | | | uncomment a couple of the desired loop invariants.)
* Initial version of VSI Benchmarks 1 - 8Gravatar RMonahan2009-10-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 03:58:38 +0000