summaryrefslogtreecommitdiff
path: root/Binaries
Commit message (Collapse)AuthorAge
* Dafny: Fixed axioms for Seq#Contains vs. the sequence building functionsGravatar Rustan Leino2011-06-29
|
* Dafny: fixed soundness problem with HeapSucc axiomGravatar Rustan Leino2011-06-01
|
* Dafny: added set comprehension expressionsGravatar Rustan Leino2011-05-18
|
* Dafny: To help verifications involving sequences of (boxed) booleans along, ↵Gravatar Rustan Leino2011-05-16
| | | | added function $IsCanonicalBoolBox
* Dafny: fixed compilation bugs, added @-signs in front of identifiers to ↵Gravatar Rustan Leino2011-05-11
| | | | avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation
* Don't set logic to UFNIA when /useArrayTheoryGravatar Michal Moskal2011-05-09
|
* Dafny: added "choose" operator on setsGravatar rustanleino2011-03-26
|
* Dafny: compile quantifiersGravatar rustanleino2011-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 smt2Gravatar rustanleino2011-03-10
| | | | Ignore duplicated else functions in models
* Add tickleBoolGravatar MichalMoskal2011-02-18
|
* Dafny:Gravatar rustanleino2011-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:.Gravatar MichalMoskal2011-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 optionsGravatar MichalMoskal2011-02-17
|
* Workaround bug in Z3 SMT parserGravatar MichalMoskal2011-02-15
|
* Background predicate for SMT2Gravatar MichalMoskal2011-02-15
|
* Dafny: replaced the user-defined $ite function with Boogie's built-in ↵Gravatar rustanleino2011-02-03
| | | | if-then-else expression
* Dafny: removed CEV instrumentationGravatar rustanleino2011-02-03
|
* Boogie: Updated 'PrepareBoogieZip.ba?t'.Gravatar wuestholz2011-01-10
|
* Remove FSharp DLLs (no longer needed) and obsolete MakefileGravatar MichalMoskal2010-12-06
|
* Remove the checked in Microsoft.ContractsGravatar MichalMoskal2010-12-06
|
* Boogie: Updated 'PrepareBoogieZip.bat'.Gravatar wuestholz2010-12-06
|
* Factored out the ParserHelper class into a separate project and updated the ↵Gravatar wuestholz2010-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 ↵Gravatar rustanleino2010-11-01
| | | | captureState mark-ups in the Boogie code generated from Dafny
* Miscellaneous changes:Gravatar rustanleino2010-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 arraysGravatar rustanleino2010-09-21
|
* Dafny:Gravatar rustanleino2010-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:Gravatar rustanleino2010-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 explicitGravatar sboehme2010-08-27
|
* 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 20:08:17 +0000