summaryrefslogtreecommitdiff
path: root/Test/dafny2/StoreAndRetrieve.dfy
Commit message (Expand)AuthorAge
* This changeset changes the default visibility of a function/predicate body ou...Gravatar leino2015-03-09
* Stop pretty-print from emitting deprecated semi-colons.Gravatar qunyanm2015-03-05
* Disallow parentheses-less declarations of predicates and co-predicates, along...Gravatar leino2014-08-27
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, ...Gravatar Rustan Leino2013-04-01
* renamed "abstract module" to "module facade"Gravatar Rustan Leino2012-10-22
* improved and fixed compilation and resolution of assign-such-that statementsGravatar Rustan Leino2012-10-05
* Dafny: updated test suite to new syntaxGravatar Jason Koenig2012-07-30
* Dafny: restored soundness for refinement by disallowing certain updates and m...Gravatar Jason Koenig2012-07-11
* Dafny: reinstated autocontractsGravatar Jason Koenig2012-07-02
* Dafny: fixed a couple of compiler bugsGravatar Unknown2012-06-14
* Dafny: support assign-such-that in var declarations in refinementsGravatar Unknown2012-03-15
* Dafny: added StoreAndRetrieve refinement exampleGravatar Unknown2012-03-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 12:57:53 +0000