Subject: RE: How Sugar supports the assume/guarantee paradigm
From: Armoni, Roy (roy.armoni@intel.com)
Date: Mon Jul 30 2001 - 09:49:38 PDT
Hi Cindy,
LTL is also a subset of FTL, but I do not know how to prove completeness
of LTL with respect to the A/G.
Could you sketch a proof for your claims?
Regards, Roy
-----Original Message-----
From: Cindy_Eisner/Haifa/IBM%IBMIL [mailto:eisner@il.ibm.com]
Sent: Monday, July 30, 2001 5:24 PM
To: vardi@cs.rice.edu
Cc: owner-vfv; roy.armoni; vfv
Subject: Re: How Sugar supports the assume/guarantee paradigm
moshe,
>To get soundness, you restrict
>to a fragment of Sugar, but then you do not have completeness.
according to the generalized definition of soundness, sugar (and not a
subset) is sound. i fail to understand what completeness has to do with
restricting to a subset. on the contrary, if i restrict to a subset of
sugar, it is easier for me to get completeness, not harder (just as your
trivial logic containing only true and false is complete). in any case, we
never claimed theoretical completeness, only practical completeness, so
this is not an issue.
what is an issue, or should be, is the practical applicability of
assumptions in forspec when not only f, but rather f1, f2, ... fn are
assumed. can you please address this point?
regards,
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
This archive was generated by hypermail 2b28 : Mon Jul 30 2001 - 09:51:53 PDT