summaryrefslogtreecommitdiff
path: root/Test/dafny0/FunctionSpecifications.dfy
Commit message (Expand)AuthorAge
* Make reveal axioms from opaque functions quantify over layersGravatar Dan Rosén2014-07-10
* New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Added support for opaque function definitions, indicated via the {:opaque} at...Gravatar Bryan Parno2013-12-13
* Fixed let-such-that and if-then-else encodings so that they will pass the sub...Gravatar Rustan Leino2013-02-21
* Dafny: fixed bug in checking postconditions of functions that mention the res...Gravatar Unknown2012-08-29
* Dafny: permanently changed the syntax of "datatype" declarations to what prev...Gravatar Rustan Leino2011-05-27
* Dafny: allow self-calls in function postconditions--these simply refer to the...Gravatar rustanleino2011-02-03