That is an interesting point you bring up. It is very true that there are
static sets in there that are subsets in there that we do not want to
change. We would only really want to change pushed set, adding and removing
buttons from it. Same for the other states, they have subsets we would not
want changing in the specification. I like the idea of moving them out of
the scheme blocks and into axiomatic blocks.

I have two questions on that then. First, from a since and style
standpoint, if I wanted to make everything neat in the spec I would place
the no changing sets in the axiom after the state schema, but for
functionality standpoint, if I wanted to use them in the predicate section
of the schema they would need to go before it. So what would you see as
being the better option? The second is would I prove their consistency just
like I did the global variables?

I do see a problem though in that I don't want those sets to be accessed by
anyone, only if the schema is included in the beginning of the operation.
Could we resolve this matter by using the schema paragraphs? So we would
create two schema descriptions of Button_State for example and then the
first contains the static and the second the dynamic sets. Then when
accessing an operation the static or does not change symbol is placed in
front of the static Button_State schema, allowing access to the sets, but
not allowing change, and this way only when the name is provided in the
description is the information accessible. Would that work to accomplish
the same goal?


On Wed, Sep 26, 2012 at 4:35 AM, Roger Bishop Jones <> wrote:

> Jon,
> On Tuesday 25 Sep 2012 22:05, Jon Lockhart wrote:
> > I started doing the "There Exist" proofs, and as you said
> > they seem quite trivial indeed, but I seem to be stuck
> > after the first two lines. So I have the goal, and it
> > has been rewritten, now I am not sure what is the right
> > question to ask. Do I do the z_"There Exist"_tac or
> > something else? What constitutes a witness for some of
> > the predicate declarations.
> Ideally you would say "prove_∃_tac" and it would do it for
> you, but at present automation for existential goals in Z is
> not strong, so you normally have to supply the witness
> yourself and should use z_∃_tac.
> You have to ask yourself what are the objects which belong
> to the schema (ButtonState in this case) and chose a simple
> one to use as a witness.
> You then have to prove that the witness does indeed have the
> required properties.
> So the question is, "what's a simple binding which satisifies
> the ButtonState predicate?", i.e. what are the acceptable
> states of the buttons.
> The components of ButtonState are all sets.
> You have said nothing which requires any of them to be non-
> empty, and the specified relationships all hold if they are
> all empty.
> So the binding in which every component is the empty set
> will be your simplest witness.
> If you supply that witness and then rewrite that should
> solve the goal.
> At this point you might ask yourself whether "ButtonState"
> does not allow more things to vary than might be thought
> acceptable.
> Do you really want your system to allow all the buttons to
> disappear, or even to allow that the set of buttons might
> change, or to allow that a floor button become a lift button?
> I don't know your application, but I would have thought that
> the set of buttons would be fixed and only the "pushed" bit
> was actually part of the state.
> In that case you could have buttons, floorButtons and
> elevatorButtons as loosely specified by an axiomatic
> paragraph, so that they are fixed in any implementation of
> the spec but not fixed by the spec, and then you would have
> only one component in ButtonState, i.e. "pushed",
> constrained to be a subset of the available buttons.
> Roger
Proofpower mailing list

Reply via email to