summaryrefslogtreecommitdiff
path: root/Test/VSI-Benchmarks/Answer
Commit message (Collapse)AuthorAge
* Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵Gravatar Rustan Leino2013-03-05
| | | | Codeplex repositories.
* Dafny: re-ran parser generator to include semicolon-less body-less ↵Gravatar Rustan Leino2011-07-26
| | | | functions/methods, and updated some test files accordingly (compare with changesets 1429 and 1366)
* Fixed regression test failures due to removal of bodiless methods and functions.Gravatar Jason Koenig2011-07-15
|
* 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
| | | | | * Recoded frame axioms to be more goal directed * Added Main test driver to Test/VSI-Benchmarks/b2.dfy
* 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
* Added wellformedness checks to method specificationsGravatar rustanleino2010-03-12
|
* * Added decreases clauses to functionsGravatar rustanleino2009-11-24
| | | | | | | | | | | | | | | | | | | | * If no decreases clause is given, the decreases clause defaults to the set of objects denoted by the reads clause, which was the previous Dafny behavior * Made Dafny check loops for termination by default. Previously, this was done only if the loop had a decreases clause. To indicate that a loop is to be checked only for partial correctness, Dafny now allows "decreases *". * Allow "reads *" to say that the function may read anything at all (sound, but not very useful) * Adjusted frame axioms of functions to speak of allocated objects more liberally; and also added antecedents about the heaps being well-formed and the parameters being allocated * Added some previously omitted well-definedness checks. * Fixed some bugs in the resolver that caused some type errors not to be reported * Added some messages to go with some (previously rather opaquely reported) errors * Fixed some test cases that previously had ordered conjuncts incorrectly to prove termination and reads checks (such checks were previously omitted) * Beefed up Test/dafny0/SchorrWaite.dfy to use datatypes to specify that no garbage gets marked. The full-functional total-correctness verification of this Schorr-Waite method now takes about 3.2 seconds.
* 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-11-27 09:52:07 +0000