| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Added option to force Dafny compilation, even if verification fails. |  Jason Koenig | 2011-06-30 |
| | | |||
| * | Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵ | mikebarnett | 2011-03-10 |
| | | | | | | | dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked. | ||
| * | Dafny: Non-empty Visual-Studio error messages for related split-expr locations. | rustanleino | 2011-02-27 |
| | | | | | Dafny: Forbid jumps from ghost code. | ||
| * | Dafny: Improved scheme for splitting expressions. Also, report each split ↵ | rustanleino | 2011-02-19 |
| | | | | | in error messages. | ||
| * | Dafny: removed CEV instrumentation | rustanleino | 2011-02-03 |
| | | |||
| * | Dafny: white-space deltas in source code | rustanleino | 2011-02-02 |
| | | |||
| * | Dafny: Fixed some build issues with duplicated and malformed Code Contracts. | rustanleino | 2011-01-13 |
| | | |||
| * | Add functions generated in lambda-expansion of function body to top-level ↵ | MichalMoskal | 2010-12-17 |
| | | | | | program declarations. | ||
| * | Factored out the ParserHelper class into a separate project and updated the ↵ | wuestholz | 2010-12-02 |
| | | | | | | | files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#. | ||
| * | Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln | qadeer | 2010-12-01 |
| | | |||
| * | forgot to check this file in | qadeer | 2010-11-28 |
| | | |||
| * | Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵ | qadeer | 2010-11-27 |
| | | | | | Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0. | ||
| * | Dafny: a partial first crack at a Dafny model-viewer provider, including ↵ | rustanleino | 2010-11-01 |
| | | | | | captureState mark-ups in the Boogie code generated from Dafny | ||
| * | Update to VS2010. | MichalMoskal | 2010-10-07 |
| | | |||
| * | Dafny: | rustanleino | 2010-09-14 |
| | | | | | | | | | * Added internal support for multi-dimensional arrays (but not all surface syntax is there yet) * Removed unused variables from Dafny.atg Boogie and Dafny: * Improved error message for postcondition violations | ||
| * | Dafny: Made line endings consistent | tabarbe | 2010-08-04 |
| | | |||
| * | Dafny: Removed trailing spaces in code | tabarbe | 2010-08-04 |
| | | |||
| * | Fixed some infelicities in the project files. | mikebarnett | 2010-08-04 |
| | | |||
| * | fixed path to the binaries directory; there was an extra .." | qadeer | 2010-08-03 |
| | | |||
| * | Also build Boogie and Dafny projects in 32-bit configurations. | rustanleino | 2010-07-30 |
| | | | | | Don't insist on DafnyDriver picking up the LKG version (1.0.21125.0) of the Spec# runtime (in fact, most builders will probably have 1.0.21126.0). | ||
| * | Sign both of the Dafny projects and have Dafny.exe get a version number as well. | mikebarnett | 2010-07-30 |
| | | |||
| * | Dafny: DafnyDriver port part 3/3: Updating sources to reference new project. | tabarbe | 2010-07-28 |
| | | |||
| * | Dafny: DafnyDriver port part 2/3: Adding new dependent file, removing ↵ | tabarbe | 2010-07-28 |
| | | | | | unnecessary one. | ||
| * | Dafny: DafnyDriver port part 1/3: Replacing old source files with ported version | tabarbe | 2010-07-28 |
| | | |||
| * | Dafny/DafnyDriver: Renaming source files in preparation for port commit | tabarbe | 2010-07-28 |
| | | |||
| * | Boogie: Added an additional parameter 'defines' to the method ↵ | wuestholz | 2010-07-06 |
| | | | | | 'BoogiePL.Parser.Parse'. | ||
| * | Updated the frame files to work with the latest Coco/R. This entails *not* ↵ | mikebarnett | 2010-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. | ||
| * | Dafny: | rustanleino | 2010-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: | rustanleino | 2010-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 | ||
| * | Dafny: | rustanleino | 2010-03-12 |
| | | | | | | * Modifies clause checking is now done with each update, instead of at the end of the method. Not only does this improve error messages, but on some examples, it gives a dramatic speed-up (2x) in proving time. * bugfix: range expressions of foreach statements were previously ignored during Translation | ||
| * | Dafny: Added stratosphere tests for datatypes--that is, it is now checked ↵ | rustanleino | 2010-03-11 |
| | | | | | that every datatype has some value. | ||
| * | Added resolution and translation of algebraic datatypes and (in function ↵ | rustanleino | 2009-11-20 |
| | | | | | | | bodies) match expressions. Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies. | ||
| * | * Boogie and Dafny: added /cev:<file> option | rustanleino | 2009-09-15 |
| | | | | | | * SscBoogie: changed default setting for /modifiesOnLoop (we really should move this SscBoogie-specific code to the Spec# codeplex) | ||
| * | Sign assemblies | stobies | 2009-08-17 |
| | | |||
| * | Initial set of files. | mikebarnett | 2009-07-15 |
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |