Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ↵ | Jason Koenig | 2012-07-17 |
| | | | | parallel statements. | ||
* | Dafny: Implemented abstract modules | Jason Koenig | 2012-06-26 |
| | |||
* | Dafny: fixed a couple of compiler bugs | Unknown | 2012-06-14 |
| | |||
* | Dafny: beefed up allocation axioms for boxes stored in fields | Unknown | 2012-06-12 |
| | |||
* | Dafny: Added map comprehensions and updated display syntax | Unknown | 2012-05-31 |
| | |||
* | Dafny: Added compilation of finite maps | Unknown | 2012-05-25 |
| | |||
* | Dafny: added finite maps | Unknown | 2012-05-25 |
| | |||
* | Dafny: fully qualify (with module names) names of types in the translation ↵ | Rustan Leino | 2012-01-05 |
| | | | | | | | into Boogie Dafny: started cloning of refined classes Dafny: added /rprint switch to print the (syntax of the) resolved Dafny program | ||
* | Dafny: added comment about how to mark the run-time expression-sequencing ↵ | Rustan Leino | 2012-01-04 |
| | | | | method as a good candidate for inlining (supported in .NET 4.5) | ||
* | Dafny: compile let expressions efficiently (i.e., with an extra variable, ↵ | Rustan Leino | 2012-01-04 |
| | | | | not with a substitution) | ||
* | Dafny: moved definition of class.array into prelude, anticipating writing ↵ | Rustan Leino | 2011-11-09 |
| | | | | axioms that use it | ||
* | Dafny: removed support for assigning to an array-range (that is, an ↵ | Rustan Leino | 2011-10-26 |
| | | | | assignment statement where the LHS has the form a[lo..hi]) | ||
* | Dafny: implemented compilation of parallel statements | Rustan Leino | 2011-10-25 |
| | | | | Dafny: beefed up resolution of parallel statements | ||
* | Updated 'PrepareBoogieZip.bat' to include Houdini. | wuestholz | 2011-08-23 |
| | |||
* | Fixed axiom for Take/Update commuting. | Jason Koenig | 2011-07-19 |
| | |||
* | Added compilation support for multisets and sequences from arrays. | Jason Koenig | 2011-07-15 |
| | |||
* | Strengthened axioms for multisets and sequences. | Jason Koenig | 2011-07-14 |
| | |||
* | Added multiset from sequence axioms, removed array range RHSs. Fixed issue ↵ | Jason Koenig | 2011-07-13 |
| | | | | with duplicate array.Length functions in generated Boogie file. | ||
* | Multiset forming operators added. | Jason Koenig | 2011-07-11 |
| | |||
* | Partial implementation of multisets. | Jason Koenig | 2011-07-11 |
| | |||
* | Dafny: Dafny now uses the Euclidean definition of division. (Verifier and ↵ | Jason Koenig | 2011-07-08 |
| | | | | runtime.) | ||
* | Dafny: Fixed axioms for Seq#Contains vs. the sequence building functions | Rustan Leino | 2011-06-29 |
| | |||
* | Dafny: fixed soundness problem with HeapSucc axiom | Rustan Leino | 2011-06-01 |
| | |||
* | Dafny: added set comprehension expressions | Rustan Leino | 2011-05-18 |
| | |||
* | Dafny: To help verifications involving sequences of (boxed) booleans along, ↵ | Rustan Leino | 2011-05-16 |
| | | | | added function $IsCanonicalBoolBox | ||
* | Dafny: fixed compilation bugs, added @-signs in front of identifiers to ↵ | Rustan Leino | 2011-05-11 |
| | | | | avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation | ||
* | Don't set logic to UFNIA when /useArrayTheory | Michal Moskal | 2011-05-09 |
| | |||
* | Dafny: added "choose" operator on sets | rustanleino | 2011-03-26 |
| | |||
* | Dafny: compile quantifiers | rustanleino | 2011-03-26 |
| | | | | | | Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction Dafny: split expressions when proving function postconditions Boogie and BVD: updated copyright year ranges | ||
* | Updated PrepareBoogieZip.bat to include BVD and smt2 | rustanleino | 2011-03-10 |
| | | | | Ignore duplicated else functions in models | ||
* | Add tickleBool | MichalMoskal | 2011-02-18 |
| | |||
* | Dafny: | rustanleino | 2011-02-17 |
| | | | | | | | | | | | | | | | | | | * Big change: Add type and allocatedness information everywhere in the Boogie translation. This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program. On the downside, it also requires discharging more antecedents in order to use some axioms. Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case). * Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms). (Internally, this uses the new canCall mechanism.) * Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type. * More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal") * Add axioms about idempotence of set union and intersection * The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one * In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase * Fixed error in translation of while(*) | ||
* | Provide /p: as the short form of /proverOpt:. | MichalMoskal | 2011-02-17 |
| | | | | | Add /p:O:<name>=<value> and /p:C:<solver-argument> prover options in SMT. Add default Z3 options when using Z3. | ||
* | Make it possible to run Z3 on pipe; use generic PROVER_LOG options | MichalMoskal | 2011-02-17 |
| | |||
* | Workaround bug in Z3 SMT parser | MichalMoskal | 2011-02-15 |
| | |||
* | Background predicate for SMT2 | MichalMoskal | 2011-02-15 |
| | |||
* | Dafny: replaced the user-defined $ite function with Boogie's built-in ↵ | rustanleino | 2011-02-03 |
| | | | | if-then-else expression | ||
* | Dafny: removed CEV instrumentation | rustanleino | 2011-02-03 |
| | |||
* | Boogie: Updated 'PrepareBoogieZip.ba?t'. | wuestholz | 2011-01-10 |
| | |||
* | Remove FSharp DLLs (no longer needed) and obsolete Makefile | MichalMoskal | 2010-12-06 |
| | |||
* | Remove the checked in Microsoft.Contracts | MichalMoskal | 2010-12-06 |
| | |||
* | Boogie: Updated 'PrepareBoogieZip.bat'. | wuestholz | 2010-12-06 |
| | |||
* | 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#. | ||
* | 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 | ||
* | Miscellaneous changes: | rustanleino | 2010-10-22 |
| | | | | | | | * Also copy CodeContractExtender in PrepareBoogieZip.bat * Added some comments and a new program in Test/textbook * Included refinement keywords in Chalice emacs mode * Used assignment instead of spec statement in DuplicatesVideo.chalice | ||
* | Dafny: Compilation of multi-dimensional arrays | rustanleino | 2010-09-21 |
| | |||
* | Dafny: | rustanleino | 2010-09-17 |
| | | | | | | * Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation) * Changed syntax of array length from |a| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays. * Internally, this meant adding support for built-in classes and readonly fields | ||
* | 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: added inlined functions making reads and updates of the heap explicit | sboehme | 2010-08-27 |
| | |||
* | Boogie: Added boolean code expressions (sans well-formedness checks on the ↵ | rustanleino | 2010-08-10 |
| | | | | input). |