summaryrefslogtreecommitdiff
path: root/Binaries
Commit message (Collapse)AuthorAge
* Boogie: Added boolean code expressions (sans well-formedness checks on the ↵Gravatar rustanleino2010-08-10
| | | | input).
* Reverting accidental check-inGravatar stobies2010-08-06
|
* Remove support for Z3 V1 and clean up parameter processing code for Z3Gravatar stobies2010-08-06
| | | | svn-ignoring some build artifacts
* <Boogie> This dll is not one that needs to be in the depot. It should be ↵Gravatar tabarbe2010-07-15
| | | | added in manually.
* Missing file needed for new C# projects.Gravatar mikebarnett2010-07-14
|
* Dafny: Axiom about inverting a set union operation, similar to the recent ↵Gravatar rustanleino2010-07-09
| | | | ones added for sequence concatenation. The new SeparationLogicList example profits from this axiom.
* Boogie:Gravatar rustanleino2010-06-22
| | | | | | | | | * Set Z3's QI_COST as the sum of "weight" and "generation", not their product. This worked better when setting the :weight of a quantifier (see below). Dafny: * Improved axiomatization of sequences; in particular, use an axiom to generate terms that say what the two pieces of a concatenation are * Two of the (previous) sequence axioms could cause a matching loop, in cases where Z3's arithmetic reasoning does not infer all rational arithmetic equalities during instantiation. The effect of this was apparently not noticed before, perhaps the concatenation/drop properties previously had to be supplied in manual assert statements. But now, with the improved sequence axiomatization (see previous bullet), this effect became remarkably noticeable. To reduce the bad effect of this apparent matching loop, Michal and I added a :weight annotation on two of the axioms, which, along with the Boogie change above, seems to give acceptable results. * Removed several assert lemmas that are no longer needed in Test programs (the test programs now contain only about a handful of such lemmas)
* Dafny:Gravatar rustanleino2010-06-18
| | | | | | * Added some more set axioms that go "inside out" for union and set differences (UnionOne already had such an axiom) * Fixed bug to, once again, allow multiple .dfy files on the command line (with the effect of them being merged into one program) * Fixed bug in translation of reads/modifies clauses that mention sequences
* Dafny:Gravatar rustanleino2010-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
* Script that gathers the files for the binary distribution Boogie.zip.Gravatar rustanleino2010-05-17
|
* Dafny:Gravatar rustanleino2010-05-13
| | | | | * Effectively make all in- and out-parameters of ghost methods ghosts. * Added DafnyRuntime.cs back in, which is needed to run Dafny programs, but which, unfortunately, is currently not being used in the test suite (something we should address)
* Changed the 'svn:ignore' property of /Binaries such that ALL currently not ↵Gravatar mschwerhoff2010-05-12
| | | | svn-added files are ignored. Currently added are only the files that are not generated during the build process (e.g. Makefile, FSharp.Core.dll), hence all files generated during the build process won't be committed.
* Dafny:Gravatar rustanleino2010-05-06
| | | | | * Recoded frame axioms to be more goal directed * Added Main test driver to Test/VSI-Benchmarks/b2.dfy
* Dafny:Gravatar rustanleino2010-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:Gravatar rustanleino2010-03-31
| | | | | | | * Added match statements (in addition to the previous match expressions) * Added missing axiom about boxes and datatypes * Improved axioms for datatype rank comparisons * Added test cases with mutual-recursion termination challenges
* Dafny: Ensures that function axioms are not being used while their ↵Gravatar rustanleino2010-03-19
| | | | consistency is being checked.
* Added a comment to the MakefileGravatar mschwerhoff2010-03-12
|
* Update to F# 1.9.9.9.Gravatar MichalMoskal2010-02-18
|
* Dafny: Added if-then-else expressions (replacing and extending the previous ↵Gravatar rustanleino2010-02-04
| | | | | | | | boolean-only if-then-else expressions) Dafny: Added 'class' functions and methods (i.e., functions and methods with a receiver parameter) Dafny grammar changes: Tthe 'use' keyword now goes before 'function' (akin to 'ghost' and 'class'), and quantifier triggers now go before the '::' Dafny: Check for division-by-zero for both '/' and '%'
* Dafny: updated to reflect Boogie's new parsing of function argumentsGravatar rustanleino2010-01-07
|
* Added resolution and translation of algebraic datatypes and (in function ↵Gravatar rustanleino2009-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.
* Start (some parsing and resolution) of adding algebraic datatypes to Dafny.Gravatar rustanleino2009-11-08
| | | | Included VSI-Benchmarks in standard tests.
* Added a sequence update expression in Dafny.Gravatar rustanleino2009-11-06
|
* Redesigned the encoding of Dafny generics, including the built-in types set ↵Gravatar rustanleino2009-11-06
| | | | | | | | | | | | and seq. Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43). Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed. Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy. Added a space in the pretty printing of Boogie coercion expressions.
* Applied patch 4316, which fixes an unsoundness in the axiomatization of ↵Gravatar rustanleino2009-11-05
| | | | sequences (for both Dafny and Chalice). This in turn fixes issue 5876.
* Update F# binaries to Oct09 CTPGravatar MichalMoskal2009-10-30
|
* Restoring Spec# binariesGravatar stobies2009-09-30
|
* Fixed some bugs in the generation of bitvector input for Z3.Gravatar rustanleino2009-09-29
| | | | Deleted/ignored some binaries in the Binaries directory.
* Dafny: Added axioms for division and modulo.Gravatar rustanleino2009-09-15
| | | | | Dafny: Make use of function preconditions in function well-definedness checks. Chalice: Changed old "install" to current "reorder" keyword in Emacs mode.
* Dafny:Gravatar rustanleino2009-09-14
| | | | | | | | * Added DeclType(f)==C axioms, which for each field f says which class declares it. Boogie: * Changed behavior of free loop invariants. Now, a free loop invariant is ignored on the checking side, just like for free requires and free ensures. The new switch /alwaysAssumeFreeLoopInvariants flag gives the previous behavior. * NOTE: I did NOT yet make the corresponding change for loop unrolling, but it is needed.
* Full (?) support in Dafny for Counterexample Visualizer predicates.Gravatar rustanleino2009-08-19
|
* Incorporated Counterexample Visualizer (CEV) information in the generated ↵Gravatar rustanleino2009-08-15
| | | | Boogie.
* Changes needed in order to build Boogie using a freshly built Spec# compiler ↵Gravatar mikebarnett2009-08-10
| | | | and not just the LKG.
* Initial set of files.Gravatar mikebarnett2009-07-15