summaryrefslogtreecommitdiff
path: root/Util/vim
Commit message (Collapse)AuthorAge
* 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: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
* Vim: add keywords to ChaliceGravatar kyessenov2010-09-02
|
* Syntax file for Chalice.Gravatar kyessenov2010-07-14
|
* 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
* slightly improved syntax fileGravatar kyessenov2010-06-24
|
* VIM syntax file for BPL. I just had it laying around.Gravatar MichalMoskal2010-06-21
|
* A simple highlighting syntax file for Vim.Gravatar kyessenov2010-06-21