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 |
- Prev by Date: [Frama-c-discuss] Jessie - help proving adequate behavior on array computation in loops
- Next by Date: [Frama-c-discuss] CFP: 9th International Conference on TESTS AND PROOFS (TAP 2015)
- Previous by thread: [Frama-c-discuss] Jessie - help proving adequate behavior on array computation in loops
- Next by thread: [Frama-c-discuss] CFP: 9th International Conference on TESTS AND PROOFS (TAP 2015)