Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | minor changes | 2016-06-06 | |
| | |||
* | Merging complete. Everything looks good *crosses fingers* | 2016-06-06 | |
| | |||
* | 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 |