Subject: the problem with/phenomenon of assume/guarantee
From: eisner@il.ibm.com
Date: Wed Jul 11 2001 - 23:49:08 PDT
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 : Wed Jul 11 2001 - 23:44:00 PDT