Roger, So after some serious thought the last couple of days, and after having some discussions with my advisers, and comparing the pros and cons of the various options I have at accomplishing the goal I want to achieve, I have decided to move everything that is static in my state schemas to axioms like you had mentioned. It definitely is the best option and accomplishes the goal I need, along with further placing realistic constraints on the system. Once I get it all written up, I will send you a copy so you can look at it and maybe provide further advice. Once this is all wrapped up I got to get back to the init operations and get those proven.
Regards, Jon On Tue, Oct 2, 2012 at 4:23 AM, Roger Bishop Jones <r...@rbjones.com> wrote: > > 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
