Subject: Re: Temporal e
From: David Van Campenhout (dvc@verisity.com)
Date: Wed Jul 11 2001 - 07:59:13 PDT
>
> On one hand, I understand that Temporal e does not have full negation.
> On the other hand, the claim is that there is support for A/G. But that
> means that youhave to have negation, at least at the top level.
>
Correct. Temporal e does not have negation as an operator; instead it
has 'fail'. However, if 'fail' acts at the top level, it behaves like
negation, thus supporting assmue guarantee reasoning.
(For nested subexpressions of 'expect' or 'assume' declarations, both
the omega and the star semantics matter; for top level expressions
only the omega semantics matter. The omega semantics of 'fail' is
identical to that of complementation (negation); the star semantics of
'fail' is very different.)
David
This archive was generated by hypermail 2b28 : Wed Jul 11 2001 - 08:00:24 PDT