| Commit message (Collapse) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | Introduced operator !in in Dafny. An expression "x !in S" is equivalent to ↵ |  rustanleino | 2009-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. | rustanleino | 2009-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 channels | rustanleino | 2009-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. | mikebarnett | 2009-07-15 | |
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |