summaryrefslogtreecommitdiff
path: root/Binaries
Commit message (Collapse)AuthorAge
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 06:40:40 +0000