summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks/b7.dfy
Commit message (Collapse)AuthorAge
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
|
* Enhanced the VSI-Benchmarks tests:Gravatar Rustan Leino2013-03-26
| | | | | - replaced the sequences used to specify permutations with multisets - used some of the newer syntax in Dafny
* Dafny: allow constructors only inside classes, removed semi-colons at end of ↵Gravatar Rustan Leino2011-07-11
| | | | body-less functions/methods
* Dafny: retired the "call" keywordGravatar Rustan Leino2011-05-26
|
* Dafny:Gravatar rustanleino2010-05-21
| | | | | | | * Added arrays * Beefed up set axiomatization to know more things about set displays * Added a simple heuristic that can infer some simple decreases clauses for loops * Added Dafny solutions to a couple of VACID benchmarks
* Dafny:Gravatar rustanleino2010-05-06
| | | | | | | | * First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies) * Added "print" statement (to make running compiled programs more interesting) * Changed name of default class from $default to _default Boogie: * Included "lambda" as a keyword in emacs and latex style files
* 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.
* Initial version of VSI Benchmarks 1 - 8Gravatar RMonahan2009-10-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 12:30:16 +0000