--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on August 2008 ---
On Mon, 2008-08-04 at 18:43 +0200, Yannick Moy wrote: > Concerning the problem of different semantics and priority for && in > code and annotations, Jonathan Shapiro answered on the Why list: > > > This is a sufficiently bad intrusion into C expressions that > the logical > annotation language would do well to change keywords. > Let me expand on this briefly. The current ACSL syntax sometimes requires rewrites of meta-statements in ways that significantly reduce their visual clarity. In my opinion, being able to understand and maintain those statements is very important, not least because undiagnosed but mis-stated verification conditions have been responsible for so many proof errors over the years. This is a quoting problem. The annotation language is a meta-language including language expressions as a sub-grammar. There are two possible choices for a clean design: 1. Construct the metalanguage grammar in such a way that the language expression sub-grammar can be included without ambiguities of this kind (and therefore does not require quoting), or 2. Introduce a quoting or bracketing syntax that resolves the ambiguity of the grammar. I personally prefer solution [1], because it is visually cleaner, but either design is a valid choice. There is also a middle position: 3. Have a bracketing syntax, but design the meta-language grammar so that it is rarely required in practice. I believe that this is the best approach for ACSL. The challenge in this case will be that the syntax of C expressions makes choosing a non-colliding keyword very difficult -- perhaps impossible -- and most of the alternatives (e.g. &&&) are ugly. Since a fully clean syntax seems difficult, here is a concrete proposal to consider: 1. Incorporate an expression bracketing syntax into ACSL. It should exist in order to forcibly resolve ambiguities in rare cases. In this case, it seems possible that the answer is simply to wrap the ambiguous C expression in parentheses. That is a nice solution, because it requires no new syntax. I have not thought carefully about whether this actually works. 2. Choose keywords in ACL that are very unlikely to collide, so that expression bracketing is rarely needed. One possibility would be to use ascii names in uppercase: AND OR these have the advantage that they *look* like syntax, and they are unlikely to be used in real C programs for reasons of historical style. When they are, the need for bracketing of expressions will be visually obvious. I think that my particular choice of syntax would work in practice, but syntax is a religious matter. The criteria that I am suggesting seem important. The particular proposal does not. shap