summaryrefslogtreecommitdiff
path: root/Test/vstte2012/BreadthFirstSearch.dfy
Commit message (Expand)AuthorAge
* Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requiresGravatar qunyanm2016-03-28
* Language change: All functions and methods declared lexically outside any cla...Gravatar leino2014-12-12
* 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
* The "choose" statement, hacky and specialized as it was, is now gone. Use th...Gravatar Rustan Leino2013-03-27
* Renamed "parallel" statement to "forall" statement, and made the parentheses ...Gravatar Rustan Leino2013-03-06
* Dafny: Since it's no longer true that all types support equality at run-time ...Gravatar Unknown2012-06-21
* Added Dafny solutions to the VSTTE 2012 program verification competitionGravatar Rustan Leino2011-11-15