summaryrefslogtreecommitdiff
path: root/Util
Commit message (Collapse)AuthorAge
* 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
|
* Another test using that Multilingual Greetings fileGravatar tabarbe2010-07-08
|
* 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
* (no commit message)Gravatar tabarbe2010-06-30
|
* (no commit message)Gravatar tabarbe2010-06-29
|
* (no commit message)Gravatar tabarbe2010-06-29
|
* (no commit message)Gravatar tabarbe2010-06-29
|
* (no commit message)Gravatar tabarbe2010-06-29
|
* (no commit message)Gravatar tabarbe2010-06-29
|
* (no commit message)Gravatar tabarbe2010-06-29
|
* (no commit message)Gravatar tabarbe2010-06-29
|
* (no commit message)Gravatar tabarbe2010-06-29
|
* (no commit message)Gravatar tabarbe2010-06-29
|
* (no commit message)Gravatar tabarbe2010-06-29
|
* (no commit message)Gravatar tabarbe2010-06-29
|
* Testing whether history of an old file remains after rename and commit.Gravatar tabarbe2010-06-29
|
* Chalice:Gravatar rustanleino2010-06-25
| | | | | * renamed keyword "maxlock" to "waitlevel" * added -vs switch, for I/O suitable for VS integration
* 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
|
* Dafny:Gravatar rustanleino2010-05-21
| | | | | | | * 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
* Boogie:Gravatar rustanleino2010-05-15
| | | | | | | | | | * 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
* Dafny:Gravatar rustanleino2010-05-08
| | | | | 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.
* Dafny:Gravatar rustanleino2010-05-06
| | | | | | | | * 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
* Dafny:Gravatar rustanleino2010-03-16
| | | | | * Beginning of module implementation * Changed "class" modifier (for functions and methods) to "static"
* Removed files that were under GPL.Gravatar mikebarnett2010-02-22
|
* Boogie (Util): Added an Emacs flymake extension for BoogiePL.Gravatar wuestholz2010-02-19
|
* Boogie (Emacs mode): Added an alternative Emacs mode for BoogiePL. It ↵Gravatar wuestholz2010-02-19
| | | | supports syntax-highlighting, auto-indentation and imenu.
* Dafny: Added if-then-else expressions (replacing and extending the previous ↵Gravatar rustanleino2010-02-04
| | | | | | | | 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 '%'
* Dafny:Gravatar rustanleino2010-01-14
| | | | | | | * Allow (and currently ignore) "ghost" modifier. * Fixed bug in boxing. * Check for div-by-zero error for modulo operator. * Improved emacs and latex modes.
* Start (some parsing and resolution) of adding algebraic datatypes to Dafny.Gravatar rustanleino2009-11-08
| | | | Included VSI-Benchmarks in standard tests.
* Introduced operator !in in Dafny. An expression "x !in S" is equivalent to ↵Gravatar rustanleino2009-11-05
| | | | | | | "!(x in S)". Changed Dafny test files to use the new operator. Included the file b8.dfy into the VSI-Benchmarks test harness.
* Dafny: Added axioms for division and modulo.Gravatar rustanleino2009-09-15
| | | | | Dafny: Make use of function preconditions in function well-definedness checks. Chalice: Changed old "install" to current "reorder" keyword in Emacs mode.
* * Implemented channelsGravatar rustanleino2009-08-16
| | | | | | | | | | | | | | | | - 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
* Initial set of files.Gravatar mikebarnett2009-07-15