--- layout: fc_discuss_archives title: Message 124 from Frama-C-discuss on November 2013 ---
[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?



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.?

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

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131127/f71f630f/attachment.html>