assume and assert
By pascal on Friday, August 3 2012, 09:35 - Permalink
The previous post links to a message from Michał Moskal highlighting ACSL constructs that the VCC developers at Microsoft Research had either regretted the absence of or found superfluous while re-designing their own annotation language for VCC. In that e-mail, the third item in the “missing” list was:
ACSL is surprisingly missing /*@ assume ... */, we've found it tremendously useful when debugging specifications.
The feedback VCC developers sent us caused us to review our design choices and nudge ACSL a bit. Not having an
assume annotation, however, was a conscious decision that remained. I am going to give an explanation that makes it look as if the exclusion is part of a larger, well though-out plan. I did not think of this explanation at the time, and it only came to me recently while talking about something else.
I am not sure what this says about the plan. At some level the plan was there all along, but for some reason we failed to explain it well, perhaps especially in these circumstances when it would have been useful.
The assume annotation in VCC
Design-by-contract is also sometimes called “assume-guarantee reasoning” (if you know the precise difference between these two, please leave a comment. The only reason I see for separate denominations is that “Design by Contract” seems to be a registered trademark of Eiffel Software in the United States).
This is not the “assume” we are looking for. In ACSL, and now in VCC, the expectations of a function are introduced with the
requires keyword. The keyword
assume could have been used for that, but this is not the choice that was made, and Michał's e-mail is definitely not saying that ACSL is missing a keyword to introduce the precondition of a function.
Instead, in VCC,
assume is the dual of
assert annotation is attached to a specific point in a program and introduces a property that is supposed to hold (that the verifier should endeavor to verify) there:
stuff; /*@ assert property ; */ // the verifier tries to prove that "stuff" makes "property" hold.
assume keyword tells the verifier to take it as granted that a property holds somewhere, and to use that for reasoning about the rest of the program:
/*@ assume property ; */ // "property" is useful to understand what "stuff" does. stuff;
Beware that ACSL, since it does not use
assumethis way, reserves the keyword
assumesfor something else entirely. When the rest of this post says that ACSL does not have
assume, it means that ACSL does not have a VCC-like
It is a worthy goal to minimize the number of keywords forced on you by a BISL—Behavioral Interface Specification Language (the acronym is catching on already). One could argue that both the functionality of
assert above can be captured with a single keyword. The verifier, when encountering that keyword, should first try to establish the property as a consequence of the code above. Then, regardless of whether it was able to establish it, it should incorporate it in its hypotheses for the study of the code below it.
This is exactly how Frama-C approaches the issue. Plug-ins that understand ACSL at all both try to prove such properties and then use them as assumptions. The properties are introduced with the
assert keyword which, in ACSL,
conveys both meanings. This may mean that a bit of redundant work is made, but the resulting annotation language is so beautiful, like a smartphone with only two hardware buttons, that the sacrifice is worth it.
Well, this explanation is not actually quite right. Please read on.
Plug-in collaboration and property status management
There is a deeper explanation than just “each plug-in can do the work both ways and that will save a keyword”. This other explanation is specific to what Frama-C is. Or rather what Frama-C intends to be, for it is a long-term effort.
Frama-C is—or intends to be—a collaborative verification framework. Frama-C makes it convenient to seamlessly subject one same annotated program to different and complementary analysis techniques. In particular, it was always the intention that whichever property was assumed by a plug-in could be proved by another. For the Frama-C platform to be usable this way, it is necessary, but not sufficient, to have a single annotation language with a formal semantics that all plug-ins agree on, to express properties like
It is also necessary to use a single keyword for assumptions and goals, because without that, the user would need to go to the source code and change
assert or vice-versa when switching from a plug-in to another. In Frama-C, a plug-in's assumption is another plug-in's goal.
The Frama-C kernel tracks each program property and its verification status. A property that was only ever assumed, never proved, is an assumption of the whole verification. A property that was assumed by a plug-in and proved by another is just like an intermediate lemma in a mathematical proof.
The devil is in the details, of course, and the details are in the article “Combining Analyses for C Program Verification” (FMICS2012) by my colleagues Loïc Correnson and Julien Signoles.
Trying to prove a goal can still be expensive and unnecessary. There will eventually be a way to mark a property as “assumed” in the Frama-C kernel for efficiency reasons. We are still thinking about the best way to do that.
Thanks to Julien Signoles, Florent Kirchner, Virgile Prevosto, Sébastien Bardin and Michał Moskal for their remarks on earlier iterations of this blog post.