summaryrefslogtreecommitdiff
path: root/Source/Dafny
Commit message (Collapse)AuthorAge
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵Gravatar mikebarnett2011-03-10
| | | | | | dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
* Dafny:Gravatar rustanleino2011-03-06
| | | | | | * Support for induction over more than 1 variable * Added many of the Rippling induction benchmarks * Fixed bug in case handling
* Dafny: Added heuristic for when to turn on the induction tacticGravatar rustanleino2011-03-05
|
* Dafny:Gravatar rustanleino2011-03-04
| | | | | | * Add support for an {:induction} attribute on universal quantifiers over one bound variable. It causes the universally quantified formulas to be proved by induction. * For a user-defined function F, introduce not just F and F#limited, but also F#2 (which sits "above" F, just as F sits "above" F#limited) * In base case of SplitExpr, make use of F#2 functions (unless already inside an inlined predicate)
* Dafny: support for nested match expressionsGravatar rustanleino2011-03-01
|
* Dafny: Non-empty Visual-Studio error messages for related split-expr locations.Gravatar rustanleino2011-02-27
| | | | Dafny: Forbid jumps from ghost code.
* Dafny: Improved scheme for splitting expressions. Also, report each split ↵Gravatar rustanleino2011-02-19
| | | | in error messages.
* 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(*)
* Dafny: every decreases clause implicitly ends with a never-ending sequence ↵Gravatar rustanleino2011-02-03
| | | | of TOP elements; this reduces the need for manually supplied decreases clauses (see the Outer/Inner example in Test/dafny0/Termination.dfy and the Substitute/SubstSeq example in Test/dafny1/Substitution.dfy).
* Dafny: allow self-calls in function postconditions--these simply refer to ↵Gravatar rustanleino2011-02-03
| | | | the result value of the current call
* Dafny: implemented a more precise scheme for allowing use of a function's ↵Gravatar rustanleino2011-02-03
| | | | rep axiom
* 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
|
* Dafny: removed unused Position argument from CheckWellformedGravatar rustanleino2011-02-03
|
* Dafny: white-space deltas in source codeGravatar rustanleino2011-02-02
|
* Dafny: added ensures clauses to functionsGravatar rustanleino2011-02-02
|
* Dafny: Fixed some build issues with duplicated and malformed Code Contracts.Gravatar rustanleino2011-01-13
|
* Dafny: Fixed error in printing an error message. Changed "function method" ↵Gravatar rustanleino2011-01-11
| | | | to "function" in a test case.
* 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#.
* Get rid of F# dependencies - use System.Numerics and a custom Rational ↵Gravatar MichalMoskal2010-12-02
| | | | structure instead
* Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵Gravatar qadeer2010-11-27
| | | | Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
* Dafny: Improved default decreases clauses for methods and functionsGravatar rustanleino2010-11-25
| | | | | Dafny: Don't display "alloc" field in BVD Chalice: Fixed error-message parsing error in VS mode
* 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
* Dafny: Record source positions of start/end curly braces for declaration ↵Gravatar rustanleino2010-10-27
| | | | | | constructs. Dafny VS2010 extension: link with Dafny and use it to parse and type check
* Updated parser.cs files to pick up the new .frame improvements from ↵Gravatar rustanleino2010-10-26
| | | | boogiepartners
* Boogie:Gravatar rustanleino2010-10-26
| | | | | | | | | * Updated Parser.cs/Scanner.cs to use new .frame files from boogiepartners. * It changes, for example, "syntax error:" to just "error:", so adjusted expected Test outputs. Dafny: * Ditto for its Parser.cs/Scanner.cs. * Added ability to provide a custom Errors handler for scanner/parser. * Added Test/dafny1/Cubes.dfy
* Update to VS2010.Gravatar MichalMoskal2010-10-07
|
* 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 a command-line option to change the prelude fileGravatar sboehme2010-08-30
|
* Dafny: fallback to ShallowType (elements of IndexField arrays seem to have ↵Gravatar sboehme2010-08-27
| | | | Type null)
* Dafny: added inlined functions making reads and updates of the heap explicitGravatar sboehme2010-08-27
|
* More line ending fixups.Gravatar MichalMoskal2010-08-06
|
* Dafny: Made line endings consistentGravatar tabarbe2010-08-04
|
* Dafny: Removed trailing spaces in codeGravatar tabarbe2010-08-04
|
* Fixed some infelicities in the project files.Gravatar mikebarnett2010-08-04
|
* Dafny: This file is required by DafnyPipeline.Gravatar tabarbe2010-08-03
|
* Dafny: Port commit part 1/2: Committing changed files.Gravatar tabarbe2010-08-03
| | | | Do not attempt to regenerate the Parser and Scanner files before the port of Boogie/Core is done, as these have undergone changes, but will not be committed until after the Core port.
* Dafny: Renaming the DafnyPipeline source files in preparation for the commit ↵Gravatar tabarbe2010-08-03
| | | | of my port of that project.
* Sign both of the Dafny projects and have Dafny.exe get a version number as well.Gravatar mikebarnett2010-07-30
|
* Tortoise SVN screwed up previous commit.Gravatar kyessenov2010-07-14
|
* Dafny: added comments for refinements assertions.Gravatar kyessenov2010-07-14
|
* Dafny: better error reporting on resolution of refinements. Replace ↵Gravatar kyessenov2010-07-14
| | | | assertions with "if"s to handle errors gently and add cycle detection check.
* Dafny: keep counters for loops, temporary variables across two ↵Gravatar kyessenov2010-07-07
| | | | implementations in the refinement VC
* Dafny:Gravatar rustanleino2010-07-06
| | | | | * changed rule about scoping of out-parameters * added "refines", "replaces", and "by" as keywords in emacs, vim, and latex style files
* Boogie: Added an additional parameter 'defines' to the method ↵Gravatar wuestholz2010-07-06
| | | | 'BoogiePL.Parser.Parse'.
* Dafny: added assertions in the refinement obligation necessitating that the ↵Gravatar kyessenov2010-07-03
| | | | return values of concrete and abstract executions are equal. Refactored a test to simulate "static" function call.
* Dafny: Support class type parameters in refinements. Added another ↵Gravatar kyessenov2010-07-02
| | | | regression test -- a sequence refined by a singly linked list.
* Dafny: support input/output parameters in refined methods.Gravatar kyessenov2010-07-02
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 03:48:53 +0000