On Friday 28 Sep 2012 22:26, Jon Lockhart wrote: > 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?
First I should repeat my caveat. This is not a style of specification which I have used or studied, so my views on this may be eccentric. If you are using ProofPower you have to present the specification so that every global variable is specified before it is used. There may be tools which can reorder the specification for you, but ProofPower doesn't. I'm not entirely sure what you meant by "in the axiom after the state schema", I hope you didn't mean in the predicate of the state schema! Yes, consistency proofs are the same as the ones you have been doing. When you say "just like the global variables", you do them like global variables because they will actually be 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. It won't be possible to change them, but they will be global variables so any part of the specification after they have been introduced could access them. > 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. I think that is a good way of organising this material. But the nub of the original suggestion was that they might be taken out of the signature of the operations, and in order for them to be accessible in defining the operations on the state they would have to be made into global variables (which is appropriate for something the specification regards as fixed in value). So if you did define a schema containing what one might consider configuration data, you would have to use that schema to introduce the names in its signature as global variables so that they could then be accessed in you operation specifications (or in your definition of state). > 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? You could do something like this, though its not what I intended to suggest. If I understand you correctly you are suggesting that the signature of the operation contains certain fixed data as well as the components which are subject to change (and any input or output values). I have never seen this done, and so I imagine this is a larger departure from normal practice than I was advocating. It has some disadvantages relative to the method I intended to suggest. Generally it is a good idea to try and structure the specification so that the size of signatures does not get very large. It is a disadvantage of Z that the syle of specification encourages all the state of the system to be represented in the flat signature of a single state schema, You can split this up into many parts and use schema inclusion to make this seem better structured in the specification, but when you come to reasoning with it you will be reasoning with objects which have very large signatures, and this make comprehension of what's going on more difficult. In ProofPower is can lead to performance problems, and may lead to hard to understand diagnostics from the type inference system. Another problem which may arise is in the schema calculus. I have not looked into it, but operations like composition may not do the right thing with the extra components in the schema. You could of course put the configuration variables in the state with an equivalence operator, then you would be back with something more standard (perhaps that's what you intended). Schema composition would then do the right thing. I suspect that this conversation is a little to intricate to work very well by email, since the misunderstandings which arise in such a discussion take to long to resolve. If you want to talk about this we could have a Skype conversation, you can find me on skype from my email address. (we would have to agree a time by email). Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
