Merge branch 'blog-mini-acsl' into 'master'

[blog] post about quick ACSL guide for Eva

See merge request !144

_posts/2022-04-06-eva-acsl-quick-guide.md

+---
+layout: post
+author: André Maroneze (review by V. Prevosto, P. Baudin)
+date: 2022-04-06 18:00 +0100
+categories: acsl
+title: "Quick ACSL Guide for Eva: a new mini-tutorial"
+---
+
+In 2016, a few blog posts
+([part 1](2016/09/23/A-mini-tutorial-of-ACSL-specifications-for-Value.html),
+[part 2](2016/09/30/A-mini-ACSL-tutorial-for-Value-part-2-functional-dependencies.html),
+[part 3](2016/10/12/A-mini-ACSL-tutorial-for-Value-part-3-indirect-assigns.html))
+presented a short tutorial on writing ACSL clauses for Eva (back then,
+the *Value Analysis* plug-in). A few things changed since then,
+but posting them again in this blog would lead to the same issue in the future.
+Instead, we added an annex to the
+[Eva user manual](https://www.frama-c.com/download/frama-c-eva-manual.pdf).
+This annex, titled *ACSL Quick Guide for Eva*, is targeted towards a slightly
+different audience, including complete ACSL beginners. In this blog post,
+we present the annex, its motivation, and summarize its most interesting
+contents.
+
+## Yet Another ACSL Tutorial?
+
+[ACSL, the ANSI/ISO C Language](https://frama-c.com/html/acsl.html), the
+*lingua franca* of Frama-C, is important for most, if not all, Frama-C users.
+Fortunately, most users will _never_ (or rarely) need to read the
+[ACSL reference manual](https://frama-c.com/download/acsl.pdf), just like most
+Java programmers will never have to read the
+[Java Language Specification](https://docs.oracle.com/javase/specs/jls/se18/html/index.html),
+and most C programmers... well, most C programmers _should_ read the C standard,
+just to realize how deep the madness goes.
+But I digress.
+
+ACSL has currently at least 2 excellent guides:
+[Blanchard's WP tutorial](https://allan-blanchard.fr/frama-c-wp-tutorial.html),
+available in English *and* French, and
+[ACSL by Example](https://github.com/fraunhoferfokus/acsl-by-example), by
+Gerlach et al., from Fraunhofer FOKUS. However, their target audience are
+mainly [WP](https://frama-c.com/fc-plugins/wp.html) users, who fell into the
+loop invariant cauldron when they were a baby.
+These guides *must* be as thorough as possible,
+since their users will need to not only _read_ but also _write_ lots of ACSL
+(except if they are using [MetAcsl](https://www.frama-c.com/fc-plugins/metacsl.html),
+of course).
+For the fledging Eva user, who wants mostly to pretend that ACSL does not exist
+and just keep on verifying their code as automatically as they can
+(with Frama-C as inconspicuous as possible), such guides are more than they
+need.
+
+This is one of the motivations of the original blog post series mentioned
+in the beginning of this post. However, industrial users over the years have
+shown us that those posts *still* require some knowledge of ACSL (it is
+written in the first post: *Prerequisites: ... Basic knowledge of ACSL*). But
+then, where do they get such *basic knowledge*? From reading the ACSL
+language specification (oh, the horror!)? From reading one of the WP guides?
+But then, where do they start, and where do they stop? Should users just
+learn by themselves by reading Frama-C's standard library specifications
+(*no: this is neither the easiest nor the safest way to do so*)?
+None of these solutions is satisfying. Hence the need for a new,
+zero-ACSL-required tutorial.
+
+## ACSL ∩ Eva in 10 pages
+
+Writing a quick ACSL guide for Eva allows us to simplify the presentation
+and avoid content that is irrelevant for Eva, either because currently
+unsupported (such as some higher-level logic features), or because it never
+appears in the specifications used by Eva. We also designed a few sections
+as optional material, with predicates which are _sometimes_ seen in libc
+specifications (and thus potentially relevant for Eva), but not essential
+for first-time users. We also included sections on behaviors (not for the
+faint-hearted, but essential for precision and thus present in several libc
+specifications), dynamic memory allocation, and some unintuitive features
+that might confuse users. Finally, in the end, we added a
+*FAQ/Troubleshooting/Common errors* section, whose purpose is to, ideally,
+allow users to <kbd>Ctrl+V</kbd> unexpected error messages and hopefully
+get a direct explanation about them. This section can definitely benefit
+from user feedback; if you find an error message that seems too cryptic
+or that took you longer than necessary to understand, please consider
+[filing an issue](https://git.frama-c.com/pub/frama-c/-/issues/new)
+with the code and the message, and we'll consider incorporating it in the
+guide. If you are really motivated, you can even create a merge request
+in our Gitlab! The Eva user manual is part of the source code of Frama-C,
+in directory `doc/value`, so everyone can contribute (at least everyone who
+can write in LaTeX, but here I digress again). That is also one
+of the benefits of putting the guide in the user manual instead of a
+blog post.
+
+## A few tricks up Eva's sleeve
+
+This quick guide is not *only* for new Frama-C/Eva users. It also describes
+a few ACSL details specific to Eva, which explain some specification choices
+and may help users understand why some cases are not handled by Eva as one would
+expect. The main one is the `indirect:` label in some `\from` clauses, which
+is currently _only_ used by Eva (but very helpful in avoiding the production of
+*garbled mix*). The difference between disjunctions with holes and
+interval-like disjunctions (e.g. `a != 0` creates a single interval with 0 as a
+"hole", while `a < 0 || a > 0` creates two intervals without holes) is also
+specific to Eva, and earns a mention in the guide.
+
+## Conclusion
+
+We expect this guide to be especially useful for new Frama-C/Eva users, who
+have never seen ACSL before and would like to start using Eva as quickly as
+possible, without having to invest too much time into learning. Of course,
+code relying heavily on C standard library files, or requiring stubs for
+complex reasoning, will always require some effort; but lowering that effort
+is one of the objectives of Frama-C: showing that formal methods can be
+efficiently applied at industrial scale, to cope with this ineffable
+language that is C.