index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Test
Commit message (
Expand
)
Author
Age
*
Fixed another specification bug in a test case.
Rustan Leino
2013-01-23
*
Fixed bug in translation of method termination checks, and also fixed a (prev...
Rustan Leino
2013-01-23
*
Split verification of quantifier expressions into #2 for checked and #1 for a...
Rustan Leino
2013-01-23
*
Examples from co-induction paper
Rustan Leino
2013-01-22
*
Translate let-such-that expressions
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
*
Fixed the problem with the previous check-in.
Rustan Leino
2013-01-18
*
Some additional resolution checks for co stuff.
Unknown
2013-01-18
*
Proper support for inlining codatatype equalities
Rustan Leino
2013-01-18
*
Removed the syntactic form copredicate #-form with the implicit argument.
Rustan Leino
2013-01-16
*
Encode codatatype equalities by predefined copredicates, including their pref...
Rustan Leino
2013-01-15
*
Support for copredicates and prefix predicates in comethods.
Rustan Leino
2012-12-04
*
Parse prefix predicates/methods
Rustan Leino
2012-11-24
*
Beefed up loop invariant to prove a functional postcondition in a test case.
Rustan Leino
2012-11-24
*
fixed type resolution bug (http://boogie.codeplex.com/discussions/403801)
Rustan Leino
2012-11-20
*
Beautified a test program
Rustan Leino
2012-11-19
*
renamed "abstract module" to "module facade"
Rustan Leino
2012-10-22
*
allow a refinement to introduce "return" statements, at the price of re-verif...
Rustan Leino
2012-10-22
*
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 poss...
Rustan Leino
2012-10-19
*
added two "calc" proofs (by Nadia) of the MajorityVote example
Unknown
2012-10-19
*
fixed and improved scheme for inferring type parameters
Rustan Leino
2012-10-19
*
Added a test case for "all cases of a datatype"
Unknown
2012-10-17
*
Included "all cases of a datatype" property for method in-parameters (see htt...
Unknown
2012-10-17
*
Added some axioms to try to recover boxed data. In particular, any element '...
Unknown
2012-10-17
*
Added/fixed decreases clauses that use multisets or maps.
Unknown
2012-10-16
*
Change the encoding of proof certificates to make the two levels explicit
Unknown
2012-10-12
*
Removed some old code for the defunct array-range assignments
Rustan Leino
2012-10-11
*
Removed the old (though automatic) coinduction principle
Rustan Leino
2012-10-11
*
New feature:
Rustan Leino
2012-10-11
*
improved and fixed compilation and resolution of assign-such-that statements
Rustan Leino
2012-10-05
*
Longer output lines to indicate failures in regression test suite
Rustan Leino
2012-10-05
*
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
*
Added Test/dafny3 and another test file for iterators (hey, you can even run ...
Rustan Leino
2012-10-04
*
changed default decreases clause for functions with a reads clause: use the r...
Rustan Leino
2012-10-04
*
Fixed some build/migration issues
Rustan Leino
2012-10-04
*
Dafny: fixed merge
Rustan Leino
2012-10-04
*
Merge
Rustan Leino
2012-10-04
|
\
*
|
Dafny: complete implementation of iterators
Rustan Leino
2012-10-03
*
|
Dafny: automatically update iterator _new field upon allocations
Rustan Leino
2012-10-03
*
|
Dafny: good error locations for yield statements; other iterator improvements...
Rustan Leino
2012-10-03
*
|
Dafny: more part of verifying iterators
Rustan Leino
2012-10-03
*
|
Dafny: changed iterator body to resolve to implicit fields rather than to the...
Rustan Leino
2012-10-02
*
|
Dafny: incomplete snapshot of verification of iterators
Rustan Leino
2012-10-02
|
*
Merge
Nadia Polikarpova
2012-09-29
|
|
\
|
|
*
Dafny: removed div/mod axioms, since Boogie now interprets div/mod
Unknown
2012-09-28
|
|
*
Boogie and Dafny: adjustments to the test suite expected output (and a tempor...
Unknown
2012-09-27
*
|
|
Dafny: compile iterators
Rustan Leino
2012-09-26
[next]