Closed DavePearce closed 2 years ago
It seems pretty straightforward to me that we need requires clauses on property declarations. We cannot have ensures clauses though. I'm also not sure exactly how they would translate into Boogie either.
requires
property
ensures
It seems pretty straightforward to me that we need
requiresclauses onpropertydeclarations. We cannot haveensuresclauses though. I'm also not sure exactly how they would translate into Boogie either.