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
*
Beefed up assign/let-such-that to generate possible witnesses for set/multise...
Rustan Leino
2013-03-25
*
Updated two test files.
Rustan Leino
2013-03-22
*
Merge
Nadia Polikarpova
2013-03-20
|
\
*
|
Finished support for ==# in calc, changed Paulson example to use it.
Nadia Polikarpova
2013-03-20
|
*
Added multiset update.
Nadia Polikarpova
2013-03-20
|
/
*
Added a coinductive/inductive Filter example to the test suite
Rustan Leino
2013-03-18
*
Merge
Rustan Leino
2013-03-15
|
\
*
|
Fixed yield statement to process its arguments.
Rustan Leino
2013-03-15
|
*
Added several co-induction examples from a 1996 paper by Larry Paulson.
Rustan Leino
2013-03-15
|
*
Added explies support to calculations.
Nadia Polikarpova
2013-03-15
|
*
Added a test case for <==.
Nadia Polikarpova
2013-03-14
|
/
*
Adjustments in the /vcsMaxKeepGoingSplits flag in the test suite
Rustan Leino
2013-03-09
*
Disallow allocations in ghost contexts
Rustan Leino
2013-03-06
*
New Answer file from previous change
Rustan Leino
2013-03-06
*
Renamed "parallel" statement to "forall" statement, and made the parentheses ...
Rustan Leino
2013-03-06
*
New well-formedness checks for calculations (no cascading).
Nadia Polikarpova
2013-03-05
*
Added side-effects and control-flow checks in hints.
Nadia Polikarpova
2013-03-05
*
Adjustment in test output from previous commit
Rustan Leino
2013-02-21
*
Fixed let-such-that and if-then-else encodings so that they will pass the sub...
Rustan Leino
2013-02-21
*
Added Equals method on Type
Rustan Leino
2013-02-20
*
Added tests: parallel calc, better well-formedness checks, calc expression.
Nadia Polikarpova
2013-02-15
*
Support for paren-free guards in if and while statements.
Nadia Polikarpova
2013-02-15
*
Updated a test in dafny2 with the new calc syntax.
Nadia Polikarpova
2013-02-14
*
Merge
Nadia Polikarpova
2013-02-13
|
\
|
*
Frame expressions are now checked to be well formed.
Rustan Leino
2013-02-13
*
|
Merge
Nadia Polikarpova
2013-02-14
|
\
|
|
*
Report error if type of a quantified variable cannot be inferred
Rustan Leino
2013-02-11
*
|
Merge
Nadia Polikarpova
2013-02-12
|
\
|
|
*
Reverted some accidental changes to a test case
Rustan Leino
2013-02-11
*
|
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
*
Renamed a variable in some test cases
Rustan Leino
2013-02-02
*
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
[next]