--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about hybrid logic functions



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