Well based on what you have just told me, I would feel that my Init
paragraphs that I have written are a form of Operation. When the system is
initialized these should be the first set of operations that are run to
make sure the subsets of consequence are set to the proper starting
parameters. The others we do not care what there values are initialized to
and are hence not in the Init paragraphs. So based on what you have said
does that mean then that pushed = {} should be changed to pushed' = {}
since it would be a consequence of the Init operation running at start up?

If this change is necessary, and of course I will apply it to the other two
init operations, would the pre operator then be more useful in being
applied to this operation?


On Thu, Sep 20, 2012 at 9:59 AM, Roger Bishop Jones <> wrote:

> Jon,
> On Wednesday 19 Sep 2012 22:26, Jon Lockhart wrote:
> > I thought that might come up, the idea that I missed
> > pushed = {}. Since this is describing an initialization
> > section for the system, would pushed = {} need to be a
> > precondition? What I mean is is that when the subset
> > pushed is created or generated, the system may very well
> > fill it with garbage, but when the system initializes
> > pushed must be set to the empty set. Does this then
> > still need to be a precondition or does this become just
> > a by product I have to prove of showing the
> > preconditions of the init operation?
> The precondition operator is really only relevant to schemas
> which are operations, i.e. in which there is a before and
> after state and possibly some outputs.
> i.e. in which there are components ending ' and possibly
> some ending with ?
> When applied to such a schema the precondition operator
> tells you essentially the domain of the operation, i.e. all
> the possible combinations of before state and input
> variables (and actually any other junk) under which some
> possible after state and output values are specified.
> The initial state is not an operation, its just a state, so
> the notion of precondition is not really applicable.
> When you apply the precondition operator to a schema it
> obtains its result by existentially quantifying over the new
> state and output components.
> If there are none, then this has no effect.
> This explains why pushed={} is in your "precondition".
> You can find a description of the Pre operation in the
> ProofPower-Z reference manual in the section on schema
> expressions.
> Roger
Proofpower mailing list

Reply via email to