Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires | 2016-03-28 | |
| | | | | | it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run. | ||
* | Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B" | 2016-02-02 | |
| | |||
* | Made /rewriteFocalPredicates:1 the default | 2015-10-02 | |
| | |||
* | Merge | 2015-09-02 | |
|\ | |||
* | | Implement workarounds for some tests that fail with /autoTriggers. | 2015-08-28 | |
| | | | | | | | | | | | | The issues here are mostly with induction (wrt. to trigger selection and quantifier splitting) and with expressions like P(i, j-1) where no good choices are available. | ||
* | | Suppress many warnings in the test suite. | 2015-08-28 | |
| | | | | | | | | | | We already have separate tests for those, and we want the output to be the same with and without /autoTriggers. | ||
| * | Fixed spelling mistake in test file | 2015-08-28 | |
|/ | |||
* | Changed dafny3/Filter.dfy to use higher-order functions instead of the ↵ | 2015-08-12 | |
| | | | | previous function handles | ||
* | Change the induction heuristic for lemmas to also look in precondition for ↵ | 2015-08-12 | |
| | | | | | | clues about which parameters to include. As a result, improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and beautified some others. | ||
* | Renamed "ghost method" to "lemma" whenever appropriate (which is most of the ↵ | 2015-07-28 | |
| | | | | | | time) in the test suite. Removed some assertions that have been rendered unnecessary because of the computations that Dafny instructs the SMT solver to do. | ||
* | Fix encoding in Dijkstra.py | 2015-07-20 | |
| | |||
* | Reflect cleaner syntax in some test programs | 2015-03-31 | |
| | |||
* | This changeset changes the default visibility of a function/predicate body ↵ | 2015-03-09 | |
| | | | | | | | | | | outside the module that declares it. The body is now visible across the module boundary. To contain the knowledge of the body inside the module, mark the function/predicate as 'protected'. Semantics of 'protected': * The definition (i.e., body) of a 'protected' function is not visible outside the defining module * The idea is that inside the defining module, a 'protected' function may or may not be opaque. However, this will be easier to support once opaque/reveal are language primitives. Therefore, for the time being, {:opaque} is not allowed to be applied to 'protected' functions. * In order to extend the definition of a predicate in a refinement module, the predicate must be 'protected' * The 'protected' status of a function must be preserved in refinement modules | ||
* | Stop pretty-print from emitting deprecated semi-colons. | 2015-03-05 | |
| | |||
* | Language change: All functions and methods declared lexically outside any ↵ | 2014-12-12 | |
| | | | | | | | | | | class are now automatically static, and fields are no longer allowed to be declared there. Stated differently, all heap state must now be declared inside an explicitly declared class, and functions and methods declared outside any class can be viewed as belonging to the module. The motivating benefit of this change is to no longer need the 'static' keyword when declaring a module of functions and methods. | ||
* | Rewrote two tests to make triggering better (while waiting for better ↵ | 2014-08-12 | |
| | | | | automatic triggering support in either Dafny or Boogie) | ||
* | Another variation of GenericSort, this time instantiating with "int" | 2014-07-14 | |
| | |||
* | Tidy up two files in test suite | 2014-07-07 | |
| | |||
* | Merge | 2014-07-07 | |
|\ | |||
* | | New logical encoding of types with Is and IsAlloc | 2014-07-07 | |
| | | |||
| * | Removed the old test infrastructure. | 2014-07-01 | |
|/ | |||
* | Set up the same test infrastructure as in Boogie. | 2014-05-29 | |
| | |||
* | Improvements in sequence axioms to make checking more automatic. | 2014-04-02 | |
| | | | | Minor changes in a test file. | ||
* | Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵ | 2014-02-23 | |
| | | | | -> "prefix lemma") | ||
* | Add pretty-printing flag to the dafny3 test script. | 2013-12-19 | |
| | |||
* | Added test3/GenericSort.dfy, which shows how modules can be used to write ↵ | 2013-12-18 | |
| | | | | and use a sorting routine parameterized with a comparison function | ||
* | Added missing file (sorry) | 2013-12-18 | |
| | |||
* | Add support for the /verifySeparately flag in Boogie and change most tests ↵ | 2013-12-18 | |
| | | | | to use it. | ||
* | Don't inline opaque functions. | 2013-12-17 | |
| | | | | Added a verifying example with opaque functions and explicit proofs. | ||
* | Added some test cases: theorem about infinite and finite trees. | 2013-07-27 | |
| | |||
* | Syntactic improvements in two tests. | 2013-07-16 | |
| | |||
* | Added some test cases having to do with finite/infinite trees | 2013-07-10 | |
| | |||
* | Fixed soundness bug with co-recursive calls: co-recursive calls may now no ↵ | 2013-06-29 | |
| | | | | longer to to functions with ensures clauses | ||
* | Updated two test files. | 2013-03-22 | |
| | |||
* | Finished support for ==# in calc, changed Paulson example to use it. | 2013-03-20 | |
| | |||
* | Added a coinductive/inductive Filter example to the test suite | 2013-03-18 | |
| | |||
* | Added several co-induction examples from a 1996 paper by Larry Paulson. | 2013-03-15 | |
| | |||
* | Renamed "parallel" statement to "forall" statement, and made the parentheses ↵ | 2013-03-06 | |
| | | | | around the bound variables optional. | ||
* | Changed calc syntax (custom operators are now written before the hint) | 2013-02-08 | |
| | |||
* | Added some test cases that show exmaples that iterate over set elements. | 2013-02-02 | |
| | |||
* | Examples from co-induction paper | 2013-01-22 | |
| | |||
* | More automatic co-induction for comethods | 2013-01-20 | |
| | |||
* | Added some co- test cases. Fixed some bugs. | 2013-01-20 | |
| | |||
* | Removed the syntactic form copredicate #-form with the implicit argument. | 2013-01-16 | |
| | | | | Added syntactic support for codatatype #-form equalities. | ||
* | renamed "abstract module" to "module facade" | 2012-10-22 | |
| | | | | renamed "ghost module" to "abstract module", adding a keyword "abstract" | ||
* | allow a refinement to introduce "return" statements, at the price of ↵ | 2012-10-22 | |
| | | | | | | re-verifying the postcondition at that time let refined classes inherit attributes | ||
* | added some calculational proofs from Dijkstra's writings | 2012-10-21 | |
| | |||
* | Test cases for co-inductive proofs, and an axiom that makes some of them ↵ | 2012-10-19 | |
| | | | | possible | ||
* | Support default (which, here, means nameless) class-instance constructors | 2012-10-05 | |
| | |||
* | Fixed some goof-ups in the test script edits | 2012-10-04 | |
| | | | | Changed the test output to make it easier to spot (in the console output) that everything passed with success or if there were any failures |