summaryrefslogtreecommitdiff
path: root/Util
Commit message (Collapse)AuthorAge
* DafnyExtension: fixed build problemsGravatar Rustan Leino2011-11-15
|
* Dafny: allow single-quote as a character in identifiers in the VS2010 modeGravatar Rustan Leino2011-11-09
|
* Dafny: added "multiset" keyword to syntax highlighting in emacs, vim, latex, VSXGravatar Rustan Leino2011-11-09
|
* Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" ↵Gravatar Rustan Leino2011-10-26
| | | | statement)
* Dafny: changed triggers (which are never really used, anyhow) from having a ↵Gravatar Rustan Leino2011-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 modeGravatar Rustan Leino2011-10-19
|
* Jennisys: change of keywords, now: interface/datamodel/codeGravatar Rustan Leino2011-09-28
| | | | Jennisys: allow assignment statements in interfaces (for now, these are syntactic sugar for ensures clauses)
* MergeGravatar Rustan Leino2011-08-04
|\
* | Dafny: for VS mode, let lexer allow "?"Gravatar Rustan Leino2011-08-04
| |
| * Chalie: Fix Visual Studio integration and add note about JVM stack size ↵Gravatar stefanheule2011-08-04
|/ | | | problems.
* Chalice VS integration: recognize string literalsGravatar Rustan Leino2011-08-03
|
* Chalice: added string type and string literals (but no other string operations)Gravatar Rustan Leino2011-07-26
|
* Added new multiset keyword to VS2010 syntax highlighter.Gravatar Jason Koenig2011-07-11
|
* Dafny: removed deprecated "call" and "use" keywords from syntax highlightersGravatar Rustan Leino2011-06-20
|
* Dafny: added constructorsGravatar Rustan Leino2011-05-28
|
* Better VisualStudio plugin feedback.Gravatar Jason Koenig2011-05-27
|
* VisualStudio plugin now informs the user of a timeout.Gravatar Jason Koenig2011-05-26
|
* Dafny: Alternative (and candidate replacement) syntax for declaring datatypesGravatar Rustan Leino2011-04-20
| | | | Dafny: Additional induction test cases
* Dafny: added type "nat"Gravatar Rustan Leino2011-04-19
|
* Jennisys: Parse and printGravatar Rustan Leino2011-04-07
|
* Dafny: added "choose" operator on setsGravatar rustanleino2011-03-26
|
* 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: implemented a more precise scheme for allowing use of a function's ↵Gravatar rustanleino2011-02-03
| | | | rep axiom
* 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
* VSIP integration into VS: Changed idle delay to 300ms (from 1s). ↵Gravatar rustanleino2010-11-17
| | | | Distinguish warnings/errors in Chalice.
* 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
* Added AssemblyInfo.cs, missing from previous DafnyExtension check-inGravatar rustanleino2010-10-22
|
* New Dafny mode for Visual Studio 2010, using the VS2010 extensions.Gravatar rustanleino2010-10-22
|
* Miscellaneous changes:Gravatar rustanleino2010-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:Gravatar rustanleino2010-10-09
| | | | | * extended the cheap type inference to also consider "in" expressions and quantifiers * added some refinement keywords to the Emacs mode for Chalice
* Util: Minor changes to the LaTeX listings packages for Boogie and Dafny.Gravatar wuestholz2010-09-30
|
* 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
|
* VS 2010: add "spec" as keyword in ChaliceGravatar kyessenov2010-09-02
|
* VS2010 mode for Dafny and Boogie: updated, for example to properly deal ↵Gravatar rustanleino2010-09-01
| | | | with string literals
* Boogie: Adding an autobuild and regression cmd file for Boogie and Dafny - ↵Gravatar tabarbe2010-08-27
| | | | Cleans and builds both projects, then executes the regressions if the build succeeded. If the build had failed, it will stop the script.
* VS 2010 mode for Chalice: some errors didn't show up in the window because ↵Gravatar kyessenov2010-08-20
| | | | positions were negative
* Simplified grammar for Chalice VS 2010 integration. It should now work and ↵Gravatar kyessenov2010-08-19
| | | | be easily extensible.
* Dafny: Fixed VS 2010 mode to really include all Dafny keywordsGravatar rustanleino2010-08-06
|
* Boogie: Added a new code snippet for IEnumerable out parametersGravatar tabarbe2010-08-02
|
* Code Snippets: Corrected an annoyance in one of the snippetsGravatar tabarbe2010-08-02
|
* Chalice:Gravatar kyessenov2010-07-30
| | | | | | | * add sequence axiom updates from Dafny * fix a bug in pretty printer for functions and predicates * add a command line option for not checking termination; refactor options code to update syntax help string * relax resolver to allow ghost state in assume statements (we don't know how to compile them in general anyways; assume false is still a special case and is compiled into assert false)
* Boogie/Dafny: For those who may have not used custom code snippets before, ↵Gravatar tabarbe2010-07-30
| | | | some instructions on getting VS to track them down, along with an Excel sheet detailing the ones available.
* Boogie/Dafny: Boogie and Dafny's conversion to C# and Code Contracts does ↵Gravatar tabarbe2010-07-30
| | | | not need to mean that adding functionality will take longer than it had before, now that the handy Spec# non-null typesystem and verification keywords no longer are used. Here are some handy Code Snippets which can be implemented in Visual Studio in order to make adding to the Boogie codebase rapid.
* VS2010 integration: fixed typo in Boogie mode (install for .bpl files, not ↵Gravatar rustanleino2010-07-19
| | | | | | .dfy file; duh!) Chalice tests: removed machine-specific path from test.bat (replacing the file reference with just 'scala', which in some ways is machine-specific too)
* Chalice: Introduced '[[ S ]]' as a shorthand syntax for 'lock (this) { S ↵Gravatar rustanleino2010-07-19
| | | | | | | }'. Think of the new brackets as atomicity brackets (see PetersonsAlgorithm.chalice) Chalice: Added Peterson's algorithm to test suite (safety properties only) VS 2010 integration: Updated Chalice and Dafny modes, added keyword highlighting for a new Boogie mode
* Visual Studio 2010 integration for Dafny and Chalice. See the "How to ↵Gravatar rustanleino2010-07-15
| | | | install binaries" link from the boogie.codeplex.com home page.
* Syntax file for Chalice.Gravatar kyessenov2010-07-14
|
* Chalice: No longer use Mask for "held" field; instead, only use the value ↵Gravatar rustanleino2010-07-14
| | | | of the "held" field in the heap
* Another part of the testing with that file.Gravatar tabarbe2010-07-08
|