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