--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on October 2014 ---
Le 26/09/2014 18:02, Marko Sch?tz Schmuck a ?crit : > Dear All, > > I'd like to specify binary search trees parameterized with the > comparison function on the data items stored in them. I run into the > problem that I am not allowed to do anything with the function > pointers other than check for equality. > > How would one go about this? Well, the first thing I would do is to specify binary search trees with a specific comparison function. I would think about making a parametric one only after succeeding to specify and prove a specific one. Then, to make that parametric, I'm afraid that ACSL is missing constructs on function pointers: typically, one would like to specify something like "the function pointed by this pointer has this contract". But I'm not aware of any way to do that in ACSL. By the way, about specification of binary search trees and similar structures, there are already many existing material, e.g see the recent paper https://hal.inria.fr/hal-01067217 or the VCC case study http://vacid.codeplex.com/SourceControl/latest#VACID-0/VCC/RedBlackTrees.c Hope this helps, - Claude -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |