# 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] ACSL by Example (for Nitrogen)

*Subject*: [Frama-c-discuss] ACSL by Example (for Nitrogen)*From*: moy at adacore.com (Yannick Moy)*Date*: Mon, 16 Jan 2012 10:18:37 +0100*In-reply-to*: <2A880318-7B19-4614-BF73-EBA80EC13F87@first.fraunhofer.de>*References*: <2A880318-7B19-4614-BF73-EBA80EC13F87@first.fraunhofer.de>

On 12/16/2011 04:52 PM, Jens Gerlach wrote: > Dear Frama-C Users, > > the Verification Group at Fraunhofer FIRST (http://www.first.fraunhofer.de/en/home/) > is pleased to announce a new release of "ACSL by Example". > > The examples have been updated for the Nitrogen release of Frama-C. > The majority of examples can now be verified by WP and Jessie (2.30). > Examples that could not be proven by WP and Jessie are marked by a '*' and '+', respectively. > > You can download the document directly from > http://www.first.fraunhofer.de/fileadmin/FIRST/ACSL-by-Example.pdf > (The link is the same as to the previous release.) > > We hope this document is useful for your work with ACSL. > If you have suggestion or comments, please write to devicesoft at first.fraunhofer.de<mailto:devicesoft at first.fraunhofer.de> . > > Best regards > > Jens Gerlach Hi Jens and happy new year! One of my new year's resolution was to read cover-to-cover your ACSL by Example doc, so here are a few remarks in case you find them useful. The first thing is that your introductory section "Structure of this document" does not do justice to the work done in chapters 7 and 8. While the previous chapters correspond to what you announce (implementation and verification of C simple algorithms), chapters 7 and 8 tackle some much more difficult examples, and this should be announced from the start. I was quite impressed that you could prove this automatically! This would be the place to warn the user that complex data structures require complex annotations and verification, in particular for automatic provers which must be guided through the proof. (and you've got plenty of examples of that, e.g. ghost functions) It would be interesting to get some feedback (or horror stories! :)) on your experience here, when developing the code/proofs for chapters 7 and 8. You never mention which automatic provers you are using. You should do it and give some information on what properties each prover is better at proving. (I guess the lemma Ampersand_0 is only proved by Z3 for example.) It would be useful for potential industrial users to say a few words on the licensing conditions for these external provers. (In case you don't know it yet, Z3 is now available at around 15,000$ for industrial use.) In the foreword, you mention Frama-C Boron, but you say in your email (and in the doc) that you use version Nitrogen. On p 24, you say "When used in an assumes clause the label Here refers to the pre-state of a function" but your example uses label Here in an ensures clause. After listing 3.3, you could explain that an equivalence is needed in the ensures clause. Putting an equality instead is not legal in ACSL, because IsEqual is a predicate. In listing 3.4, I would put braces around the loop body for clarity, even if not around the if. The explanation that follows mentions Line 9 for the array access on Line 10, and Line 6 for the variant on Line 7, and Line 8-10 for loop body on lines 9-11. Same discrepancy between reported lines and effective ones in the explanation of find_first_of on p 33. The legend for figure 3.25 is "Explanation for Line 12" but should be for line 13. The example for reverse_copy is missing a \separated precondition. For axiom whithe_lemma, ou say "However, as a lemma it can be proven only by induction and this is impossiple (impossible) when using automatic theorem provers that work with Frama-C." This is not true, as you could any of the manual provers targeted by Why3 to prove this lemma. Maybe you could say that, for simplicity, you did not prove it manually. The example for remove_copy is missing a \separated precondition. The precondition of iota is unnecessarily restrictive, it should be: (val + n-1 <= INT_MAX) (and "Lines 2", "Lines 3" should be singular) I think you should explain the role of the ghost function pop_push_heap_copy, which only serves to introduce a lemma in the context, and the use of all the intermediate assertions in the body of pop_push_heap_copy (I guess to help automatic provers?) Its use in push_heap is not explained either. You say "It is interesting, that neither in the specification nor in the implementation of is_heap the predicates Even and Odd are explicitly used." You should also say that the link between the axiomatization for Odd/Even and the code is the use of the "x&1" expression. In the loop invariant on line 14 of push_heap, it seems the invariant could be \forall integer i; i < n and ParentChild(hol,i) ==> a[i] < tmp (that is, a strict inequality instead of a non-strict one) For pop_heap, you mention removing manually the "Why axiom in32_extensionality" without explaining the rationale for that. The end of the explanations for this function does not correspond to the actual code (line 25, 34, 39, 44, 50, etc do not correspond). As the more complex function shown so far, pop_heap deserves a larger description I think, both for the actual algorithm implemented (pushing down the max value to position n-1 by finding an appropriate place for a[n-1]) and the "magic" done with intermediate assertions and loop invariants to force automatic provers in finding the proof. It seems that the algorithm computes a maximum value of 2*n (for hole=n-1 in the loop) so that a precondition (2*n <= INT_MAX) would be sufficient. You could also write the tests to check for a possible overflow before computing 2*n+2 and 2*n+1, so that you would not need a precondition. Why define as postcondition for size_stack that IsValidStack(s)? (already in precondition). Same thing for empty_stack, full_stack, top_stack. Page 142, I don't understand your systematic generation of code from axioms, in particular: * Generate a clause requires x1 == ... == xn for each variable x with n occurrences in s and t. * Change the i-th occurrence of x to xi in s and t. * Translate both terms s and t to reversed polish notation. -- Yannick

**Follow-Ups**:**[Frama-c-discuss] ACSL by Example (for Nitrogen)***From:*jens.gerlach at first.fraunhofer.de (Jens Gerlach)

**[Frama-c-discuss] ACSL by Example (for Nitrogen)***From:*pascal.cuoq at gmail.com (Pascal Cuoq)

- Prev by Date:
**[Frama-c-discuss] Visitor example in plugin-development guide** - Next by Date:
**[Frama-c-discuss] ACSL by Example (for Nitrogen)** - Previous by thread:
**[Frama-c-discuss] New release of WP plug-in** - Next by thread:
**[Frama-c-discuss] ACSL by Example (for Nitrogen)** - Index(es):