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: Claude.Marche at inria.fr (Claude Marche)
  • Date: Mon, 24 Aug 2009 14:38:32 +0200
  • In-reply-to: <B0130C58-E12F-44DA-8F19-E94169F4BBE3@di.uminho.pt>
  • References: <B0130C58-E12F-44DA-8F19-E94169F4BBE3@di.uminho.pt>
Jorge Sousa Pinto wrote:
>
> 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?
>
Yes, but some information must be given on which part of the memory heap 
it depends on.
> 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) ;
>   @*/
>
here, by default it is assumed that the value of  "count_of{L} (s)" does 
not depend on the heap, which is not what you want...

> /*@ 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?
The inconsistency follows from what I've said above: since st is 
unchanged, count_of{Here}(st) == count_of{Old}(st), hence if you state 
the same with - 1, it introduce a contradiction

The idea of "abstract data type" should be modelized by providing an 
abstract state, which is the purpose of "model fields" (ACSL manual, 
section 2.11.2) which also exist in JML for Java. Unfortunately these 
are not supported in Frama-C yet. What you can do also is to use a ghost 
field.

//@ logic type abstract_stack;

struct stack {
  //@ ghost abstract_stack my_abstraction;
} st;

/*@ axiomatic A {
  @    logic integer count_of{L} (Stack s) reads s.my_abstraction;
  @*/

/*@ requires 0 < count_of{Here}(st);
  @ assigns st.my_abstraction;
  @ ensures  count_of{Here}(st) == count_of{Old}(st) - 1;
  @*/
void pop(void) ;

and this will not give any inconsistency.


Hope this helps,

- Claude


>
> 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
>
> ------------------------------------------------------------------------
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |