--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on October 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] specifying binary search trees ...?





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                    |