Roger, As for the change to the Intial Condition block I changed to what I have read for literature over here, which is what Jacky claims is best practice. I only switched it back to the original so that I could work from what was original to the specifciation before moving to ProofPower and becuase since I had moved back to working on rewriting the state properties into static and dynamic areas, I had forgotten the discussion of why we switched to using the prime on the State variable name in the Init operation. It is quite an easy change back, so I will more for the reason, as you have mentioned, I rather be consistent with what Spivey and Woodcock have done over say Jacky.
This brings me to the next point. I realized from the output we had switched to a horizontal schema notation, as for work I had seen in my readings and from the other outputs I had worked with, but I thought the braces around the schema replacement were of some consequence. It sounds like from your account that they are just there for sanity purposes and should look at it like I did any other variable in the previous proofs and just provide proper witness to the system to show the proof. I assume I acheive this by using the "there_exists" tactic like I have on the other existance proofs I have shown. The other question I have is is there any harm, or looking at it the other way any need, to use the precondition proof on intialization operations if I am using an existance proof already? The reason I was going with the precondition proofs as my starting base was because they were the proofs that were used in your example specification in the paper that is on the ProofPower site. As for your final point, you are quite correct in that the specification I have written is a functional specification describing what the system must accomplish, but not how those objectives can be accomplished, that is what I was intending for code. Essentially this specification document was constructed from a set of requirements, so a requirements specification, from a customer, and I took those and constructed this specification to describe what the elevator must do to meet the needs of the customer. As for the question about certain aspects of the elevator, making sure all floors in a direction serviced, or you are able to get off, I think I could see a way, possibly, to state this in a schema notation, but in proving such a claim I am not sure on. My idea of using the schema may be incorrect as well. Regards, Jon On Tue, Oct 16, 2012 at 4:21 AM, Roger Bishop Jones <r...@rbjones.com> wrote: > Jon, > > On Tuesday 16 Oct 2012 01:12, Jon Lockhart wrote: > > > I guess I didn't quite understand or comprehend properly > > the second point you were trying to make. I inserted an > > existance proof like I had done for the state schemas > > and I unfortunately get a very interesting goal after > > the rewrite, as seen in the error zip attached. > > The point I was making was very elementary, so you probably > already understood it. > I didn't have a specific issue to address and you had already > made a mistake in choice of witness so I thought I would > start there. > > Your present example illustrates what happens when you > rewrite with the definition of a schema. > The first thing that happens is that the schema name is > replaced by the horizontal schema corresponding to the > definition. > Often the context allows this to be eliminated, typically in > favour of the predicate obtained from the declaration and > body parts of the schema, but in some cases as in the > declaration part of your existential, this is not possible. > > It is better when you have an existential goal to supply a > witness before you rewrite. > When you supply the witness the declaration part disappears > and the witness is asserted to belong to the schema. In this > context when you rewrite with the schema definition it is > possible to eliminate the horizontal schema. > > It is not essential to supply the witness first, but if you > don't you are likely to see these unfamiliar expressions in > which horizontal schemas are used. > > I see that you are using operations for initial conditions > rather than following either Spivey or Woodcock with a > before or an after state respectively. > (I don't know a reason why not, except that you are more > likely to get comments along the lines "that's not how you > specify initial conditions"). > > > This > > makes me wonder if it would be better to attempt to use > > the precondition proof code found underneath the start > > of the existance proof for trying to prove properties > > about the init operations, and then further of course > > into the system opertaions. > > If you are using an operation to specify the initial > conditions, then the consistency of your initial conditions > is equivalent to the assertionj that the precondition of the > operation is the before state, in this case > > pre Button_Init <=> Button_State > > The existential form was recommended for the case that you > were specifying the initial condition not as an operation > (a delta Button_state) but as a before state (a > Button_State) or an after state (a Button_State'). > However, the existential proof you have started is perfectly > OK, you just have to carry it through without being phased > by horizontal schemas. > > > The second question I have is a more general one, and > > this may be difficult to answer since I am still green > > at proving properties of formal specifications. Say for > > example I do the precondition proofs and those all work > > out. What else can we say about the operations in this > > system before we exhaust the possibilities and I move on > > to coding, and verification there. > > Before proceeding to implementation you would want to verify > that the system as specified has the most important of the > properties which you would expect of it. > > Think of the difference between a specification of the system, > and a specification of the requirements which the system must > meet. > > You don't have what I would call a "requirements" > specification, you have a functional specification. > The kind of thing a requirements specification might say is > that every request for a lift is eventually honoured, and > that when you get in the lift you are eventually let out on > the floor you requested. > Can you see how to state and prove such claims? > > Roger Jones > > > > > > >
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
