Re: COND and incomplete information

["Robert P. Goldman" <goldman@htc.honeywell.com>]

>>>>> "JR" == John Rushby <RUSHBY@csl.sri.com> writes:

JR> Robert,
>> maybe(p) : bool
>> 
>> interrupted(p) : bool =
>> COND
>> wanted_time(p) < timer_setting(p)) -> false,
>> wanted_time(p) > timer_setting(p)) -> true,
>> wanted_time(p) = timer_setting(p)) -> maybe(p)
>> ENDCOND

JR> As you and Darrell Kindred noted, the problem with this is that the outcome
JR> in the third case is always the same (you just don't know what it
JR> is).

Actually, I was thinking of p as being a single, unique process
invocation (the full theory makes this clear).  So the fact that

p = q -> maybe(p) = maybe(q)

doesn't bother me at all.

The thing that did bother me was that I was gooping up the global
namespace with this maybe function.

I suspect that the solution to the question I was asking is to simply
scope the function inside the definition of interrupted.

Best to all,
Robert

---

• References:
  • COND and incomplete information
    • From: "Robert P. Goldman" <goldman@htc.honeywell.com>
  • Re: COND and incomplete information
    • From: John Rushby <RUSHBY@csl.sri.com>

• Prev by Date: Re: Why no TCC generated?
• Next by Date: Emacs version?
• Prev by thread: Re: COND and incomplete information
• Next by thread: PVS @ Linux other than RedHat
• Index(es):
  • Date
  • Thread