Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Added initial support for float addition | 2015-09-17 | |
| | |||
* | Added the fp32 class, copied from the previously existing BigDec class. No ↵ | 2015-04-17 | |
| | | | | significant changes from BigDec have been made | ||
* | The back pred files have been eliminated. The small backpred string is now ↵ | 2013-12-08 | |
| | | | | directly included in ProverInterface.cs. | ||
* | Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵ | 2013-03-05 | |
| | | | | Codeplex repositories. | ||
* | Removed Dafny, Jennisys, Chalice, and BCT, which now live in different ↵ | 2013-03-05 | |
| | | | | Codeplex repositories. | ||
* | Updated PrepareBoogieZip.bat file for the binary release that just went out ↵ | 2012-10-22 | |
| | | | | on Codeplex | ||
* | deleted unnecessary files | 2012-10-04 | |
| | |||
* | Dafny: fixed merge | 2012-10-04 | |
| | |||
* | Merge | 2012-10-04 | |
|\ | |||
* | | Dafny: complete implementation of iterators | 2012-10-03 | |
| | | |||
* | | Dafny: more part of verifying iterators | 2012-10-03 | |
| | | |||
* | | Dafny: incomplete snapshot of verification of iterators | 2012-10-02 | |
| | | |||
| * | Updated the 'PrepareBoogieZip.bat' script. | 2012-10-01 | |
| | | |||
| * | Dafny: removed div/mod axioms, since Boogie now interprets div/mod | 2012-09-28 | |
| | | | | | | | | | | Dafny: included FloydCycleDetect again (which had been temporarily commented out) DafnyExtension: adjusted to Boogie's change in abstract-interpretation support | ||
| * | Boogie: added type 'real' with overloaded arithmetic operations plus real ↵ | 2012-09-27 | |
| | | | | | | | | | | | | | | | | | | division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested) | ||
| * | Boogie: new syntax for integer division and modulus: use div and mod instead ↵ | 2012-09-27 | |
|/ | | | | of / and % | ||
* | Dafny: things about sequences: parse Suffix expressions after DisplayExpr's, ↵ | 2012-09-12 | |
| | | | | and axiomatize [][..0] == [] == [][0..] | ||
* | Implement support for alternative SMT solvers -- CVC3 and CVC4 | 2012-09-06 | |
| | |||
* | Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ↵ | 2012-07-17 | |
| | | | | parallel statements. | ||
* | Dafny: Implemented abstract modules | 2012-06-26 | |
| | |||
* | Dafny: fixed a couple of compiler bugs | 2012-06-14 | |
| | |||
* | Dafny: beefed up allocation axioms for boxes stored in fields | 2012-06-12 | |
| | |||
* | Dafny: Added map comprehensions and updated display syntax | 2012-05-31 | |
| | |||
* | Dafny: Added compilation of finite maps | 2012-05-25 | |
| | |||
* | Dafny: added finite maps | 2012-05-25 | |
| | |||
* | Dafny: fully qualify (with module names) names of types in the translation ↵ | 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 ↵ | 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, ↵ | 2012-01-04 | |
| | | | | not with a substitution) | ||
* | Dafny: moved definition of class.array into prelude, anticipating writing ↵ | 2011-11-09 | |
| | | | | axioms that use it | ||
* | Dafny: removed support for assigning to an array-range (that is, an ↵ | 2011-10-26 | |
| | | | | assignment statement where the LHS has the form a[lo..hi]) | ||
* | Dafny: implemented compilation of parallel statements | 2011-10-25 | |
| | | | | Dafny: beefed up resolution of parallel statements | ||
* | Updated 'PrepareBoogieZip.bat' to include Houdini. | 2011-08-23 | |
| | |||
* | Fixed axiom for Take/Update commuting. | 2011-07-19 | |
| | |||
* | Added compilation support for multisets and sequences from arrays. | 2011-07-15 | |
| | |||
* | Strengthened axioms for multisets and sequences. | 2011-07-14 | |
| | |||
* | Added multiset from sequence axioms, removed array range RHSs. Fixed issue ↵ | 2011-07-13 | |
| | | | | with duplicate array.Length functions in generated Boogie file. | ||
* | Multiset forming operators added. | 2011-07-11 | |
| | |||
* | Partial implementation of multisets. | 2011-07-11 | |
| | |||
* | Dafny: Dafny now uses the Euclidean definition of division. (Verifier and ↵ | 2011-07-08 | |
| | | | | runtime.) | ||
* | Dafny: Fixed axioms for Seq#Contains vs. the sequence building functions | 2011-06-29 | |
| | |||
* | Dafny: fixed soundness problem with HeapSucc axiom | 2011-06-01 | |
| | |||
* | Dafny: added set comprehension expressions | 2011-05-18 | |
| | |||
* | Dafny: To help verifications involving sequences of (boxed) booleans along, ↵ | 2011-05-16 | |
| | | | | added function $IsCanonicalBoolBox | ||
* | Dafny: fixed compilation bugs, added @-signs in front of identifiers to ↵ | 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 | 2011-05-09 | |
| | |||
* | Dafny: added "choose" operator on sets | 2011-03-26 | |
| | |||
* | Dafny: compile quantifiers | 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 | 2011-03-10 | |
| | | | | Ignore duplicated else functions in models | ||
* | Add tickleBool | 2011-02-18 | |
| | |||
* | Dafny: | 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(*) |