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] specifying binary search trees ...?

  • Subject: [Frama-c-discuss] specifying binary search trees ...?
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Tue, 21 Oct 2014 13:12:11 +0200
  • In-reply-to: <87h9zuwesv.wl%MarkoSchuetz@web.de>
  • References: <87h9zuwesv.wl%MarkoSchuetz@web.de>


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                    |