Subject: RE: the problem with/phenomenon of assume/guarantee
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Thu Jul 12 2001 - 02:19:33 PDT
sandeep,
your example does not show the use of the assume/guarantee paradigm. in
order to use the paradigm, you have to show that E \models f, and that M \
models f -> g. however, you put your formulas inside of main, which is
already E||M.
if you try to prove f -> g in M without E, you will see the problem.
(fixing t to first 0, then to 1 in M eithout E will indeed work, but that
is the whole point.)
cindy.
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
"Sandeep K. Shukla" <skshukla@ics.uci.edu> on 12/07/2001 10:32:27
Please respond to "Sandeep K. Shukla" <skshukla@ics.uci.edu>
To: Cindy Eisner/Haifa/IBM@IBMIL, vfv@eda.org
cc: roy.armoni@intel.com
Subject: RE: the problem with/phenomenon of assume/guarantee
This gives me a chance to show off how Cadence SMV is great!
I just coded the example in cadence SMV and guess what, all the things
you said cannot be proven are proved with SMV easily.
In the first case, I vary t, and hence I had to change your assertions
to include p_t (past value of t), in the second case, I use layer
constructs
to fix t, and you can run the proof twice by commenting out one of the
layers (FixT0, FixT1) and using the appropriate assertions.
Sandeep
module myE(i,a,b){
input i : boolean;
output a : boolean;
output b: boolean;
init(b) := 0;
next(b) := i;
a := i;
}
module myM(a,b, c, d) {
input a: boolean;
input b : boolean;
output c: boolean;
output d: boolean;
init(c) := 0;
next(c) := a;
d := b;
}
module main(){
i, a,b,c,d: boolean;
E1: myE(i,a,b);
M1: myM(a,b,c,d);
t: boolean;
p_t: boolean;
init(p_t) := 0;
next(p_t) := t;
prop1: assert(G(c=d));
prop2: assert(G((a=t) -> X(b=p_t)));
prop3: assert(G(G((a=t) -> X(b=p_t)) -> G(c=d)));
prop4: assert(G((a=t) -> X(b=p_t)) -> G(c=d));
}
However, if you are not interested in t to vary, then try the following
module myE(i,a,b){
input i : boolean;
output a : boolean;
output b: boolean;
init(b) := 0;
next(b) := i;
a := i;
}
module myM(a,b, c, d) {
input a: boolean;
input b : boolean;
output c: boolean;
output d: boolean;
init(c) := 0;
next(c) := a;
d := b;
}
module main(){
i, a,b,c,d: boolean;
E1: myE(i,a,b);
M1: myM(a,b,c,d);
t: boolean;
layer fixT0: {
t := 0;
}
--layer fixT1:{
-- t:= 1;
-- }
prop1: assert(G(c=d));
prop2: assert(G((a=t) -> X(b=t)));
prop3: assert(G(G((a=t) -> X(b=t)) -> G(c=d)));
prop4: assert(G((a=t) -> X(b= t)) -> G(c=d));
using t//fixT0
prove prop2, prop3, prop4;
-- using t//fixT1
-- prove prop2, prop3, prop4;
}
> -----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 - 02:14:06 PDT