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

Hi,

Commenting on your post:

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


This is what the ACSL document says in 2.2.3 Typing of logic expressions.
I don't know if it will be implemented in the near future though. Maybe
Benjamin can answer this?

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

If many users find the use of && and || awkward, then AND and OR could be
proposed as an alternate syntax (if we're willing to support two syntax...)
or even a complete replacement before more users get used to the old ones.
For those who don't like the look of these capitalized keywords, there is
always the possibility of using the utf8 symbols ...

-- 
Yannick
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20080805/b4f3b05d/attachment.html