Subject: RE: the problem with/phenomenon of assume/guarantee
From: Sandeep K. Shukla (skshukla@ics.uci.edu)
Date: Thu Jul 12 2001 - 19:26:25 PDT
Hi Cindy,
After experimenting differently with SMV, I see your point.
Sandeep
module myM(a,b, c, d) {
input a: INDEX;
input b : INDEX;
output c: INDEX;
output d: INDEX;
next(c) := a;
d := b;
}
module main(){
a,b:INDEX;
c,d: INDEX;
M1: myM(a,b,c,d);
t: INDEX;
forall (t in INDEX) {
prop2[t] : assert(G((a=t) -> X(b=t)));
assume prop2[t];
prop3[t] : assert(G( (c = d)));
using prop2[t]
prove prop3[t];
}
}
> -----Original Message-----
> From: owner-vfv@eda.org [mailto:owner-vfv@eda.org]On Behalf Of
> eisner@il.ibm.com
> Sent: Wednesday, July 11, 2001 11:49 PM
> To: vfv@eda.org
> Cc: roy.armoni@intel.com
> Subject: the problem with/phenomenon of assume/guarantee
>
>
>
>
> all,
>
> roy and i have been discussing off-line what i see as a problem with the
> assume/guarantee paradigm, and what roy terms a phenomenon, or an
> artifact.
> i asked roy to explain this to the committee, but since he is
> traveling and
> has not had time, we agreed that i be the one to explain it to
> you. a word
> file containing a very simple example is attached below.
>
> the attachment shows that the problem is not related to one specific
> language. in fact, as roy has pointed out, it exists also in
> ltl, with the
> following assumption: G ((t <-> X t) & (a=t -> X b=t)). thus,
> the problem
> is with the paradigm itself. note that the example does not show that the
> paradigm breaks down: the paradigm says that *if* you can prove that E
> models f and that M models f->g, then you can conclude that E||M models g.
> since in the example we cannot prove that M models f->g, the paradigm does
> not require us to be able to conclude anything at all. from a purely
> formal point of view, then, the paradigm is upheld by the example.
> however, this example calls into question the practical applicability of
> the assume/guarantee paradigm for many formulas.
>
> in light of all this, we find the mantra that "every FTL property can be
> used as an assumption (and as an assertion)" to be formally correct, but
> misleading. using the formula shown in the example as an assumption is
> possible, but will result in a false negative - i.e., in a counter-example
> to a specification which is valid under the assumption. users will not
> tolerate false negatives (and should not be told to).
>
> thus, while full support of the assume/guarantee paradigm is certainly
> "nice to have", we know of no language for which the paradigm is useful
> for all formulas. users should not be made to understand why formally the
> paradigm is fully supported, rather, they should be guided by the language
> as to how to make use of its capabilities.
>
> regards,
>
> cindy.
>
> (See attached file: assumeguaranteeproblem.doc)
>
> Cindy Eisner
> Formal Methods Group Tel: +972-4-8296-266
> IBM Haifa Research Laboratory Fax: +972-4-855-0070
> Haifa 31905, Israel e-mail:
> eisner@il.ibm.com
>
This archive was generated by hypermail 2b28 : Thu Jul 12 2001 - 19:30:13 PDT