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] question about hybrid logic functions
- Subject: [Frama-c-discuss] question about hybrid logic functions
- From: jsp at di.uminho.pt (Jorge Sousa Pinto)
- Date: Wed, 29 Jul 2009 11:10:02 +0100
Hi, Consider some hybrid logic function (or predicate) for which no definition or axioms are given (the function is simply declared). Is it in principle possible to use such a function in ACSL contracts? The situation I have in mind is to specify the behaviour of some abstract data type and to be able to reason about operations on that type independently of concrete implementations. For instance something like struct stack {} st; /*@ axiomatic A { @ logic integer count_of{L} (Stack s) ; @*/ /*@ requires 0 < count_of{Here}(st); @ ensures count_of{Here}(st) == count_of{Old}(st) - 1; @*/ void pop(void) ; One would like to be able to reason about pop without an actual implementation of it (or indeed of the stack type!) being given. I've tried this in Frama-c Lithium and obtain an inconsistency, I wonder if this idea is just absurd? A different task would of course be to prove the correctness of a given implementation by defining the logic function in accordance with the concrete type (that one I can do). Many thanks Jorge -------------- next part -------------- A non-text attachment was scrubbed... Name: smime.p7s Type: application/pkcs7-signature Size: 3110 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090729/f91243b7/attachment.bin
- Prev by Date: [Frama-c-discuss] Problem with real division
- Next by Date: [Frama-c-discuss] Problem with real division
- Previous by thread: [Frama-c-discuss] Problem with real division
- Next by thread: [Frama-c-discuss] Oracles of Jessie tests in source distributions
- Index(es):