summaryrefslogtreecommitdiff
path: root/Test/dafny2
Commit message (Expand)AuthorAge
* Dafny: Since it's no longer true that all types support equality at run-time ...Gravatar Unknown2012-06-21
* Dafny: fixed a couple of compiler bugsGravatar Unknown2012-06-14
* Dafny: cleaned up test scripts a littleGravatar Unknown2012-06-14
* Dafny: added another version of the majority finding algorithm to the test suiteGravatar Unknown2012-06-12
* Dafny: beefed up allocation axioms for boxes stored in fieldsGravatar Unknown2012-06-12
* Dafny: added some test programsGravatar Rustan Leino2012-06-08
* Dafny: support assign-such-that in var declarations in refinementsGravatar Unknown2012-03-15
* Dafny: added StoreAndRetrieve refinement exampleGravatar Unknown2012-03-15
* Dafny: implemented thresholds for the new interval domain (/infer:j)Gravatar Rustan Leino2011-12-12
* Dafny tests: Disabled SnapshotableTrees.dfy for now while performance issues ...Gravatar Rustan Leino2011-12-07
* Dafny: call C# compiler directly from inside Dafny, and optionally produce a ...Gravatar Rustan Leino2011-11-22
* Added some Dafny and Boogie test cases, including Turing's factorial program,...Gravatar Rustan Leino2011-11-03
* Dafny: Commented out SnapshotableTrees.Node.FunctionalInsert while performanc...Gravatar Rustan Leino2011-10-26
* Dafny: fixed performance-buggy translation of exists, and also added some oth...Gravatar Rustan Leino2011-10-19
* Dafny: added COST Verification Competition challenge programs to test suiteGravatar Rustan Leino2011-10-07
* Dafny: Updated snapshotable tree to remove IsReadonly precondition for Create...Gravatar Rustan Leino2011-09-30
* Dafny: beautification in one test case, and fixed an Answer fileGravatar Rustan Leino2011-09-29
* Dafny: Added TreeBarrier as a test caseGravatar peter mueller peter.mueller@inf.ethz.ch2011-09-29
* Dafny: added Snapshotable Trees exampleGravatar Rustan Leino2011-09-11