Subject: FTL fully supports that assume/guarantee paradigm
From: Armoni, Roy (roy.armoni@intel.com)
Date: Thu Jul 12 2001 - 06:35:54 PDT
Hi Everyone,
Following an early discussion on the assume/guarantee paradigm, Moshe Vardi
and
myself wrote the attached document to explain how a full support for
assume/guarantee is achieved in FTL, hence, to show that it is very useful.
The claims that were made earlier that "the assume/guarantee paradigm does
not
require us to be able to conclude anything at all"(Cindy) were made because
in some
logics it is indeed impossible to conclude anything. However, the attached
document
contains a definition for completeness that does require that IT WILL ALWAYS
BE
POSSIBLE TO CONCLUDE SOMETHING. Thus, answering the "question the practical
applicability of the assume guarantee paradigm" (Cindy). We show that in a
careful design of a logic like we did in FTL, the assume/guarantee becomes
very
practical.
Enjoy, Roy
<<ag.ZIP>>
This archive was generated by hypermail 2b28 : Thu Jul 12 2001 - 06:37:24 PDT