summaryrefslogtreecommitdiff
path: root/Test/vstte2012
Commit message (Expand)AuthorAge
* Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requiresGravatar qunyanm2016-03-28
* Change the induction heuristic for lemmas to also look in precondition for cl...Gravatar leino2015-08-12
* Renamed "ghost method" to "lemma" whenever appropriate (which is most of the ...Gravatar Rustan Leino2015-07-28
* Stop pretty-print from emitting deprecated semi-colons.Gravatar qunyanm2015-03-05
* Language change: All functions and methods declared lexically outside any cla...Gravatar leino2014-12-12
* Change behavior of 'decreases *', which can be applied to loops and methods. ...Gravatar Rustan Leino2014-08-19
* MergeGravatar Rustan Leino2014-07-08
|\
* | Cleaned up a test programGravatar Rustan Leino2014-07-08
| * MergeGravatar Dan Rosén2014-07-07
| |\ | |/ |/|
| * New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
* | Removed the old test infrastructure.Gravatar wuestholz2014-07-01
* | Invert LHS sub-expressions in forall assignment statements, which gives the o...Gravatar Rustan Leino2014-06-24
|/
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Removed unused declarationGravatar Rustan Leino2014-01-03
* Changed BreadthFirstSearch example to no longer use "inductive naturals", seq...Gravatar Rustan Leino2014-01-03
* Add support for the /verifySeparately flag in Boogie and change most tests to...Gravatar wuestholz2013-12-18
* Added an assert to help the theorem prover out in the RingBuffer.Enqueue method.Gravatar Rustan Leino2013-07-29
* Changed ranking function for Seq, so that it's compatible with data types.Gravatar Unknown2013-06-26
* Beefed up axioms about cardinality and the empty (multi)set, which fixes Issu...Gravatar Rustan Leino2013-06-20
* Made Test/vstte2012/RingBuffer.dfy and Test/dafny1/ExtensibleArray.dfy more s...Gravatar Rustan Leino2013-04-22
* The "choose" statement, hacky and specialized as it was, is now gone. Use th...Gravatar Rustan Leino2013-03-27
* Adjustments in the /vcsMaxKeepGoingSplits flag in the test suiteGravatar Rustan Leino2013-03-09
* Renamed "parallel" statement to "forall" statement, and made the parentheses ...Gravatar Rustan Leino2013-03-06
* Reverted some accidental changes to a test caseGravatar Rustan Leino2013-02-11
* Renamed a variable in some test casesGravatar Rustan Leino2013-02-02
* Fixed some goof-ups in the test script editsGravatar Rustan Leino2012-10-04
* Added Test/dafny3 and another test file for iterators (hey, you can even run ...Gravatar Rustan Leino2012-10-04
* Dafny: reinstated autocontractsGravatar Jason Koenig2012-07-02
* Dafny: fixed up test suite (temporarily removed autocontract tests)Gravatar Jason Koenig2012-06-28
* Undo bad merge.Gravatar afd2012-06-27
* MergeGravatar Unknown2012-06-25
|\
| * Dafny: Since it's no longer true that all types support equality at run-time ...Gravatar Unknown2012-06-21
* | Merged with default.Gravatar chmaria2012-06-18
|\|
| * Dafny: cleaned up test scripts a littleGravatar Unknown2012-06-14
* | Dafny: Added tests.Gravatar chmaria2012-06-12
|/
* Dafny: removed a now-inferred type-parameter instantiation in a test fileGravatar Unknown2012-03-07
* Dafny: added ghost modules (the meaning is simply that such a module will not...Gravatar Rustan Leino2012-03-07
* Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic sp...Gravatar Unknown2012-03-05
* Dafny: call C# compiler directly from inside Dafny, and optionally produce a ...Gravatar Rustan Leino2011-11-22
* Added Dafny solutions to the VSTTE 2012 program verification competitionGravatar Rustan Leino2011-11-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 13:08:55 +0000