Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] The && operator in logical annotations

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