Roger, I am having a little trouble getting the axioms created, moving the static portions of the Button_State to an axiom from the schema. I can't seem to get the proof to operate properly. Any suggestions?
As always the zip is attached. Thanks, Jon On Thu, Oct 4, 2012 at 3:08 PM, Jon Lockhart <[email protected]> wrote: > 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 <[email protected]>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 >> >> >> >> >> >> >
elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
