| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Chalice: added syntax, printer and resolver for coupling invariants |  kyessenov | 2010-08-20 |
| | | |||
| * | VS 2010 mode for Chalice: some errors didn't show up in the window because ↵ | kyessenov | 2010-08-20 |
| | | | | | positions were negative | ||
| * | Chalice: more regression tests; cosmetic changes to code | kyessenov | 2010-08-19 |
| | | |||
| * | Chalice: added finite differencing refinement | kyessenov | 2010-08-19 |
| | | |||
| * | Chalice: | kyessenov | 2010-08-19 |
| | | | | | | * support multi-step refinement (convert refinement blocks into normal sequences of statements) * added tests | ||
| * | Chalice: | kyessenov | 2010-08-19 |
| | | | | | | | * added loop transform pattern * implemented translation of refined loops to Boogie (only assert new loop invariants) * refactored loop target computation code (async call was not handled as maybe some other statement) | ||
| * | Chalice: turn asserts into assumes for method refinements (use -noFreeAssume ↵ | kyessenov | 2010-08-19 |
| | | | | | to disable) | ||
| * | Chalice: | kyessenov | 2010-08-18 |
| | | | | | | | * transforms are now callable * resolve transform specs * implement translation for refinement blocks (correct for manipulating locals, not globals) | ||
| * | Chalice: | kyessenov | 2010-08-18 |
| | | | | | | | | * print type checked program (use -print -noTypecheck if you want old behavior) * refactored program context in Resolver ('errors' is kept as a ListBuffer and shared) * added resolver for refinement blocks (no loops yet) * pretty printer should work now for transforms | ||
| * | Chalice: added surface syntax for transform, AST matching algorithm | kyessenov | 2010-08-17 |
| | | |||
| * | Chalice: refactored AST code for class hierarchy (no need for caches since ↵ | kyessenov | 2010-08-17 |
| | | | | | Scala uses structural equality for case classes); landed first piece of refinement code | ||
| * | Chalice: bug fixes -- "check termination" flag was not properly preserved ↵ | kyessenov | 2010-08-16 |
| | | | | | (i.e. if function app was inside old, the flag was ignored); != was not properly translated for sequences | ||
| * | Chalice: add pre-conditions to specification statements; semantically spec ↵ | kyessenov | 2010-08-13 |
| | | | | | statement is just like a call statement now | ||
| * | Chalice: add specification statement ( ghost? (const|var) (x (:T)?)+ [P(x)] ) | kyessenov | 2010-08-13 |
| | | |||
| * | Chalice: accept many input files at once; read from stdin if no input file ↵ | kyessenov | 2010-08-12 |
| | | | | | specified | ||
| * | Chalice: example proving a simple identity (for refinement demonstration), ↵ | kyessenov | 2010-08-12 |
| | | | | | revise code comments | ||
| * | Chalice: put classes and objects into package "chalice" | kyessenov | 2010-08-11 |
| | | |||
| * | Chalice: fix "assume false" in the example (intended a spec statement) | kyessenov | 2010-08-11 |
| | | |||
| * | Chalice: finite differences with recursion instead of loops | kyessenov | 2010-08-10 |
| | | |||
| * | Chalice: added uninterpreted functions; attempting to re-verify Celebrity in ↵ | kyessenov | 2010-08-10 |
| | | | | | Chalice | ||
| * | Chalice: forcefully kill Boogie with taskkill /T /F on termination | kyessenov | 2010-08-10 |
| | | |||
| * | Chalice: refinement of a list with nodes (instead of lists pointing to sublists) | kyessenov | 2010-08-06 |
| | | |||
| * | Chalice: terminate Boogie subprocess manually on interrupt; Z3 still stays ↵ | kyessenov | 2010-08-06 |
| | | | | | alive though??? | ||
| * | Chalice: still cannot verify refinement of List.get (Z3 goes out of memory); ↵ | kyessenov | 2010-08-06 |
| | | | | | added classic sqrt refinement; assertions on acc(s[*].f) have now positions attached | ||
| * | Chalice: try using output coupling assertion as loop invariant | kyessenov | 2010-08-05 |
| | | |||
| * | Chalice: testing refinement of a linked list | kyessenov | 2010-08-04 |
| | | |||
| * | Chalice: testing refinement of Counter | kyessenov | 2010-08-04 |
| | | |||
| * | Chalice: abstract Shorr-Waite algorithm verified | kyessenov | 2010-08-03 |
| | | |||
| * | Chalice: deriving SchorrWaite algorithm with Chalice | kyessenov | 2010-08-03 |
| | | |||
| * | Chalice: added Tarjan's SCC algorithm for computing function call graph and ↵ | kyessenov | 2010-08-03 |
| | | | | | recursion bits | ||
| * | Chalice: | kyessenov | 2010-08-02 |
| | | | | | | | | * change syntax for range: [a..b] instead of [a:b] * add multi-triggers to Boogie bindings * fix unsoundness in frame axiom for functions -- whenever acc(s[*].f,...) is detected in pre-condition, a different encoding to Boogie is applied * add limited functions to translator (disabled since Resolver is not ready yet) | ||
| * | Chalice: | kyessenov | 2010-08-02 |
| | | | | | | | * added quantifiers over any type (forall i: int :: i + 1 == i + 1) * cleaned up AST transformation code; organized one transform operation that should preserve source positions -- it was very annoying to see assertions with lost source positions * added a desugar method that simplifies Chalice AST by unrolling a few constructs -- maybe useful in the future to quickly add a syntactic sugar | ||
| * | Chalice: | kyessenov | 2010-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) | ||
| * | Chalice: pretty printer now prints element type for sequences; fixed a bug ↵ | kyessenov | 2010-07-27 |
| | | | | | in copying resolved member in sequence accesses; added graph closure (DSW) verification example | ||
| * | Chalice: bug -- permissions were implicity converted to Booge expressions ↵ | kyessenov | 2010-07-22 |
| | | | | | (due to "implicit def") | ||
| * | Chalice: bug -- expression substitution should preserve typing | kyessenov | 2010-07-22 |
| | | |||
| * | Chalice: sequence access wildcards a[*].* and a[*].f have been implemented ↵ | kyessenov | 2010-07-22 |
| | | | | | (sans checking for epsilon going beyond infinity and rd(...,*) permissions) | ||
| * | Chalice: introduced proper AST nodes for permission expressions and ↵ | kyessenov | 2010-07-21 |
| | | | | | permissions. This gets of redundancy in treating acc and rd in many places and should hopefully make permissions code more comprehensible | ||
| * | Chalice: fixed typos in strings; trying out committing with TFS | kyessenov | 2010-07-21 |
| | | |||
| * | Chalice: added surface syntax for acc(s[*].*) and acc(s[*].f); extended AST, ↵ | kyessenov | 2010-07-20 |
| | | | | | resolver, printer; translation is not yet done | ||
| * | Chalice: fixed a bug with permission operations treating AccessAll not as a ↵ | kyessenov | 2010-07-20 |
| | | | | | permission expression; refactored Translator my moving prelude/implicits into TranslatorHelper for consistency | ||
| * | Chalice: added type information for sequences ("where" clauses in local ↵ | kyessenov | 2010-07-20 |
| | | | | | variable declarations and method/function formals); the clause says that every element in a sequence is either null or its dtype is the element type | ||
| * | Chalice: adding support for sequence local variables; removed ClassType from ↵ | kyessenov | 2010-07-20 |
| | | | | | Boogie since it was maskng bad job done by Translator; fixing warnings in case we ever decide to switch to newer Scala compiler | ||
| * | Chalice: extended substitutor to handle "exists" quantifier and sequence ↵ | kyessenov | 2010-07-20 |
| | | | | | containment; refactoring and preparing to extend wild card permissions to sequences | ||
| * | VS2010 integration: fixed typo in Boogie mode (install for .bpl files, not ↵ | rustanleino | 2010-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: added sequence containment surface syntax ("in" comparison ↵ | kyessenov | 2010-07-19 |
| | | | | | operator); cleaned up some deprecation warnings; resolved ambiguity with "unfolding ... in" expression | ||
| * | Chalice: Introduced '[[ S ]]' as a shorthand syntax for 'lock (this) { S ↵ | rustanleino | 2010-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 | ||
| * | Chalice: added "exists" quantifier; changed surface syntax for quantifier ↵ | kyessenov | 2010-07-19 |
| | | | | | expressions | ||
| * | Chalice: Re-designed lockchange on methods and loops. The lockchange clause ↵ | mueller | 2010-07-18 |
| | | | | | is now required to list all objects whose held or rdheld field has changed since the _method_ prestate. It seems desirable to exclude objects that were not allocated in the prestate, but this feature is not implemented yet. | ||
| * | Chalice: Removed the restriction that "holds" must occur only in positive ↵ | mueller | 2010-07-16 |
| | | | | | positions. | ||
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |