summaryrefslogtreecommitdiff
path: root/Dafny/Makefile
Commit message (Collapse)AuthorAge
* Dafny: added ensures clauses to functionsGravatar rustanleino2011-02-02
|
* Factored out the ParserHelper class into a separate project and updated the ↵Gravatar wuestholz2010-12-02
| | | | | | files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#.
* Unified the .frame files so that both Boogie and Dafny use exactly the same ↵Gravatar mikebarnett2010-06-25
| | | | ones.
* Dafny:Gravatar rustanleino2010-06-24
| | | | | * re-introduced the feature where an input filename of "stdin.dfy" says to read the program from standard input * supplied missing case (NotInSet) in Compiler.ssc
* Updated the frame files to work with the latest Coco/R. This entails *not* ↵Gravatar mikebarnett2010-06-22
| | | | | | having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories. Lots of code changes to compensate for the new frame files.
* Initial set of files.Gravatar mikebarnett2009-07-15