[blog] post about quick ACSL guide for Eva
9 unresolved threads
9 unresolved threads
Merge request reports
Activity
Filter activity
added blog label
assigned to @maroneze
- _posts/2022-04-xx-eva-acsl-quick-guide.md 0 → 100644
17 [Eva user manual](https://www.frama-c.com/download/frama-c-eva-manual.pdf). 18 This annex, titled *ACSL Quick Guide for Eva*, is targeted towards a slightly 19 different audience, including complete ACSL beginners. In this blog post, 20 we present the annex, its motivation, and summarize its most interesting 21 contents. 22 23 ## Yet Another ACSL Tutorial? 24 25 [ACSL, the ANSI/ISO C Language](https://frama-c.com/html/acsl.html), the 26 *lingua franca* of Frama-C, is important for most, if not all, Frama-C users. 27 Fortunately, most users will _never_ (or rarely) need to read the 28 [ACSL reference manual](https://frama-c.com/download/acsl.pdf), just like most 29 Java programmers will never have to read the 30 [Java Language Specification](https://docs.oracle.com/javase/specs/jls/se18/html/index.html), 31 and most C programmers... well, most C programmers _should_ have 32 to read the C standard, just to realize how deep the madness goes<sup>1</sup>. - Comment on lines +31 to +32
31 and most C programmers... well, most C programmers _should_ have 32 to read the C standard, just to realize how deep the madness goes<sup>1</sup>. 31 and most C programmers... well, most C programmers _should_ 32 read the C standard, just to realize how deep the madness goes<sup>1</sup>. changed this line in version 2 of the diff
- _posts/2022-04-xx-eva-acsl-quick-guide.md 0 → 100644
22 23 ## Yet Another ACSL Tutorial? 24 25 [ACSL, the ANSI/ISO C Language](https://frama-c.com/html/acsl.html), the 26 *lingua franca* of Frama-C, is important for most, if not all, Frama-C users. 27 Fortunately, most users will _never_ (or rarely) need to read the 28 [ACSL reference manual](https://frama-c.com/download/acsl.pdf), just like most 29 Java programmers will never have to read the 30 [Java Language Specification](https://docs.oracle.com/javase/specs/jls/se18/html/index.html), 31 and most C programmers... well, most C programmers _should_ have 32 to read the C standard, just to realize how deep the madness goes<sup>1</sup>. 33 But I digress. 34 35 <sup>1</sup> At least for critical applications, a test on C semantics 36 should be a prerequisite for those deciding its application; that would 37 motivate them to consider implementing the application in a better changed this line in version 2 of the diff
- _posts/2022-04-xx-eva-acsl-quick-guide.md 0 → 100644
30 [Java Language Specification](https://docs.oracle.com/javase/specs/jls/se18/html/index.html), 31 and most C programmers... well, most C programmers _should_ have 32 to read the C standard, just to realize how deep the madness goes<sup>1</sup>. 33 But I digress. 34 35 <sup>1</sup> At least for critical applications, a test on C semantics 36 should be a prerequisite for those deciding its application; that would 37 motivate them to consider implementing the application in a better 38 (and safer) language. 39 40 ACSL has currently at least 2 excellent guides: 41 [Blanchard's WP tutorial](https://allan-blanchard.fr/frama-c-wp-tutorial.html), 42 available in English *and* French, and 43 [ACSL by Example](https://github.com/fraunhoferfokus/acsl-by-example), by 44 Gerlach et al., from Fraunhofer FOKUS. However, their target audience are 45 mainly [WP](https://frama-c.com/fc-plugins/wp.html) users, who eat (froot) loop changed this line in version 2 of the diff
- _posts/2022-04-xx-eva-acsl-quick-guide.md 0 → 100644
31 and most C programmers... well, most C programmers _should_ have 32 to read the C standard, just to realize how deep the madness goes<sup>1</sup>. 33 But I digress. 34 35 <sup>1</sup> At least for critical applications, a test on C semantics 36 should be a prerequisite for those deciding its application; that would 37 motivate them to consider implementing the application in a better 38 (and safer) language. 39 40 ACSL has currently at least 2 excellent guides: 41 [Blanchard's WP tutorial](https://allan-blanchard.fr/frama-c-wp-tutorial.html), 42 available in English *and* French, and 43 [ACSL by Example](https://github.com/fraunhoferfokus/acsl-by-example), by 44 Gerlach et al., from Fraunhofer FOKUS. However, their target audience are 45 mainly [WP](https://frama-c.com/fc-plugins/wp.html) users, who eat (froot) loop 46 invariants for breakfast. These guides *must* be as thorough as possible, changed this line in version 2 of the diff
- _posts/2022-04-xx-eva-acsl-quick-guide.md 0 → 100644
32 to read the C standard, just to realize how deep the madness goes<sup>1</sup>. 33 But I digress. 34 35 <sup>1</sup> At least for critical applications, a test on C semantics 36 should be a prerequisite for those deciding its application; that would 37 motivate them to consider implementing the application in a better 38 (and safer) language. 39 40 ACSL has currently at least 2 excellent guides: 41 [Blanchard's WP tutorial](https://allan-blanchard.fr/frama-c-wp-tutorial.html), 42 available in English *and* French, and 43 [ACSL by Example](https://github.com/fraunhoferfokus/acsl-by-example), by 44 Gerlach et al., from Fraunhofer FOKUS. However, their target audience are 45 mainly [WP](https://frama-c.com/fc-plugins/wp.html) users, who eat (froot) loop 46 invariants for breakfast. These guides *must* be as thorough as possible, 47 since their users will need to not only _read_ but also _write_ lots of ACSL. changed this line in version 2 of the diff
- _posts/2022-04-xx-eva-acsl-quick-guide.md 0 → 100644
62 zero-ACSL-required tutorial. 63 64 ## ACSL ∩ Eva in 10 pages 65 66 Writing a quick ACSL guide for Eva allows us to simplify the presentation 67 and avoid content that is irrelevant for Eva, either because currently 68 unsupported (such as some higher-level logic features), or because it never 69 appears in the specifications used by Eva. We also designed a few sections 70 as optional material, with predicates which are _sometimes_ seen in libc 71 specifications (and thus potentially relevant for Eva), but not essential 72 for first-time users. We also included sections on behaviors (not for the 73 faint-hearted, but essential for precision and thus present in several libc 74 specifications), dynamic memory allocation, and some unintuitive features 75 that might confuse users. Finally, in the end, we added a 76 *FAQ/Troubleshooting/Common errors* section, whose purpose is to, ideally, 77 allow users to Ctrl+V unexpected error messages and hopefully get a direct <kbd>Ctrl+V</kbd>(Ctrl+V si ça marche).Edited by Virgile Prevostochanged this line in version 2 of the diff
- _posts/2022-04-xx-eva-acsl-quick-guide.md 0 → 100644
70 as optional material, with predicates which are _sometimes_ seen in libc 71 specifications (and thus potentially relevant for Eva), but not essential 72 for first-time users. We also included sections on behaviors (not for the 73 faint-hearted, but essential for precision and thus present in several libc 74 specifications), dynamic memory allocation, and some unintuitive features 75 that might confuse users. Finally, in the end, we added a 76 *FAQ/Troubleshooting/Common errors* section, whose purpose is to, ideally, 77 allow users to Ctrl+V unexpected error messages and hopefully get a direct 78 explanation about them. This section can definitely benefit from user 79 feedback; if you find an error message that seems too cryptic or that took 80 you longer than necessary to understand, please consider 81 [filing an issue](https://git.frama-c.com/pub/frama-c/-/issues/new) 82 with the code and the message, and we'll consider incorporating it in the 83 guide. If you are really motivated, you can even create a merge request 84 in our Gitlab! The Eva user manual is part of the source code of Frama-C, 85 in directory `doc/value`, so everyone can contribute. That is also one changed this line in version 2 of the diff
- _posts/2022-04-xx-eva-acsl-quick-guide.md 0 → 100644
82 with the code and the message, and we'll consider incorporating it in the 83 guide. If you are really motivated, you can even create a merge request 84 in our Gitlab! The Eva user manual is part of the source code of Frama-C, 85 in directory `doc/value`, so everyone can contribute. That is also one 86 of the benefits of integrating the guide into the user manual, and not in a 87 blog post. 88 89 ## Conclusion 90 91 We expect this guide to be especially useful for new Frama-C/Eva users, who 92 have never seen ACSL before and would like to start using Eva as quickly as 93 possible, without having to invest too much time into learning. Of course, 94 code relying heavily on C standard library files, or requiring stubs for 95 complex reasoning, will always require some effort; but lowering that effort 96 is one of the objectives of Frama-C: showing that formal methods can be 97 efficiently applied at industrial scale, to help cope with this *aweful* changed this line in version 2 of the diff
_posts/2022-04-xx-eva-acsl-quick-guide.md 0 → 10064449 and just keep on verifying their code as automatically as they can 50 (with Frama-C as inconspicuous as possible), such guides are more than they 51 need. 52 53 This is one of the motivations of the original blog post series mentioned 54 in the beginning of this post. However, industrial users over the years have 55 shown us that those posts *still* require some knowledge of ACSL (it is 56 written in the first post: *Prerequisites: ... Basic knowledge of ACSL*). But 57 then, where do they get such *basic knowledge*? From reading the ACSL 58 language specification (oh, the horror!)? From reading one of these WP guides? 59 But then, where do they start, and where do they stop? Should users just 60 learn by themselves by reading Frama-C's standard library specifications? 61 None of these solutions is satisfying. Hence the need for a new, 62 zero-ACSL-required tutorial. 63 64 ## ACSL ∩ Eva in 10 pages changed this line in version 3 of the diff
mentioned in commit 943c0cf4
Please register or sign in to reply