Roger, 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? Regards, Jon On Wed, Sep 26, 2012 at 4:35 AM, Roger Bishop Jones <r...@rbjones.com> 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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
