[ACSL] VCC & ACSL

Michal Moskal Michal.Moskal at microsoft.com
Mon Feb 22 23:23:53 CET 2010


Dear colleagues

Over the last couple weeks we've been discussing ACSL and the changes to annotation syntax in VCC to get a better alignment. We went through the ACSL specification and made some decisions on what to include and what not. These decisions are not yet final, but are currently being implemented. They are summarized in the attached document, and the accompanying grammar.

We would like to propose some of them to be considered for future version of ACSL, in particular:

1.            The (optional?) use of _(...) (or something similar) for specifications, as opposed to /*@ ... */. This makes supporting macro expansion in the compiler way easier, and makes the specs look much more like first-class citizens.
2.            If 1. is adopted, the possibly one should consider placing function contracts after the prototype, and before the body. This makes it natural to reference parameters, declared in the prototype, in the body.
3.            ACSL is surprisingly missing /*@ assume ... */, we've found it tremendously useful when debugging specifications.
4.            We think that supporting a<b<c in the specification language might lead to people trying to use it in implementation code, with completely different results. We decided not to do that.
5.            Shouldn't the ACSL predefined types be called \integer, \real and \set<...> ? (not to clash with possible C types).

We also had some questions:

1.            We were wondering about the rationale behind the use of keyword "for" in { s for .x = 7 }, what about \with ?
2.            Similarly, we couldn't figure out usage scenarios for --> and <-->.
3.            What are the usage scenarios of \initialized and \specified?

VCC has completely different approach to ghost code than ACSL does - in VCC one does everything with regular C code, extended here and there. Similarly VCC doesn't use footprints but ownership instead. I guess this amounts for most of the remaining differences.

Any comments, suggestions, refinements, clarifications, etc are welcome.

Best,-
The VCC team: Michal, Ernie Stephan, Wolfram
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-acsl-discuss/attachments/20100222/e8d4614c/attachment-0002.htm>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-acsl-discuss/attachments/20100222/e8d4614c/attachment-0003.htm>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: grammar.txt
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-acsl-discuss/attachments/20100222/e8d4614c/attachment-0001.txt>


More information about the Frama-c-acsl-discuss mailing list