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] behaviors in ACSL

  • Subject: [Frama-c-discuss] behaviors in ACSL
  • From: pascal.cuoq at cea.fr (Pascal Cuoq)
  • Date: Thu, 11 Dec 2008 10:48:27 +0100
  • In-reply-to: <FA587957-6A90-415F-971C-21781A0AB522@first.fraunhofer.de>
  • References: <4FA912B7D4D8468FBACF5B5DDE198385@AHARDPLACE> <C88F4E451E884829944B1A79F874868C@AHARDPLACE> <20081010124942.4f8a52db@is005115> <1B3FA18004D74D5787DB01AD1EB95900@AHARDPLACE> <14791e30810100413p41eb2e81i89e9f8da63b3040d@mail.gmail.com> <C5F22AF6BA75453CA2EDEADB270E33F3@AHARDPLACE> <14791e30810100505i22345288s5a519d7eab160828@mail.gmail.com> <8F56F47622DB4469B4EBD734D7C08712@AHARDPLACE> <48F33637.5080109@inria.fr> <756435F7D0F44C23B2C7F91E053F77B9@AHARDPLACE> <14791e30810140214r29c903b5w3287a3c33afde56f@mail.gmail.com> <0215081F-3BED-430D-9C3B-E5ABD4212D94@first.fraunhofer.de> <8CFD89A5-CBA1-4F9A-BA19-7ACDDC6F47A4@cea.fr> <A1761223-6344-4BF1-865F-C9F808F931EE@first.fraunhofer.de> <6B884929-2B22-48C2-AC51-44A1AD02D93A@cea.fr> <FA587957-6A90-415F-971C-21781A0AB522@first.fraunhofer.de>
>
Hi!

I am cc-ing the mailing list.

>
> /*@
>   requires 0 <= length;
>   requires \valid_range(a, 0, length-1);
>
>   assigns nothing;
>
>   behavior match:
>     assumes \exists integer k; 0 <= k < length ==> a[k] == value;
>     ensures \result < length ==> a[\result] == value;
>     ensures \forall integer k; 0 <= k < \result ==>  a[k] != value;
>
>   behavior no_match:
>     assumes \forall integer k; 0 <= k < length ==> a[k] != value;
>     ensures \result == length;
>
>   complete behaviors;
>   disjoint behaviors;
>
>  */
>  int find_array (int* a, int length, int value);


I think that you are using 'assumes' right.
The first 'ensures' clause in the 'match' behavior looks a little  
strange,
though. Isn't the "\result < length" in itself one expected post- 
condition
of the function when this behavior holds? I would change

   ensures \result < length ==> a[\result] == value;

into

   ensures \result < length ;
   ensures a[\result] == value;

This may be an useful way to look at "assumes", depending on
your background:
Classical Hoare logic does not have "assumes", only one precondition
and one post-condition. But, when you try to use it, you end up very
often writing post-conditions of the form
"if (some condition that depends only on the pre-state) then something"

The "assumes" clause is a convenient way to format these conditions.
It saves you the writing of (and the risk of forgetting, introducing a  
bug in
your specification) all the \old(...) modifiers since the syntax makes  
it
clear that 'assumes' apply to the pre-state, and since these conditions
often have additional properties, such as being exclusive or  
complementary,
it gives the opportunity to express this  concisely.

Pascal

PS: this is not related, but I used the words so now I must say this  
in case
someone googles this message. Participants in the list do not need to  
read
this.
About bugs in specifications: they can happen. It is possible to write
contracts that are not what you intended but happen to be satisfied by
the function.
Firstly, these specification bugs only go uncaught when
the function incidentally satisfies also the buggy specification. You  
are in
effect writing what you want the function to do twice, once in the code
and once in the specification, and the redundancy catches many errors
that would otherwise go unnoticed.
Secondly, these bugs are generally caught at the next level of  
specification,
when you realize that you do not have enough hypotheses to prove that
the caller to the function with the wrong contract satisfies its own  
contract.
In another, but very specific, sense, bugs in specifications can not  
happen.