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] meaning of disjoint and complete behaviors

  • Subject: [Frama-c-discuss] meaning of disjoint and complete behaviors
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Thu, 11 Apr 2013 11:27:26 +0200
  • In-reply-to: <CA+yPOVh0UQ3xA42+wHLY=wPrHvLQ5hLxyH1PMpE26ZSegQvCrQ@mail.gmail.com>
  • References: <A16B5630-89E2-4BD5-B49B-D1EAADCB62FC@udel.edu> <CA+yPOVh0UQ3xA42+wHLY=wPrHvLQ5hLxyH1PMpE26ZSegQvCrQ@mail.gmail.com>
Hello,

2013/4/10 Virgile Prevosto <virgile.prevosto at m4x.org>:
>>  But the validity of that formula does not depend on the implementation of the function; it depends only on the contract (only on P, A1, and A2).  So what difference does it make to add this clause to the contract?
>
> Indeed, complete and disjoint clauses do not really say anything about
> the implementation. Rather, you can see them as a check on the
> contract itself.

I would add that nothing prevent you to add those kind of disjoint or
completness formula to the contract, but behaviour approach brings
improved readability. This is very useful to express real-world
specifications (e.g. the various expected functional behaviours and
erroneous behaviours of a function).

Best regards,
david