Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Dafny: fixed lack of assign-such-that restriction in parallel statement | 2012-03-15 | |
| | |||
* | Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr; | 2012-03-15 | |
| | |||
* | Merge | 2012-03-02 | |
|\ | |||
* | | Dafny: tests for skeletons | 2012-03-02 | |
| | | |||
* | | Dafny: allow more skeleton statements in refinements | 2012-03-02 | |
| | | |||
| * | Dafny: fixed well-formedness checking of LET expressions to allow the RHS to ↵ | 2012-02-29 | |
|/ | | | | be used | ||
* | Dafny: make sure assume->assert transformation gives rise to a check | 2012-02-19 | |
| | |||
* | Dafny: added syntactic support for ...'s in statements, and started ↵ | 2012-02-18 | |
| | | | | implementation of refinement transformations thereof | ||
* | Dafny: allow signatures to be omitted on refining functions/methods | 2012-02-16 | |
| | |||
* | Dafny: allow various forms of leaving off type arguments in declarations | 2012-02-16 | |
| | |||
* | Dafny: Fixed a bug in the printing of let expressions. | 2012-01-24 | |
| | |||
* | Dafny: improved error location for violations of function postconditions | 2012-01-18 | |
| | |||
* | Dafny: allow a refinement to provide a function/method body if the ↵ | 2012-01-18 | |
| | | | | function/method being refined didn't have one | ||
* | Dafny: added signature checking to refinement | 2012-01-17 | |
| | |||
* | Dafny: allow parallel statements with an empty list of bound variables | 2012-01-17 | |
| | |||
* | Dafny: parallel statements: | 2012-01-17 | |
| | | | | | | | - removed the awkward restriction that method postconditions cannot use old/fresh if there's no modifies clause and no out-parameters; instead, implemented parallel statements to handle these cases - also allow old/fresh in ensures clauses of parallel statements - allow TypeRhs and choose expressions in Call/Proof parallel statements - disallow calls to non-ghost methods in parallel statements (since those may do "print" statements and we don't want to allow those to take place in parallel; besides, the compiler wants to omit the parallel statement altogether and could not do so if there were print statements) | ||
* | Dafny: Recheck specifications that contain refined (extended) predicates, ↵ | 2012-01-16 | |
| | | | | even if they are contained inside a split expression. Superposition is thought to be sound. | ||
* | Dafny: handle refinement of nested tokens that come from SpliExpr (still ↵ | 2012-01-12 | |
| | | | | need to deal with unsplit expressions, like quantifiers) | ||
* | Dafny: make full predicate definitions available only inside a module ↵ | 2012-01-11 | |
| | | | | (outside is just an implication: the predicate implies the body known so far) | ||
* | Dafny: allow class-member declarations at top level of any module (not just ↵ | 2012-01-10 | |
| | | | | the default module); these go into the (new) default class of each module | ||
* | Dafny: added test case for refinement and predicates (and fixed a parsing bug) | 2012-01-10 | |
| | |||
* | Dafny: added predicates | 2012-01-10 | |
| | |||
* | Dafny: added support for simple superposition refinements | 2012-01-09 | |
| | |||
* | Dafny: firmed up the module system | 2012-01-05 | |
| | |||
* | Dafny: disengaged old refinement test files | 2012-01-04 | |
| | |||
* | Dafny: don't allow ghost expressions in print statements | 2012-01-03 | |
| | |||
* | Dafny: Fixed a bug in the pretty printer. | 2011-12-26 | |
| | |||
* | Dafny: Extended the support for attributes on method/constructor calls. | 2011-12-23 | |
| | |||
* | Dafny: Added support for attributes on method/constructor calls. | 2011-12-21 | |
| | |||
* | Dafny: for a datatype with just one constructor, don't check (but do assume) ↵ | 2011-12-19 | |
| | | | | that destructors are applied only to those values constructed by that one-and-only constructor | ||
* | Dafny: Made sure that error locations refer to the Dafny program, even if ↵ | 2011-12-15 | |
| | | | | the /print option is used. | ||
* | Dafny: Added support for attributes on various specification constructs ↵ | 2011-12-07 | |
| | | | | (assert, ensures, modifies, decreases, invariant). | ||
* | Dafny: fix bug in translation of (the splitting of) if-then-else expressions ↵ | 2011-12-10 | |
| | | | | (see bug report Issue 10214 on codeplex) | ||
* | Merge | 2011-12-07 | |
|\ | |||
* \ | Merge | 2011-12-07 | |
|\ \ | |||
| * | | Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable ↵ | 2011-12-07 | |
| | | | | | | | | | | | | wellformedness checks). | ||
* | | | Boogie: Added new abstract interpretation harness, which uses native Boogie ↵ | 2011-12-05 | |
|/ / | | | | | | | | | | | | | | | Expr's, not the more abstract AIExpr's. Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false. Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals Boogie: Mark all inferred conditions with attribute {:inferred} | ||
| * | Dafny: Added "type" declaration (syntax: "type X;"), which introduces an ↵ | 2011-11-21 | |
|/ | | | | arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated. | ||
* | Dafny: added let expressions (syntax: "var x := E0; E1") | 2011-11-14 | |
| | | | | | Dafny: firmed up semantics of assert/assume expressions (the condition is now good for all program control paths that pass through the expression) Dafny: various implementation clean-ups | ||
* | Dafny: implemented the wellformedness check that datatype destructors are ↵ | 2011-11-11 | |
| | | | | | | only applied to values created by the corresponding constructor Dafny: implement ghost destructors properly | ||
* | Dafny: allow assert/assume expressions in more places | 2011-11-09 | |
| | |||
* | Dafny: added assert/assume expressions | 2011-11-09 | |
| | |||
* | Dafny: fixed part of a type-inference issue with datatypes and the < ↵ | 2011-11-09 | |
| | | | | | | operator on datatypes Dafny: allow the well-formedness check of a function's specification to know that the function, on the current arguments, returns a value of the declared result type | ||
* | Dafny: fixed bug in reads checking of array-to-sequence conversions | 2011-11-08 | |
| | |||
* | Dafny induction: | 2011-10-29 | |
| | | | | | | | * implemented induction tactic for result-less, non-mutating ghost methods * refine heuristics for determining if a variables is usefully passed to a recursive function * disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy) * added command-line flags /induction and /inductionHeuristic (everything is on by default) | ||
* | Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" ↵ | 2011-10-26 | |
| | | | | statement) | ||
* | 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 | ||
* | Dafny: check subrange restriction in parallel Assign statement | 2011-10-24 | |
| | | | | | Dafny: verify parallel Call statement Dafny: fixed some bugs: handle all cases of comprehension expressions in resolver's UsesSpecFeatures, check target of method calls to be non-null (duh!) | ||
* | Dafny: continued translation of "parallel" statements (Assign and Proof ↵ | 2011-10-24 | |
| | | | | | | | forms are mostly there, Call is missing and so is compilation) Dafny: included some test cases for the "parallel" statement Dafny: starting changing old "foreach" statements to the new "parallel" statement |