index
:
debian-dafny
master
Debian packaging for Dafny
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Dafny
/
RefinementTransformer.cs
Commit message (
Expand
)
Author
Age
*
Dafny: added contracts to IRewriter methods
Unknown
2012-06-22
*
Dafny: allow "assume ..." as a refining statement (provided it replaces an "a...
Unknown
2012-06-22
*
Dafny: deal with equality-support issues in refinements
Unknown
2012-06-22
*
Dafny: Since it's no longer true that all types support equality at run-time ...
Unknown
2012-06-21
*
Dafny: improved refinement features; added staged version of the proof of the...
Unknown
2012-06-19
*
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: fixed bug in type cloning, as part of refinement machinery
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: support assign-such-that in var declarations in refinements
Unknown
2012-03-15
*
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: make sure assume->assert transformation gives rise to a check
Rustan Leino
2012-02-19
*
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: improved error location for violations of function postconditions
Rustan Leino
2012-01-18
*
Dafny: allow a refinement to provide a function/method body if the function/m...
Rustan Leino
2012-01-18
*
Dafny: added signature checking to refinement
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: 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: added predicates
Rustan Leino
2012-01-10
*
Dafny: added support for simple superposition refinements
Rustan Leino
2012-01-09
*
Dafny: changed translation to be sensitive to refinement inheritance; this fe...
Rustan Leino
2012-01-09
*
Dafny: disallow changes of datatypes in refinements
Rustan Leino
2012-01-09
*
Dafny: finished refinement cloning transformations
Rustan Leino
2012-01-07
*
Dafny: filled in more cloning for the refinement transformations
Rustan Leino
2012-01-06
*
Dafny: fully qualify (with module names) names of types in the translation in...
Rustan Leino
2012-01-05
*
Dafny: beginning of the new refinement transformations
Rustan Leino
2012-01-05