summaryrefslogtreecommitdiff
path: root/Source/Dafny/RefinementTransformer.cs
Commit message (Expand)AuthorAge
* Dafny: added signature checking to refinementGravatar Rustan Leino2012-01-17
* Dafny: Recheck specifications that contain refined (extended) predicates, eve...Gravatar Rustan Leino2012-01-16
* Dafny: handle refinement of nested tokens that come from SpliExpr (still need...Gravatar Rustan Leino2012-01-12
* Dafny: some bug fixesGravatar Rustan Leino2012-01-10
* Dafny: allow definitions and uses of parameter-less predicates to go without ...Gravatar Rustan Leino2012-01-10
* Dafny: added predicatesGravatar Rustan Leino2012-01-10
* Dafny: added support for simple superposition refinementsGravatar Rustan Leino2012-01-09
* Dafny: changed translation to be sensitive to refinement inheritance; this fe...Gravatar Rustan Leino2012-01-09
* Dafny: disallow changes of datatypes in refinementsGravatar Rustan Leino2012-01-09
* Dafny: finished refinement cloning transformationsGravatar Rustan Leino2012-01-07
* Dafny: filled in more cloning for the refinement transformationsGravatar Rustan Leino2012-01-06
* Dafny: fully qualify (with module names) names of types in the translation in...Gravatar Rustan Leino2012-01-05
* Dafny: beginning of the new refinement transformationsGravatar Rustan Leino2012-01-05
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-07 13:04:25 +0000