| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
Codeplex repositories.
|
| |\ |
|
| | | |
|
| | |
| |
| |
| | |
of / and %
|
| | |
| |
| |
| | |
and refining), no compilation or verification
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
| |
keyword is parsed but ignored.
|
| |
|
|
| |
parallel syntax, other minor fixes
|
| | |
|
| |
|
|
| |
limited)
|
| |
|
|
|
|
|
| |
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)
|
| | |
|
| | |
|
| |
|
|
| |
arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated.
|
| | |
|
| |
|
|
| |
statement)
|
| |
|
|
|
|
|
| |
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: allow assignment statements in interfaces (for now, these are syntactic sugar for ensures clauses)
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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(*)
|
| |
|
|
|
|
|
| |
* 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
|
| |
|
|
|
| |
* extended the cheap type inference to also consider "in" expressions and quantifiers
* added some refinement keywords to the Emacs mode for Chalice
|
| |
|
|
|
|
| |
* 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
|
| |
|
|
| |
of the "held" field in the heap
|
| |
|
|
|
| |
* changed rule about scoping of out-parameters
* added "refines", "replaces", and "by" as keywords in emacs, vim, and latex style files
|
| |
|
|
|
| |
* renamed keyword "maxlock" to "waitlevel"
* added -vs switch, for I/O suitable for VS integration
|
| |
|
|
|
|
|
| |
* 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
|
| |
|
|
|
|
|
|
|
|
| |
* Added support for polymorphism in lambda expressions
* Little clean-up here and there
* Added 'then' keyword to emacs and latex modes
Dafny:
* Added support for fine-grained framing, using the back-tick syntax from Region Logic
* Internally, changed checking of reads clauses to use a local variable $_Frame, analogous to the $_Frame variable used in checking modifies clauses
|
| |
|
|
|
| |
Previously, a "use" function was one whose definition was applied only in limited ways, namely when the function was uttered in a program (possibly in a "use" statement). Now, recursive functions are always limited, unless declared with the new modifier "unlimited". Non-recursive functions are always unlimited. Also new is that only function calls within the same SCC of the call graph use the limited form of the callee.
The "use" modifier is no longer supported. The "use" statement is still supported, now for both limited and unlimited functions; but it's probably better and easier to just explicitly mention a function in an assertion, if needed.
|
| |
|
|
|
|
|
|
| |
* 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
|
| |
|
|
|
| |
* Beginning of module implementation
* Changed "class" modifier (for functions and methods) to "static"
|
| | |
|
| | |
|
| |
|
|
| |
supports syntax-highlighting, auto-indentation and imenu.
|
| |
|
|
|
|
|
|
| |
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 '%'
|
| |
|
|
|
|
|
| |
* Allow (and currently ignore) "ghost" modifier.
* Fixed bug in boxing.
* Check for div-by-zero error for modulo operator.
* Improved emacs and latex modes.
|
| |
|
|
| |
Included VSI-Benchmarks in standard tests.
|
| |
|
|
|
| |
Dafny: Make use of function preconditions in function well-definedness checks.
Chalice: Changed old "install" to current "reorder" keyword in Emacs mode.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- channel declarations
- send and receive statements
- bounds clause for new, to accommodate channels
- Added ProdConsChannel.chalice test case
- Resolve and Translate (but no Compile yet)
- Added Credits to global state in encoding (this caused changes to lots of source lines)
* Simplified meaning of maxlock==E
* Various parser improvements
* Added alternative syntax for eval statements
* Some renamings in error messages (e.g., install -> reorder)
* Added preliminary parsing for condition variables and their wait and signal operations
* Added new keywords to Chalice emacs mode
|
| |
|
Rustan Leino
Rustan Leino
Unknown
Nadia Polikarpova