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