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
/
Dafny.atg
Commit message (
Expand
)
Author
Age
*
Dafny: removed allocated, changed semantics of fresh
Jason Koenig
2012-07-29
*
Dafny: compilation of abstract modules, including local definitions (as in mo...
Jason Koenig
2012-07-17
*
Dafny: allow implict self (as in "`field") in frame declarations.
Jason Koenig
2012-07-16
*
Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to ...
Jason Koenig
2012-07-10
*
Merge
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
|
*
Dafny: types can now be qualified with full module paths
Jason Koenig
2012-07-06
*
|
Merge
Rustan Leino
2012-07-04
|
\
|
|
*
Dafny: added support for nested abstract modules, fixed some translation issues
Jason Koenig
2012-07-03
*
|
Merge
Rustan Leino
2012-07-03
|
\
|
*
|
Dafny: added copredicates
Rustan Leino
2012-07-03
|
*
Dafny: reinstated autocontracts
Jason Koenig
2012-07-02
|
/
*
Dafny: Merge
Jason Koenig
2012-06-27
|
\
*
|
Dafny: fixed bug in which _module scope declarations were not verified.
Jason Koenig
2012-06-27
*
|
Dafny: Implemented abstract modules
Jason Koenig
2012-06-26
|
*
Dafny: allow "assume ..." as a refining statement (provided it replaces an "a...
Unknown
2012-06-22
|
*
Dafny: Since it's no longer true that all types support equality at run-time ...
Unknown
2012-06-21
|
*
Merge
Unknown
2012-06-19
|
|
\
|
*
|
Dafny: improved refinement features; added staged version of the proof of the...
Unknown
2012-06-19
*
|
|
Dafny: disallow declare identifiers starting with underscore (_)
Jason Koenig
2012-06-19
*
|
|
Dafny: Added nested modules
Jason Koenig
2012-06-19
|
|
/
|
/
|
*
|
Dafny: fixed parsing bug.
Jason Koenig
2012-06-15
|
/
*
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: fixed resolution bug for inductive datatypes (previous check did not h...
Unknown
2012-04-25
*
Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr;
Unknown
2012-03-15
*
Dafny: added ghost modules (the meaning is simply that such a module will not...
Rustan Leino
2012-03-07
*
Dafny: allow more skeleton statements in refinements
Unknown
2012-03-02
*
Dafny: added syntactic support for ...'s in statements, and started implement...
Unknown
2012-02-18
*
Dafny: allow signatures to be omitted on refining functions/methods
Unknown
2012-02-16
*
Dafny: allow parallel statements with an empty list of bound variables
Rustan Leino
2012-01-17
*
Dafny: Recheck specifications that contain refined (extended) predicates, eve...
Rustan Leino
2012-01-16
*
Dafny: allow class-member declarations at top level of any module (not just t...
Rustan Leino
2012-01-10
*
Dafny: added test case for refinement and predicates (and fixed a parsing bug)
Rustan Leino
2012-01-10
*
Dafny: allow definitions and uses of parameter-less predicates to go without ...
Rustan Leino
2012-01-10
*
Dafny: added predicates
Rustan Leino
2012-01-10
*
Dafny: firmed up the module system
Rustan Leino
2012-01-05
*
Dafny: Start of new refinement features -- clean out old ones
Rustan Leino
2012-01-04
*
Dafny: Extended the support for attributes on method/constructor calls.
wuestholz
2011-12-23
*
Dafny: Added support for attributes on method/constructor calls.
wuestholz
2011-12-21
*
Dafny: Added support for attributes on various specification constructs (asse...
wuestholz
2011-12-07
*
Dafny: corrected merge snafus
Rustan Leino
2011-12-07
*
Merge
Rustan Leino
2011-12-07
|
\
[next]