[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: COND and incomplete information



Robert P. Goldman writes:
 > I'm afraid I don't understand this.  I understand that I am defining a
 > function but, since p is a variable (of type process in this case),
 > why is maybe(p) a constant function?  Surely if p and q are different,
 > maybe(p) need not equal maybe(q).  Or have I misunderstood the syntax?

You're right, I misspoke.  The function `maybe' may have
different values given different arguments.  Its value at
any fixed argument, however, is fixed.  That may or may not
make sense in your example; I don't know what p represents.

If the value of p uniquely identifies a single execution of
a process, then it may be reasonable to use your `maybe'
approach.  (Or the `choose' equivalent I describe below.)
In this case, you could prove things like

   wanted_time(p) = timer_setting(p) 
     IMPLIES (run_time(p) = 123 OR run_time(p) = 345)

If p's value only specifies the values of certain parameters
of the process, then you probably want run_time to be
nondeterministic, since you want to allow two processes with
the same parameters to choose different paths.  If that's
the case, you'll probably want run_time to return a set or
range of possible runtimes.

By the way, an equivalent expression to maybe(p), which
won't require defining extra functions, is

	choose({b:bool|true})

That has the added advantage that you can use it several
times and each occurrence may have a different value.

- Darrell