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] Information hiding: how to handle module's private static variables in Frama-C?

  • Subject: [Frama-c-discuss] Information hiding: how to handle module's private static variables in Frama-C?
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Wed, 27 Nov 2013 16:31:00 +0100
  • In-reply-to: <CAOH62Jg5uajSHmWa-ntPLMD9M9S4EtuFzjQ6nCqjy_=dpjoL5A@mail.gmail.com>
  • References: <CAC3Lx=bqpi2v3cwLZ1bKeWPm262vt+44Ocw1DvQoh1OkGSLQhA@mail.gmail.com> <CAOH62Jg5uajSHmWa-ntPLMD9M9S4EtuFzjQ6nCqjy_=dpjoL5A@mail.gmail.com>
Hello Pascal,

2013/11/27 Pascal Cuoq <pascal.cuoq at gmail.com>:
> I have been discussing this very question with Claude March?, who pointed me
> to Asma Tafat's PhD thesis:
> https://www.lri.fr/~atafat/These/manusrit_tafat.pdf [French].
> Key quote: ?La sp?cification d?un programme a besoin d??tre abstraite pour
> plusieurs raisons. La premi?re est que les sp?cifications d?crivent le
> comportement fonctionnel des programmes, c?est-?-dire ce que fait le
> programme et non pas comment il le fait.?

As an occasional user of B Method, I strongly agree with this quote
(~= "specs should be abstract, firstly because specs describe
functional behaviour of a program, i.e. the what and not the how").

Thanks for the pointer. I unfortunately haven't enough time to real
the whole thesis but from a quick read, Asma Tafat's work implements a
mechanism similar to B refinement, but with probably more automatic
generation of gluing invariant through hidden program typing and
language restrictions.

>From my own experience, B Method is very powerful but also very
manual. One can endanger the correctness of a program through
incorrect or missing gluing invariant. And some manual proofs are
needed. An approach keeping the refinement ideas but automating it for
both annotations and proofs would be very useful.

> I think that Frama-C and ACSL should natively incorporate some of these
> ideas, but as of yet, they do not.

Yes. B Method and SPARK 2014 probably have an advantage in this
regard. For example, SPARK 2014 has a mechanism to abstract some
internal module variables into abstract ones (see
http://www.spark-2014.org/entries/detail/spark-2014-rationale-global-state).
But I haven't played with this mechanism so I don't know how useful it
is in practice.

In the same spirit, Bertrand Meyer advocating Domain Theory, i.e. a
library of operators specialized to a domain in order to easily
express function contracts is very interesting
(http://bertrandmeyer.com/2012/04/11/domain-theory-the-forgotten-step-in-program-verification/).
Frama-C's ghost variables could be linked to this view. SPARK 2014's
specification functions
(http://www.spark-2014.org/entries/detail/spark-2014-rationale-specification-functions)
can also be linked to it. From my user point of view, ability to
express natural contracts, i.e. contracts that are abstract in some
way and use the same vocabulary as the user, could greatly help to use
formal methods. Prover iLock product using notation close to railway
signalling engineers notation seems to be a successful product for
that reason (see screenshot 2 in
http://www.prover.com/products/prover_ilock/verifier_module/).

> Claude and I arrived to the conclusion
> that it was possible in the meantime to play with the presented ideas by
> cheating (i.e. presenting to the users of the function to abstract a
> different (more abstract) specification than was used to verify it), but I
> forget the details now.

I had a similar intent in my example. In the first version of this
program, functions f() and incr_a() of q18_a.c where merged (contract
& code). For clarity and provability, I then separated the code into
code specific to an internal API (incr_a()) and code specific to an
external API (f()).

On Why3 mailing list, Lo?c Correnson proposed an approach to implement
refinements in WhyML
(http://lists.gforge.inria.fr/pipermail/why3-club/2013-February/000545.html).
Maybe such approach could be applied in Frama-C?

In any case, if you or Claude have suggestions on ways to improve
modularity of Frama-C programs, I would be very interested in them.

Best regards,
david