| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires |  qunyanm | 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" | qunyanm | 2016-02-02 |
| | | |||
| * | Made /rewriteFocalPredicates:1 the default | Rustan Leino | 2015-10-02 |
| | | |||
| * | Merge |  Clément Pit--Claudel | 2015-09-02 |
| |\ | |||
| * | | Implement workarounds for some tests that fail with /autoTriggers. | Clément Pit--Claudel | 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. | Clément Pit--Claudel | 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 | Rustan Leino | 2015-08-28 |
| |/ | |||
| * | Changed dafny3/Filter.dfy to use higher-order functions instead of the ↵ | leino | 2015-08-12 |
| | | | | | previous function handles | ||
| * | Change the induction heuristic for lemmas to also look in precondition for ↵ | leino | 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 ↵ | Rustan Leino | 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 | Clément Pit--Claudel | 2015-07-20 |
| | | |||
| * | Reflect cleaner syntax in some test programs | leino | 2015-03-31 |
| | | |||
| * | This changeset changes the default visibility of a function/predicate body ↵ | leino | 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. | qunyanm | 2015-03-05 |
| | | |||
| * | Language change: All functions and methods declared lexically outside any ↵ | leino | 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 ↵ | Rustan Leino | 2014-08-12 |
| | | | | | automatic triggering support in either Dafny or Boogie) | ||
| * | Another variation of GenericSort, this time instantiating with "int" | Rustan Leino | 2014-07-14 |
| | | |||
| * | Tidy up two files in test suite |  Dan Rosen | 2014-07-07 |
| | | |||
| * | Merge | Dan Rosén | 2014-07-07 |
| |\ | |||
| * | | New logical encoding of types with Is and IsAlloc | Dan Rosén | 2014-07-07 |
| | | | |||
| | * | Removed the old test infrastructure. | wuestholz | 2014-07-01 |
| |/ | |||
| * | Set up the same test infrastructure as in Boogie. | wuestholz | 2014-05-29 |
| | | |||
| * | Improvements in sequence axioms to make checking more automatic. | Rustan Leino | 2014-04-02 |
| | | | | | Minor changes in a test file. | ||
| * | Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵ | Rustan Leino | 2014-02-23 |
| | | | | | -> "prefix lemma") | ||
| * | Add pretty-printing flag to the dafny3 test script. | wuestholz | 2013-12-19 |
| | | |||
| * | Added test3/GenericSort.dfy, which shows how modules can be used to write ↵ | Rustan Leino | 2013-12-18 |
| | | | | | and use a sorting routine parameterized with a comparison function | ||
| * | Added missing file (sorry) | Rustan Leino | 2013-12-18 |
| | | |||
| * | Add support for the /verifySeparately flag in Boogie and change most tests ↵ | wuestholz | 2013-12-18 |
| | | | | | to use it. | ||
| * | Don't inline opaque functions. | Rustan Leino | 2013-12-17 |
| | | | | | Added a verifying example with opaque functions and explicit proofs. | ||
| * | Added some test cases: theorem about infinite and finite trees. | Rustan Leino | 2013-07-27 |
| | | |||
| * | Syntactic improvements in two tests. | Rustan Leino | 2013-07-16 |
| | | |||
| * | Added some test cases having to do with finite/infinite trees | Rustan Leino | 2013-07-10 |
| | | |||
| * | Fixed soundness bug with co-recursive calls: co-recursive calls may now no ↵ |  Rustan Leino | 2013-06-29 |
| | | | | | longer to to functions with ensures clauses | ||
| * | Updated two test files. | Rustan Leino | 2013-03-22 |
| | | |||
| * | Finished support for ==# in calc, changed Paulson example to use it. |  Nadia Polikarpova | 2013-03-20 |
| | | |||
| * | Added a coinductive/inductive Filter example to the test suite | Rustan Leino | 2013-03-18 |
| | | |||
| * | Added several co-induction examples from a 1996 paper by Larry Paulson. | Rustan Leino | 2013-03-15 |
| | | |||
| * | Renamed "parallel" statement to "forall" statement, and made the parentheses ↵ | Rustan Leino | 2013-03-06 |
| | | | | | around the bound variables optional. | ||
| * | Changed calc syntax (custom operators are now written before the hint) | Nadia Polikarpova | 2013-02-08 |
| | | |||
| * | Added some test cases that show exmaples that iterate over set elements. | Rustan Leino | 2013-02-02 |
| | | |||
| * | Examples from co-induction paper | Rustan Leino | 2013-01-22 |
| | | |||
| * | More automatic co-induction for comethods | Rustan Leino | 2013-01-20 |
| | | |||
| * | Added some co- test cases. Fixed some bugs. | Rustan Leino | 2013-01-20 |
| | | |||
| * | Removed the syntactic form copredicate #-form with the implicit argument. | Rustan Leino | 2013-01-16 |
| | | | | | Added syntactic support for codatatype #-form equalities. | ||
| * | renamed "abstract module" to "module facade" | Rustan Leino | 2012-10-22 |
| | | | | | renamed "ghost module" to "abstract module", adding a keyword "abstract" | ||
| * | allow a refinement to introduce "return" statements, at the price of ↵ | Rustan Leino | 2012-10-22 |
| | | | | | | | re-verifying the postcondition at that time let refined classes inherit attributes | ||
| * | added some calculational proofs from Dijkstra's writings | Rustan Leino | 2012-10-21 |
| | | |||
| * | Test cases for co-inductive proofs, and an axiom that makes some of them ↵ | Rustan Leino | 2012-10-19 |
| | | | | | possible | ||
| * | Support default (which, here, means nameless) class-instance constructors | Rustan Leino | 2012-10-05 |
| | | |||
| * | Fixed some goof-ups in the test script edits | Rustan Leino | 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 | ||
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |