assume and assert

The previous post links to a message [removed dead link] 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. The 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.

The 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 assume this way reserves the keyword assumes for 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 assume.

Keyword minimalism

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 assume and 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 \valid(p).

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 assume to 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.