Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | DafnyExtension: hide execution-trace output, show split-expr related error ↵ | 2012-08-10 | |
| | | | | locations, set a 10-second timeout | ||
* | DafnyExtension: improvements | 2012-08-08 | |
| | |||
* | DafnyExtension: fixed build issues; added support for some refinement features | 2012-08-08 | |
| | |||
* | Dafny: the DafnyExtension mode for Visual Studio now calls the verifier and ↵ | 2012-08-08 | |
| | | | | visually indicates a non-verified buffer | ||
* | Dafny VS Extension: edited to make it build with new AST types, fixed some ↵ | 2012-08-02 | |
| | | | | bugs, added a temporary progress indicator | ||
* | Dafny: removed allocated keyword, changed module import syntax. "opened" ↵ | 2012-07-30 | |
| | | | | keyword is parsed but ignored. | ||
* | Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to ↵ | 2012-07-10 | |
| | | | | parallel syntax, other minor fixes | ||
* | Dafny: added copredicates | 2012-07-03 | |
| | |||
* | Dafny: Merge | 2012-06-27 | |
|\ | |||
* | | Dafny: Implemented abstract modules | 2012-06-26 | |
| | | |||
| * | Dafny: equality-support test cases. This is just a snapshot--some things ↵ | 2012-06-22 | |
|/ | | | | still to be fixed up. | ||
* | Dafny: removed support for the old keyword "unlimited" (all functions are ↵ | 2012-06-11 | |
| | | | | limited) | ||
* | Dafny: added finite maps | 2012-05-25 | |
| | |||
* | Dafny: fixed resolution bug for inductive datatypes (previous check did not ↵ | 2012-04-25 | |
| | | | | | | | handle generic datatypes correctly) Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code) Dafny: added "codatatype" declaration (syntax only for now) | ||
* | Dafny VSX: fixed compilation inconsistency | 2012-01-10 | |
| | |||
* | Dafny: added predicates | 2012-01-10 | |
| | |||
* | Dafny: Start of new refinement features -- clean out old ones | 2012-01-04 | |
| | |||
* | Merge | 2011-11-22 | |
|\ | |||
| * | DafnyExtension: fix up compilation (once again) | 2011-11-22 | |
| | | |||
* | | 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. | ||
* | DafnyExtension: fixed build problems | 2011-11-15 | |
| | |||
* | Dafny: allow single-quote as a character in identifiers in the VS2010 mode | 2011-11-09 | |
| | |||
* | Dafny: added "multiset" keyword to syntax highlighting in emacs, vim, latex, VSX | 2011-11-09 | |
| | |||
* | Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" ↵ | 2011-10-26 | |
| | | | | statement) | ||
* | Dafny: changed triggers (which are never really used, anyhow) from having a ↵ | 2011-10-21 | |
| | | | | | | | special syntactic form to being just an attribute Dafny: added "parallel" statement (so far, only parsing and resolving) Dafny: allow types on bound variables in "match" expressions/statements (there's never any incentive to list them explicitly in the program text, but it nevertheless seemed silly to forbid them) | ||
* | Jennisys: added "ensures" to emacs mode | 2011-10-19 | |
| | |||
* | Jennisys: change of keywords, now: interface/datamodel/code | 2011-09-28 | |
| | | | | Jennisys: allow assignment statements in interfaces (for now, these are syntactic sugar for ensures clauses) | ||
* | Merge | 2011-08-04 | |
|\ | |||
* | | Dafny: for VS mode, let lexer allow "?" | 2011-08-04 | |
| | | |||
| * | Chalie: Fix Visual Studio integration and add note about JVM stack size ↵ | 2011-08-04 | |
|/ | | | | problems. | ||
* | Chalice VS integration: recognize string literals | 2011-08-03 | |
| | |||
* | Chalice: added string type and string literals (but no other string operations) | 2011-07-26 | |
| | |||
* | Added new multiset keyword to VS2010 syntax highlighter. | 2011-07-11 | |
| | |||
* | Dafny: removed deprecated "call" and "use" keywords from syntax highlighters | 2011-06-20 | |
| | |||
* | Dafny: added constructors | 2011-05-28 | |
| | |||
* | Better VisualStudio plugin feedback. | 2011-05-27 | |
| | |||
* | VisualStudio plugin now informs the user of a timeout. | 2011-05-26 | |
| | |||
* | Dafny: Alternative (and candidate replacement) syntax for declaring datatypes | 2011-04-20 | |
| | | | | Dafny: Additional induction test cases | ||
* | Dafny: added type "nat" | 2011-04-19 | |
| | |||
* | Jennisys: Parse and print | 2011-04-07 | |
| | |||
* | Dafny: added "choose" operator on sets | 2011-03-26 | |
| | |||
* | Dafny: | 2011-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: implemented a more precise scheme for allowing use of a function's ↵ | 2011-02-03 | |
| | | | | rep axiom | ||
* | Dafny: Improved default decreases clauses for methods and functions | 2010-11-25 | |
| | | | | | Dafny: Don't display "alloc" field in BVD Chalice: Fixed error-message parsing error in VS mode | ||
* | VSIP integration into VS: Changed idle delay to 300ms (from 1s). ↵ | 2010-11-17 | |
| | | | | Distinguish warnings/errors in Chalice. | ||
* | Dafny: Record source positions of start/end curly braces for declaration ↵ | 2010-10-27 | |
| | | | | | | constructs. Dafny VS2010 extension: link with Dafny and use it to parse and type check | ||
* | Added AssemblyInfo.cs, missing from previous DafnyExtension check-in | 2010-10-22 | |
| | |||
* | New Dafny mode for Visual Studio 2010, using the VS2010 extensions. | 2010-10-22 | |
| | |||
* | Miscellaneous changes: | 2010-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 | ||
* | Chalice: | 2010-10-09 | |
| | | | | | * extended the cheap type inference to also consider "in" expressions and quantifiers * added some refinement keywords to the Emacs mode for Chalice |