summaryrefslogtreecommitdiff
path: root/Test
Commit message (Collapse)AuthorAge
...
* Support for paren-free guards in if and while statements.Gravatar Nadia Polikarpova2013-02-15
|
* Updated a test in dafny2 with the new calc syntax.Gravatar Nadia Polikarpova2013-02-14
|
* MergeGravatar Nadia Polikarpova2013-02-13
|\
| * Frame expressions are now checked to be well formed.Gravatar Rustan Leino2013-02-13
| | | | | | | | (A nice consequence of this is that the method IsTotal is no longer needed.)
* | MergeGravatar Nadia Polikarpova2013-02-14
|\|
| * Report error if type of a quantified variable cannot be inferredGravatar Rustan Leino2013-02-11
| |
* | MergeGravatar Nadia Polikarpova2013-02-12
|\|
| * Reverted some accidental changes to a test caseGravatar Rustan Leino2013-02-11
| |
* | Changed calc syntax (custom operators are now written before the hint)Gravatar Nadia Polikarpova2013-02-08
|/
* Added some test cases that show exmaples that iterate over set elements.Gravatar Rustan Leino2013-02-02
|
* Renamed a variable in some test casesGravatar Rustan Leino2013-02-02
|
* Fixed another specification bug in a test case.Gravatar Rustan Leino2013-01-23
|
* Fixed bug in translation of method termination checks, and also fixed a ↵Gravatar Rustan Leino2013-01-23
| | | | (previously undetected) specification bug in the test suite.
* Split verification of quantifier expressions into #2 for checked and #1 for ↵Gravatar Rustan Leino2013-01-23
| | | | | | assumed. Fixed cases where token was not being updated for refinement.
* Examples from co-induction paperGravatar Rustan Leino2013-01-22
|
* Translate let-such-that expressionsGravatar Rustan Leino2013-01-22
|
* More automatic co-induction for comethodsGravatar Rustan Leino2013-01-20
|
* Added some co- test cases. Fixed some bugs.Gravatar Rustan Leino2013-01-20
|
* Fixed the problem with the previous check-in.Gravatar Rustan Leino2013-01-18
|
* Some additional resolution checks for co stuff.Gravatar Unknown2013-01-18
| | | | Beefed up some test cases.
* Proper support for inlining codatatype equalitiesGravatar Rustan Leino2013-01-18
|
* Removed the syntactic form copredicate #-form with the implicit argument.Gravatar Rustan Leino2013-01-16
| | | | Added syntactic support for codatatype #-form equalities.
* Encode codatatype equalities by predefined copredicates, including their ↵Gravatar Rustan Leino2013-01-15
| | | | prefix versions
* Support for copredicates and prefix predicates in comethods.Gravatar Rustan Leino2012-12-04
| | | | | | (Missing from the co support are (prefix) equalities of codatatypes, various restrictions on the use of co/prefix-predicates, and tactic support for applying the (prefix-)induction automatically.)
* Parse prefix predicates/methodsGravatar Rustan Leino2012-11-24
|
* Beefed up loop invariant to prove a functional postcondition in a test case.Gravatar Rustan Leino2012-11-24
|
* fixed type resolution bug (http://boogie.codeplex.com/discussions/403801)Gravatar Rustan Leino2012-11-20
|
* Beautified a test programGravatar Rustan Leino2012-11-19
|
* renamed "abstract module" to "module facade"Gravatar Rustan Leino2012-10-22
| | | | renamed "ghost module" to "abstract module", adding a keyword "abstract"
* allow a refinement to introduce "return" statements, at the price of ↵Gravatar Rustan Leino2012-10-22
| | | | | | re-verifying the postcondition at that time let refined classes inherit attributes
* added some calculational proofs from Dijkstra's writingsGravatar Rustan Leino2012-10-21
|
* Test cases for co-inductive proofs, and an axiom that makes some of them ↵Gravatar Rustan Leino2012-10-19
| | | | possible
* added two "calc" proofs (by Nadia) of the MajorityVote exampleGravatar Unknown2012-10-19
|
* fixed and improved scheme for inferring type parametersGravatar Rustan Leino2012-10-19
|
* Added a test case for "all cases of a datatype"Gravatar Unknown2012-10-17
|
* Included "all cases of a datatype" property for method in-parameters (see ↵Gravatar Unknown2012-10-17
| | | | http://boogie.codeplex.com/discussions/397616).
* Added some axioms to try to recover boxed data. In particular, any element ↵Gravatar Unknown2012-10-17
| | | | 'x' of a set in the encoding satisfies Box(Unbox(x))==x. The soundness and performance of the axiomatization are dicey, so the axioms are made available only to method in-parameters.
* Added/fixed decreases clauses that use multisets or maps.Gravatar Unknown2012-10-16
|
* Change the encoding of proof certificates to make the two levels explicitGravatar Unknown2012-10-12
| | | | Restrict what conclusions comethods are allowed to have
* Removed some old code for the defunct array-range assignmentsGravatar Rustan Leino2012-10-11
|
* Removed the old (though automatic) coinduction principleGravatar Rustan Leino2012-10-11
|
* New feature:Gravatar Rustan Leino2012-10-11
| | | | | | | * Added "comethod" declarations and support for writing manual co-inductive proofs (but currently blindly assume comethod postconditions to, in positive positions, only have copredicates and codatatype equalities--other cases still need to be dealt with) Code restructuring: * New set of Boogie procedure stubs generated for each other * Start of improvements around TrSplitExpr
* improved and fixed compilation and resolution of assign-such-that statementsGravatar Rustan Leino2012-10-05
|
* Longer output lines to indicate failures in regression test suiteGravatar Rustan Leino2012-10-05
|
* Support default (which, here, means nameless) class-instance constructorsGravatar Rustan Leino2012-10-05
|
* Fixed some goof-ups in the test script editsGravatar Rustan Leino2012-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
* Added Test/dafny3 and another test file for iterators (hey, you can even run ↵Gravatar Rustan Leino2012-10-04
| | | | | | Iter.dfy!) Fixed migration issues
* changed default decreases clause for functions with a reads clause: use the ↵Gravatar Rustan Leino2012-10-04
| | | | reads clause followed by the list of parameters
* Fixed some build/migration issuesGravatar Rustan Leino2012-10-04
|
* Dafny: fixed mergeGravatar Rustan Leino2012-10-04
|