index
:
debian-boogie
dfsg_free
master
Debian packaging for Boogie
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Source
/
Dafny
/
Translator.cs
Commit message (
Expand
)
Author
Age
*
Dafny: removed allocated, changed semantics of fresh
Jason Koenig
2012-07-29
*
Dafny: added structural refinement check
Jason Koenig
2012-07-29
*
Dafny: restored soundness for refinement by disallowing certain updates and m...
Jason Koenig
2012-07-11
*
Dafny: fixed translation bug in maps with objects in the domain, added test case
Jason Koenig
2012-07-11
*
Dafny: fixed bad merge
Rustan Leino
2012-07-09
*
Merge
Rustan Leino
2012-07-09
|
\
*
|
Dafny: More work on the coinduction principle
Rustan Leino
2012-07-09
|
*
Dafny: added verification that replaced expressions are the same as the original
Jason Koenig
2012-07-09
|
*
Dafny: added named expressions and replacement
Jason Koenig
2012-07-09
*
|
Merge
Rustan Leino
2012-07-04
|
\
|
|
*
Dafny: added support for nested abstract modules, fixed some translation issues
Jason Koenig
2012-07-03
*
|
Dafny: removed old Substitute method (which has been replaced by a Substitute...
Rustan Leino
2012-07-03
*
|
Dafny: added copredicates
Rustan Leino
2012-07-03
|
*
Dafny: re-added field non-uniqueness (was accidentally reverted by a bad merge)
Jason Koenig
2012-07-02
|
/
*
Dafny: fixed bug with translation of class._System.object;
Jason Koenig
2012-06-28
*
Dafny: Merge
Jason Koenig
2012-06-27
|
\
*
|
Dafny: Implemented abstract modules
Jason Koenig
2012-06-26
|
*
Dafny: improved refinement features; added staged version of the proof of the...
Unknown
2012-06-19
*
|
Dafny: Added nested modules
Jason Koenig
2012-06-19
|
/
*
Merge
Jason Koenig
2012-06-13
|
\
*
|
Dafny: allow parallel assignments to assign to the same LHS if the RHS match.
Jason Koenig
2012-06-13
|
*
Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to c...
Unknown
2012-06-13
|
/
*
Dafny: allow types to be qualified with the name of the module that declares ...
Unknown
2012-06-11
*
Dafny: removed support for the old keyword "unlimited" (all functions are lim...
Unknown
2012-06-11
*
Dafny: change labels to use a generic singly linked list
Jason Koenig
2012-06-06
*
Dafny: Added map comprehensions and updated display syntax
Unknown
2012-05-31
*
Dafny: added finite maps
Unknown
2012-05-25
*
Dafny: more correct checking of co-inductive productivity
Unknown
2012-05-18
*
Dafny: improve printing of inductive datatypes
Unknown
2012-05-01
*
Dafny: added support for co-recursive calls
Rustan Leino
2012-05-01
*
Dafny: rudimentary translation into Boogie of co-inductive datatypes
Unknown
2012-04-25
*
Dafny: fixed bug (missing Boogie cast) in translation of induction over gener...
Unknown
2012-04-20
*
Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr;
Unknown
2012-03-15
*
Dafny: fixed build error
Rustan Leino
2012-03-09
*
Dafny: added ghost modules (the meaning is simply that such a module will not...
Rustan Leino
2012-03-07
*
Dafny: fixed well-formedness checking of LET expressions to allow the RHS to ...
Rustan Leino
2012-02-29
*
Dafny: make sure assume->assert transformation gives rise to a check
Rustan Leino
2012-02-19
*
Dafny: improved error location for violations of function postconditions
Rustan Leino
2012-01-18
*
Dafny: allow parallel statements with an empty list of bound variables
Rustan Leino
2012-01-17
*
Dafny: parallel statements:
Rustan Leino
2012-01-17
*
Dafny: Recheck specifications that contain refined (extended) predicates, eve...
Rustan Leino
2012-01-16
*
Dafny: handle refinement of nested tokens that come from SpliExpr (still need...
Rustan Leino
2012-01-12
*
Dafny: make full predicate definitions available only inside a module (outsid...
Rustan Leino
2012-01-11
*
Dafny: fixed bugs in contract types, and a code bug that caused a contract to...
Rustan Leino
2012-01-10
*
Dafny: some bug fixes
Rustan Leino
2012-01-10
*
Dafny: allow definitions and uses of parameter-less predicates to go without ...
Rustan Leino
2012-01-10
*
Dafny: changed translation to be sensitive to refinement inheritance; this fe...
Rustan Leino
2012-01-09
*
Dafny: fully qualify (with module names) names of types in the translation in...
Rustan Leino
2012-01-05
*
Dafny: Start of new refinement features -- clean out old ones
Rustan Leino
2012-01-04
*
Dafny: for a datatype with just one constructor, don't check (but do assume) ...
Rustan Leino
2011-12-19
[next]