### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Thank you for getting back to me. I will certainly look into using the axiomatic block in Z similar to the structure found in the Vending Machine example. It may take me a little to figure out how to structure it appropriately. I will dicuss this concept with my advisers and see what we can come up with. If I run into any troubles or road blocks I will be certain to post them here to get people's thoughts. Regards, Jon On Mon, Nov 12, 2012 at 4:19 AM, Roger Bishop Jones r...@rbjones.com wrote: Jon, Now I am on to another portion of the same specification which I am having difficulty with. I believe it is simaliar to the Vending Machine example where it is shown that the Vending Machine doesn't undercharge. What I would like to show is things like, from Up and Down you can only get to Countdown or Stop, from Stop you can only go to Up or Down, etc. So these would honestly be operation transistions. Is an axiom the best way to handle this like in the Vending Machine example? Is there a better way you could see for this? I hope you mean an axiomatic specification of the required condition rather than an axiom. (which since you are not using axiomatic mode doesn't get translated into an axiom). You are here just defining the condition you want to prove. This is as you say, the procedure adopted in the Vending Machine example, and should be OK in your application. Then you just set your goal using this newly defined concept (whatever it is) and go about its proof. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Thanks for the input. I adjusted the predicate section of my specification to include that precondition requirement, and everything fell right into place. Regards, Jon On Tue, Nov 6, 2012 at 3:17 PM, Roger Bishop Jones r...@rbjones.com wrote: On Tuesday 06 Nov 2012 01:04, Jon Lockhart wrote: Unfortunately I realized I needed to show that the starting and calling floors were greater than zero not greater than or equal to zero. However, this makes the goal false, so far as I can see. You need to change the specification if you want this to be the case. I have modified my goal as such, and was able to prove the first sub goal. The third sub goal should be easy to get since it is exactly like what I was originally proving. I am having trouble though with the second goal, which the point I am at can be seen in the error encountered document I have provided. It looks exactly like goal one, but the linear arithmetic tactic fails to solve it, and I tired introducing a lemma through LEMMA_T, since I could not get lemma_tac working, and I would believe that should give the system enough to prove the goal, but apparently not. It logically makes since in my head. I think the reason linear arithmetic fails is because the subgoal is false. It looks like you don't really understand what lemma_tac and LEMMA_T do. They do not do any useful proof work, they just help you to organise your proof by proving and then using a lemma. lemma_tac assumes you want to use the lemma by adding it into your assumptions using strip_asm_tac, whereas LEMMA_T allows you to specify how you are going to use the lemma. In your proof, you say asm_tac, which is like strip_asm_tac except that it adds the lemma into the assumptions without stripping it. In both cases you have to prove the lemma yourself. You can do that in the same step using THEN1 if you know a tactic which will prove it in one step, otherwise THEN1 will do the first step of the proof and you have to continue on from there. In your case, you could have solved that particular subgoal if you had used linear arithmetic instead of just a rewrite, but the lemma would not help you to solve goal 2, if (as I suspect) its not true, You need to stipulate in your general operation predicate the necessary constraints on the allowable input values. Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On Tuesday 06 Nov 2012 01:04, Jon Lockhart wrote: Unfortunately I realized I needed to show that the starting and calling floors were greater than zero not greater than or equal to zero. However, this makes the goal false, so far as I can see. You need to change the specification if you want this to be the case. I have modified my goal as such, and was able to prove the first sub goal. The third sub goal should be easy to get since it is exactly like what I was originally proving. I am having trouble though with the second goal, which the point I am at can be seen in the error encountered document I have provided. It looks exactly like goal one, but the linear arithmetic tactic fails to solve it, and I tired introducing a lemma through LEMMA_T, since I could not get lemma_tac working, and I would believe that should give the system enough to prove the goal, but apparently not. It logically makes since in my head. I think the reason linear arithmetic fails is because the subgoal is false. It looks like you don't really understand what lemma_tac and LEMMA_T do. They do not do any useful proof work, they just help you to organise your proof by proving and then using a lemma. lemma_tac assumes you want to use the lemma by adding it into your assumptions using strip_asm_tac, whereas LEMMA_T allows you to specify how you are going to use the lemma. In your proof, you say asm_tac, which is like strip_asm_tac except that it adds the lemma into the assumptions without stripping it. In both cases you have to prove the lemma yourself. You can do that in the same step using THEN1 if you know a tactic which will prove it in one step, otherwise THEN1 will do the first step of the proof and you have to continue on from there. In your case, you could have solved that particular subgoal if you had used linear arithmetic instead of just a rewrite, but the lemma would not help you to solve goal 2, if (as I suspect) its not true, You need to stipulate in your general operation predicate the necessary constraints on the allowable input values. Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, Your file does not show what you were trying to do with LEMMA_T, or what you actually did, so its hard to offer much help. lemma_tac is easier to understand that LEMMA_T, so you could try doing it with lemma_tac first. (you can always collapse it down to an application of LEMMA_T once you have succeeded in proving the lemma using lemma_tac). Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, I should have mentioned that the problem goal you are looking at can be solved by linear arithmetic so you don't need any lemma at all. Linear arithmetic is not covered by the tutorlal but this is one way to prove the goal: a (PC_T1 z_lin_arith asm_prove_tac[]); Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Community, After some discussion with my advisors, and after taking a hard look at the project we are trying to apply Zed and its proofs too, we came to the conclusion that we did not need something as complicated as the original controller I was working on. Though showing the great depth in what the language could accomplish, it was really beyond what we need. I am still working on it though so that I can refine it to be simplier and still fit all the necessary information in. In any case I have constructed a newer, much simpler specification, using the Vending Machine example from the Zed tutorial. This was much closer to our needs, though I wanted to work with my elevator as a learning process in application from what I had learned form the Vending Machine. I get to a great point, but then I seem to be stuck, and I can't seem to give the right LEMMA_T insertion to get the system to solve the last 3 pieces of the conclusion. I have spent a good while on subtle rewrites and reordering with no success. I have attached the file for convinence. Any assistance in some quick things to alliviate the isue I am having would be greatly appreciated. File is attached. Regards, Jon Lockhart On Mon, Oct 22, 2012 at 12:49 PM, Jon Lockhart jal...@bucknell.edu wrote: Community, I am having trouble proving my operations now, starting with the first one. I am using the precondition proof, and I believe I have set it up correctly, and I get to a single subgoal and I now need to do an existance proof, but I can't seem to write the write tactic to show all that was left behind. Any suggestions on what I would need to ask to complete the goal? File is attached. Regards, Jon Lockhart -- Forwarded message -- From: Jon Lockhart jal...@bucknell.edu Date: Sun, Oct 21, 2012 at 6:29 PM Subject: Re: [ProofPower] Trying to Prove my Zed Specifications To: Roger Bishop Jones r...@rbjones.com Cc: ProofPower List proofpower@lemma-one.com Roger, Well I will look into those further steps and dicuss the options with my advisor as soon as I finish my work on the operations I have. I am having trouble proving these operations now, starting with the first one. I am using the precondition proof, and I believe I have set it up correctly, and I get to a single subgoal and I now need to do an existance proof, but I can't seem to write the write tactic to show all that was left behind. Any suggestions on what I would need to ask to complete the goal? I believe I should also switch in the operation the states to have primes rather than deltas correct? File is attached. Regards, Jon On Thu, Oct 18, 2012 at 5:46 PM, Roger Bishop Jones r...@rbjones.comwrote: On Thursday 18 Oct 2012 21:14, Jon Lockhart wrote: After fixing the correction you pointed out, I was able to get the existance proofs completed and I removed the precondition proofs for those init operations. You can see this in the attached specification file. You are now using after states for initial conditions, so an existential is the best way to express the consistency of these conditions. However, you are including extra undecorated components in some of the initial state schemas, and I am not aware of a precedent for this. Its not clear what this is intended to mean. I suspect that these names might possibly be better as global variables than as local to the initial state schemas, but it depends what you are intending to say here. Now this brings up a previous question again, along with a new one. 1) Is it necessary to have the precondtion proofs with the exsistance proofs in the specification? If not necessary is it wise to use both, or are both redundant in terms of what they are showing and not necessary? Not necessary for the initial state. 2) I am now on to the first main operation of the specification, and I have a precondition proof outlined, albeit some changes are required of it, to begin proving properties of said operation. Should I stick with the precondition proof for this and the other opertations or is there another proof I should be using? What other proofs just on the operations should I be looking to use? Precondition proofs are simply a consistency check. They tell you when the operations have a result. I have already made some suggestions about what other kinds of thing you might want to prove. Generally proofs may be used either to validate your specification (ideally against some other more abstract specification), or to validate code against the specification, or to validate refinement steps which add more detail or move the spec closer to the code. Which of these you do is up to you or to you customers. Roger newElevatorSpec.doc.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Well I will look into those further steps and dicuss the options with my advisor as soon as I finish my work on the operations I have. I am having trouble proving these operations now, starting with the first one. I am using the precondition proof, and I believe I have set it up correctly, and I get to a single subgoal and I now need to do an existance proof, but I can't seem to write the write tactic to show all that was left behind. Any suggestions on what I would need to ask to complete the goal? I believe I should also switch in the operation the states to have primes rather than deltas correct? File is attached. Regards, Jon On Thu, Oct 18, 2012 at 5:46 PM, Roger Bishop Jones r...@rbjones.com wrote: On Thursday 18 Oct 2012 21:14, Jon Lockhart wrote: After fixing the correction you pointed out, I was able to get the existance proofs completed and I removed the precondition proofs for those init operations. You can see this in the attached specification file. You are now using after states for initial conditions, so an existential is the best way to express the consistency of these conditions. However, you are including extra undecorated components in some of the initial state schemas, and I am not aware of a precedent for this. Its not clear what this is intended to mean. I suspect that these names might possibly be better as global variables than as local to the initial state schemas, but it depends what you are intending to say here. Now this brings up a previous question again, along with a new one. 1) Is it necessary to have the precondtion proofs with the exsistance proofs in the specification? If not necessary is it wise to use both, or are both redundant in terms of what they are showing and not necessary? Not necessary for the initial state. 2) I am now on to the first main operation of the specification, and I have a precondition proof outlined, albeit some changes are required of it, to begin proving properties of said operation. Should I stick with the precondition proof for this and the other opertations or is there another proof I should be using? What other proofs just on the operations should I be looking to use? Precondition proofs are simply a consistency check. They tell you when the operations have a result. I have already made some suggestions about what other kinds of thing you might want to prove. Generally proofs may be used either to validate your specification (ideally against some other more abstract specification), or to validate code against the specification, or to validate refinement steps which add more detail or move the spec closer to the code. Which of these you do is up to you or to you customers. Roger elevatorSpecV5_P1.doc.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On Thursday 18 Oct 2012 21:14, Jon Lockhart wrote: After fixing the correction you pointed out, I was able to get the existance proofs completed and I removed the precondition proofs for those init operations. You can see this in the attached specification file. You are now using after states for initial conditions, so an existential is the best way to express the consistency of these conditions. However, you are including extra undecorated components in some of the initial state schemas, and I am not aware of a precedent for this. Its not clear what this is intended to mean. I suspect that these names might possibly be better as global variables than as local to the initial state schemas, but it depends what you are intending to say here. Now this brings up a previous question again, along with a new one. 1) Is it necessary to have the precondtion proofs with the exsistance proofs in the specification? If not necessary is it wise to use both, or are both redundant in terms of what they are showing and not necessary? Not necessary for the initial state. 2) I am now on to the first main operation of the specification, and I have a precondition proof outlined, albeit some changes are required of it, to begin proving properties of said operation. Should I stick with the precondition proof for this and the other opertations or is there another proof I should be using? What other proofs just on the operations should I be looking to use? Precondition proofs are simply a consistency check. They tell you when the operations have a result. I have already made some suggestions about what other kinds of thing you might want to prove. Generally proofs may be used either to validate your specification (ideally against some other more abstract specification), or to validate code against the specification, or to validate refinement steps which add more detail or move the spec closer to the code. Which of these you do is up to you or to you customers. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On Wednesday 17 Oct 2012 04:18, Jon Lockhart wrote: Attached is my latest attempt. With both the delta operator and priming Button_State, with the existance and precondition proof, I run into a wall. I get close, but can't seem to give it the right witness to solve this simple init operation. The binding display for your witness uses = but should use =^ (equal with hat). Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Thanks, I overlooked the symbol I had used, I appreciate that, that cleared the proof right up. Any thoughts on my email before those? Regards, Jon On Wed, Oct 17, 2012 at 2:21 AM, Roger Bishop Jones r...@rbjones.com wrote: On Wednesday 17 Oct 2012 04:18, Jon Lockhart wrote: Attached is my latest attempt. With both the delta operator and priming Button_State, with the existance and precondition proof, I run into a wall. I get close, but can't seem to give it the right witness to solve this simple init operation. The binding display for your witness uses = but should use =^ (equal with hat). Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, After fixing the correction you pointed out, I was able to get the existance proofs completed and I removed the precondition proofs for those init operations. You can see this in the attached specification file. Now this brings up a previous question again, along with a new one. 1) Is it necessary to have the precondtion proofs with the exsistance proofs in the specification? If not necessary is it wise to use both, or are both redundant in terms of what they are showing and not necessary? 2) I am now on to the first main operation of the specification, and I have a precondition proof outlined, albeit some changes are required of it, to begin proving properties of said operation. Should I stick with the precondition proof for this and the other opertations or is there another proof I should be using? What other proofs just on the operations should I be looking to use? Regards, Jon On Wed, Oct 17, 2012 at 1:16 PM, Jon Lockhart jal...@bucknell.edu wrote: Roger, Thanks, I overlooked the symbol I had used, I appreciate that, that cleared the proof right up. Any thoughts on my email before those? Regards, Jon On Wed, Oct 17, 2012 at 2:21 AM, Roger Bishop Jones r...@rbjones.comwrote: On Wednesday 17 Oct 2012 04:18, Jon Lockhart wrote: Attached is my latest attempt. With both the delta operator and priming Button_State, with the existance and precondition proof, I run into a wall. I get close, but can't seem to give it the right witness to solve this simple init operation. The binding display for your witness uses = but should use =^ (equal with hat). Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Thanks, I overlooked the symbol I had used, I appreciate that, that cleared the proof right up. Any thoughts on my email before those? Regards, Jon On Wed, Oct 17, 2012 at 2:21 AM, Roger Bishop Jones r...@rbjones.comwrote: On Wednesday 17 Oct 2012 04:18, Jon Lockhart wrote: Attached is my latest attempt. With both the delta operator and priming Button_State, with the existance and precondition proof, I run into a wall. I get close, but can't seem to give it the right witness to solve this simple init operation. The binding display for your witness uses = but should use =^ (equal with hat). Roger elevatorSpecV5_P1.doc.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

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

### Re: [ProofPower] Trying to Prove my Zed Specifications

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

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Attached is my latest attempt. With both the delta operator and priming Button_State, with the existance and precondition proof, I run into a wall. I get close, but can't seem to give it the right witness to solve this simple init operation. This does not bode well for the rest of the operations. Thanks, Jon On Tue, Oct 16, 2012 at 2:43 PM, Jon Lockhart jal...@bucknell.edu wrote: 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.comwrote: 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

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Understood, I will make sure to keep all that in mind when I working on the precondition proofs for the operations. The proof could was skeletoned in when I was working on the earlier material b/c I thought it would make things easier when I was able to return to the operations, but since changes have been made that altered the amount of information necessary in those proofs, I certainly need to rewrite them and massage them. 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. 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. 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. Appreciate all your help in this matter. Thanks, Jon On Sun, Oct 14, 2012 at 4:07 AM, Roger Bishop Jones r...@rbjones.com wrote: Jon, On Sunday 14 Oct 2012 04:52, you wrote: Any direction on how to finish these up so I may move on to the actual operations would be greatly appreciated. Two points to keep in mind. First, ProofPower does not automatically rewrite with any of the specifications which you have put in, you have to tell it which you want it to rewrite with, and in your remaining precondition proofs there are more specifications which you have to include in the rewrite. It is possible to make a proof context which expands the default set of rewrites, but at this stage you are probably better just using cut and paste on the lists of global variable names used in the rewrites. Second, when proving the non-emptyness of a schema, as in the initial conditions, you have to think of the schema as a set of bindings, consider the conditions which you have placed on which bindings belong to the schema, and then think of a way of writing down a binding which can be proven to satisfy the conditions. That will be your witness, then you just have to do the proof. Again, make sure you rewrite with everything you need to use. Roger elevatorSpecV5_P1.doc.gz Description: GNU Zip compressed data errorEncountered.doc.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Sunday 14 Oct 2012 04:52, you wrote: Any direction on how to finish these up so I may move on to the actual operations would be greatly appreciated. Two points to keep in mind. First, ProofPower does not automatically rewrite with any of the specifications which you have put in, you have to tell it which you want it to rewrite with, and in your remaining precondition proofs there are more specifications which you have to include in the rewrite. It is possible to make a proof context which expands the default set of rewrites, but at this stage you are probably better just using cut and paste on the lists of global variable names used in the rewrites. Second, when proving the non-emptyness of a schema, as in the initial conditions, you have to think of the schema as a set of bindings, consider the conditions which you have placed on which bindings belong to the schema, and then think of a way of writing down a binding which can be proven to satisfy the conditions. That will be your witness, then you just have to do the proof. Again, make sure you rewrite with everything you need to use. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Friday 12 Oct 2012 20:35, Jon Lockhart wrote: I got back to the specification today, and moved on to proving the elevator state schema, Elevator_State, and I moved the static component elevator to an axiom, similar to the static components of button. Unfortunately I get a weird sub goal pop up that says {} = elevator after I work on the existence proof. Is this b/c I used the empty set as the witness to the elevator axiom proof? No, its because you set both moving and stopped to the empty set, and this can only be the case if there are no elevators. Your spec doesn't say there are no elevators, so you can't prove it. You need to supply a witness for which the union of moving and stopped can be proven to be elevators, even though you don't know what elevators is. One way to do that is to use the state in which everything is stopped, i.e. in which moving = {} and stopped = elevators. I haven't checked that that satisfies the rest of the predicate, but I guess that's probable. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Got that error corrected, thanks for the input. Encounterd a few more hang ups on doing the proof but those were eliminated by grabbing the spec for elevator on the rewrite tactic. Same for floor. Now I am back to the Init operations. I have attached the specification again for you veiwing, but if I remember correctly we were going with using the There Exists proof still on these like we did for the States. Any direction on how to finish these up so I may move on to the actual operations would be greatly appreciated. Regards, Jon On Sat, Oct 13, 2012 at 12:28 PM, Roger Bishop Jones r...@rbjones.comwrote: Jon, On Friday 12 Oct 2012 20:35, Jon Lockhart wrote: I got back to the specification today, and moved on to proving the elevator state schema, Elevator_State, and I moved the static component elevator to an axiom, similar to the static components of button. Unfortunately I get a weird sub goal pop up that says {} = elevator after I work on the existence proof. Is this b/c I used the empty set as the witness to the elevator axiom proof? No, its because you set both moving and stopped to the empty set, and this can only be the case if there are no elevators. Your spec doesn't say there are no elevators, so you can't prove it. You need to supply a witness for which the union of moving and stopped can be proven to be elevators, even though you don't know what elevators is. One way to do that is to use the state in which everything is stopped, i.e. in which moving = {} and stopped = elevators. I haven't checked that that satisfies the rest of the predicate, but I guess that's probable. Roger elevatorSpecV5_P1.doc.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Yeah rookie mistake there huh? I remember us going over that when we first went over the axioms and their proofs, and I most certainly overlooked the little prime added to the variable name. I got back to the specification today, and moved on to proving the elevator state schema, Elevator_State, and I moved the static component elevator to an axiom, similar to the static components of button. Unfortunately I get a weird sub goal pop up that says {} = elevator after I work on the existence proof. Is this b/c I used the empty set as the witness to the elevator axiom proof? Attached is the exact output from the entire elevator state section and the specification. Thanks, Jon On Tue, Oct 9, 2012 at 3:52 PM, Roger Bishop Jones r...@rbjones.com wrote: Jon, On Tuesday 09 Oct 2012 20:22, Jon Lockhart wrote: 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? The problem is that the existential goal you are trying to prove has decorations on the names of the variables, but the witness you have supplied does not. This is a point of difference between proving the non- emptyness of a schema and the consistency of an axiomatic specification. Because the names in the signature of the axiomatic spec have already been introduced as global variables (aka constants), they cannot be used as the names in the existential which must be proven to establish the consistency of the axiomatic specification. So they get primed. When z exists tac complains that it can't match the witness against the signature of the existential, first check that the names you have used in the binding are exactly those in the existential you are trying to prove, then check that the expressions have the right type. regards, Roger Jones elevatorSpecV5_P1.doc.gz Description: GNU Zip compressed data errorEncountered.doc.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

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 jal...@bucknell.edu 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 r...@rbjones.comwrote: 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

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Tuesday 09 Oct 2012 20:22, Jon Lockhart wrote: 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? The problem is that the existential goal you are trying to prove has decorations on the names of the variables, but the witness you have supplied does not. This is a point of difference between proving the non- emptyness of a schema and the consistency of an axiomatic specification. Because the names in the signature of the axiomatic spec have already been introduced as global variables (aka constants), they cannot be used as the names in the existential which must be proven to establish the consistency of the axiomatic specification. So they get primed. When z exists tac complains that it can't match the witness against the signature of the existential, first check that the names you have used in the binding are exactly those in the existential you are trying to prove, then check that the expressions have the right type. regards, Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

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

### Re: [ProofPower] Trying to Prove my Zed Specifications

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

### Re: [ProofPower] Trying to Prove my Zed Specifications

Community, 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. Attached is the spec and the output of the goal where I am at. Also the original proof is in there for now, please just disregard I am leaving it in there for the moment to show what I originally did to what I am now going to with these there exists proofs. I am currently working on Button_State. Roger, Thank you for the catch, and I apologize about that. I am using pushed and pushed everywhere else, I believe. I guess if I missed any they will come up when I am trying to prove. Regards, Jon On Mon, Sep 24, 2012 at 9:05 AM, Roger Bishop Jones r...@rbjones.com wrote: Jon, On Sunday 23 Sep 2012 22:32, Jon Lockhart wrote: I tried adding the exclamation point to the end of the pushed' line, but if gave me a paser error saying free types here not allowed. I have provided exactly the what the paragraph looked like I tried to parse and the error that was reported in the errorEncountered document. The perils of not carefully quoting! The exclamation mark was not intended to be in the formal text, it was just my exclamation. The point I was making was just that you had said push'={} and it should have been pushed'={}! I went back to just having the two exclamation points on pushed and Button_State, in the predicate and declaration section of the schema box respectively, and this generated a monster of subgoals when I tried the provided proof strategy. Obviously there should not be that much to prove, especially when everything is the same, except for push just being set to the empty set. Should be pushed! Make sure you have no occurrences of push and if you still have a problem with the proof post it. I have also gone back and reviewed Jacky's The Way of Zed and he uses the delta operator to signify there are changes being made to the states, though he never discusses initialization, but there appears to be some disconnect between the authors, though I know Spivey and Woodcock should probably be followed so I like to stick with what they say is best practice. I don't have access to Jacky's book so I can't comment. As for the Init and State blocks that I am trying to and have proven, should there be a change there so that the proof is not of precondition but of consistency? As you have mentioned, and I have agreed with, it is really pointless to do the precondition proofs for the states when they are static and not changing, everything remains the same, and they are only showing the information provided is consistent. Yes, try proving: ∃ Init ∙ true and ∃ State ∙ true Both should be trivial proofs. Roger elevatorSpecV5_P1.doc.gz Description: GNU Zip compressed data errorEncountered.doc.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, I tried adding the exclamation point to the end of the pushed' line, but if gave me a paser error saying free types here not allowed. I have provided exactly the what the paragraph looked like I tried to parse and the error that was reported in the errorEncountered document. I went back to just having the two exclamation points on pushed and Button_State, in the predicate and declaration section of the schema box respectively, and this generated a monster of subgoals when I tried the provided proof strategy. Obviously there should not be that much to prove, especially when everything is the same, except for push just being set to the empty set. I have also gone back and reviewed Jacky's The Way of Zed and he uses the delta operator to signify there are changes being made to the states, though he never discusses initialization, but there appears to be some disconnect between the authors, though I know Spivey and Woodcock should probably be followed so I like to stick with what they say is best practice. As for the Init and State blocks that I am trying to and have proven, should there be a change there so that the proof is not of precondition but of consistency? As you have mentioned, and I have agreed with, it is really pointless to do the precondition proofs for the states when they are static and not changing, everything remains the same, and they are only showing the information provided is consistent. Thanks, Jon On Sat, Sep 22, 2012 at 4:07 AM, Roger Bishop Jones r...@rbjones.com wrote: Jon, On Saturday 22 Sep 2012 00:11, Jon Lockhart wrote: I tried what you mentioned after Phil brought it up and if you try to do State' and then push' = {} the system throws an error saying No free types allowed in predicates which to me means that push is not accessible in the predicate section. Should be pushed'={}! Roger elevatorSpecV5_P1.doc.gz Description: GNU Zip compressed data errorEncountered.doc.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Saturday 22 Sep 2012 00:11, Jon Lockhart wrote: I tried what you mentioned after Phil brought it up and if you try to do State' and then push' = {} the system throws an error saying No free types allowed in predicates which to me means that push is not accessible in the predicate section. Should be pushed'={}! Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

I checked Spivey (Understanding Z) and Woodcock (Using Z) on the conventions they use for initial state. Neither of them uses an operation for initial state. In Spivey initial state is simply a constraint on state. In Woodcock initial state is a constraint on state'. I have no idea why Woodcock uses state', it seems to me a harmless eccentricity (but possibly this has become the norm). I observe that though one might specify intial state using an operation which puts the system into that initial state, you are then specifying a transition from some state before the initial state, and of course there aren't supposed to be any states before the initial state, so its an odd thing to do. On this basis I come to the following conclusions. Firstly, jon is out of line with both Spivey and Woodcock in using an operation to specify the initial state. To fall in line he should change Button_Init by removing the delta in the signature. That would suffice to bring him in line with Spivey. To fall in with Woodcock he would also have to add 2 primes one to Button_State and one to pushed. In neither case is Button_Init an operation, and therefore in neither case would a proof of precondition be appropriate. A consistency proof might be thought desirable. In that case the conjecture to be proven would be: exists Button_Init s.t. true On the matter of the other schemas for which jon has done precondition proofs, though a precondition proof is meaningless for a schema which is not an operation, a proof of non-emptyness (essentially a consistency proof for the predicate) might be thought worthwhile. The conjecture to be proven in that case would be the same as the one above for Button_Init. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, I tried what you mentioned after Phil brought it up and if you try to do State' and then push' = {} the system throws an error saying No free types allowed in predicates which to me means that push is not accessible in the predicate section. I also agree that doing the precondition seems redundant now after you explain things, b/c since they are not operators so far, there have been no way to show there were correct unless specifying everything that was in the paragraph, as there was nothing changing, i.e. having a prime after it. So ProofPower won't let me use the 2 prime idea, so that must mean it is not in the ISO Standard as good practice. So maybe I should go with what Spivey is using. Thanks, Jon On Fri, Sep 21, 2012 at 7:00 AM, Roger Bishop Jones r...@rbjones.com wrote: On Friday 21 Sep 2012 11:52, Roger Bishop Jones wrote: I checked Spivey (Understanding Z) In fact it was The Z Notation I checked. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Well based on what you have just told me, I would feel that my Init paragraphs that I have written are a form of Operation. When the system is initialized these should be the first set of operations that are run to make sure the subsets of consequence are set to the proper starting parameters. The others we do not care what there values are initialized to and are hence not in the Init paragraphs. So based on what you have said does that mean then that pushed = {} should be changed to pushed' = {} since it would be a consequence of the Init operation running at start up? If this change is necessary, and of course I will apply it to the other two init operations, would the pre operator then be more useful in being applied to this operation? Regards, Jon On Thu, Sep 20, 2012 at 9:59 AM, Roger Bishop Jones rogerbishopjo...@btinternet.com wrote: Jon, On Wednesday 19 Sep 2012 22:26, Jon Lockhart wrote: I thought that might come up, the idea that I missed pushed = {}. Since this is describing an initialization section for the system, would pushed = {} need to be a precondition? What I mean is is that when the subset pushed is created or generated, the system may very well fill it with garbage, but when the system initializes pushed must be set to the empty set. Does this then still need to be a precondition or does this become just a by product I have to prove of showing the preconditions of the init operation? The precondition operator is really only relevant to schemas which are operations, i.e. in which there is a before and after state and possibly some outputs. i.e. in which there are components ending ' and possibly some ending with ? When applied to such a schema the precondition operator tells you essentially the domain of the operation, i.e. all the possible combinations of before state and input variables (and actually any other junk) under which some possible after state and output values are specified. The initial state is not an operation, its just a state, so the notion of precondition is not really applicable. When you apply the precondition operator to a schema it obtains its result by existentially quantifying over the new state and output components. If there are none, then this has no effect. This explains why pushed={} is in your precondition. You can find a description of the Pre operation in the ProofPower-Z reference manual in the section on schema expressions. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On 20/09/12 17:59, Jon Lockhart wrote: So based on what you have said does that mean then that pushed = {} should be changed to pushed' = {} since it would be a consequence of the Init operation running at start up? I had a quick read yesterday but no time to reply. My initial reaction was you meant pushed' = {}. However, for initialization, you don't have an initial state, so your schema should just have State' where you currently have Δ State I strongly recommend reading chapter 12 of Using Z, available at http://www.usingz.com/ If this change is necessary, and of course I will apply it to the other two init operations, would the pre operator then be more useful in being applied to this operation? pre Init is certainly worth establishing: it is useful to know whether the Init operation can be achieved. Note that with the above change to use State', pre Init is either true or false as there are no unprimed variables. You want to know that it is not false. As there is no initial state, pre Init may be written ∃ State' ∙ Init However, I see you're calculating pre Button_State pre Elevator_State pre Floor_State which is pointless. These schemas are not operations: they have no concept of before state and after state. You'll see that none have primed variables. Not surprisingly, you're finding pre X_State = X_State I also recommend chapter 14 of Using Z. The whole book is worth a read, in fact! Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Thanks for the help and the info. After your explanation I better understand what you are saying and I do agree with the point you are trying to make. I will have to look into that further. Phil, Thank you for the insight and help. From the book, examples, and papers I have read, I was developing my specification on what they had done and said was best practice in Zed. I do agree that proving the state declaration when there was no change was odd, but that is what other had done and that is just what I stuck with. I do like the idea of changing the pushed to a pushed' and thinking of the Init as an operation, but I am more curious as to why we are placing the prime on the entire state, when we are just operating on a member of the state? The delta should signify based on the Zed notation that a change is occurring to the state, but it doesn't mean that that whole state has to change. I am just thinking that placing the prime on the whole state may affect what I am trying to say in the Init operation, if that makes sense. If you be willing to provide further assistance and clarification as I make adjustments that be great. Also, I appreciate the book link. I will def take a look at it and probably add it to the Zed book I already have, The Way of Zed. Thanks, Jon Lockhart On Thu, Sep 20, 2012 at 4:10 PM, Phil Clayton phil.clay...@lineone.netwrote: Jon, On 20/09/12 17:59, Jon Lockhart wrote: So based on what you have said does that mean then that pushed = {} should be changed to pushed' = {} since it would be a consequence of the Init operation running at start up? I had a quick read yesterday but no time to reply. My initial reaction was you meant pushed' = {}. However, for initialization, you don't have an initial state, so your schema should just have State' where you currently have Δ State I strongly recommend reading chapter 12 of Using Z, available at http://www.usingz.com/ If this change is necessary, and of course I will apply it to the other two init operations, would the pre operator then be more useful in being applied to this operation? pre Init is certainly worth establishing: it is useful to know whether the Init operation can be achieved. Note that with the above change to use State', pre Init is either true or false as there are no unprimed variables. You want to know that it is not false. As there is no initial state, pre Init may be written ∃ State' ∙ Init However, I see you're calculating pre Button_State pre Elevator_State pre Floor_State which is pointless. These schemas are not operations: they have no concept of before state and after state. You'll see that none have primed variables. Not surprisingly, you're finding pre X_State = X_State I also recommend chapter 14 of Using Z. The whole book is worth a read, in fact! Phil __**_ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Phil, I was also curious why you said that my system does not have an initial state. Would not the declaration of the Button_State, Elevator_State, etc. be the initial State, or would initialization be considered the initial state? If Button_Init, etc. are not the initial state, would I use Δ Button_Init rather than Δ Button_State in my operations that are further down the line. Thanks, Jon On Thu, Sep 20, 2012 at 4:10 PM, Phil Clayton phil.clay...@lineone.netwrote: Jon, On 20/09/12 17:59, Jon Lockhart wrote: So based on what you have said does that mean then that pushed = {} should be changed to pushed' = {} since it would be a consequence of the Init operation running at start up? I had a quick read yesterday but no time to reply. My initial reaction was you meant pushed' = {}. However, for initialization, you don't have an initial state, so your schema should just have State' where you currently have Δ State I strongly recommend reading chapter 12 of Using Z, available at http://www.usingz.com/ If this change is necessary, and of course I will apply it to the other two init operations, would the pre operator then be more useful in being applied to this operation? pre Init is certainly worth establishing: it is useful to know whether the Init operation can be achieved. Note that with the above change to use State', pre Init is either true or false as there are no unprimed variables. You want to know that it is not false. As there is no initial state, pre Init may be written ∃ State' ∙ Init However, I see you're calculating pre Button_State pre Elevator_State pre Floor_State which is pointless. These schemas are not operations: they have no concept of before state and after state. You'll see that none have primed variables. Not surprisingly, you're finding pre X_State = X_State I also recommend chapter 14 of Using Z. The whole book is worth a read, in fact! Phil __**_ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Gentlemen, I moved on to the next area of my specification, which is the initializations of the states declared earlier, and I am stuck on the first one. No errors or anything, just not sure how to proceed to reduce the goal any further. As of now I actually think what I have done is made the goal more complex. Was using the z_there exists_tac to try and eliminate portions so then I could feed the goal a tac proving the last bit which is not a precondition. Unfortunately using the there exists tactic increased the goal length and just added more. I have tried setting the values to other items with no avail either in reducing the goal. Attached as always is the current spec. Regards, Jon On Tue, Sep 18, 2012 at 5:05 PM, Jon Lockhart jal...@bucknell.edu wrote: Thanks guys for the help. Those were a couple of little errors that I overlooked. Regards, Jon On Tue, Sep 18, 2012 at 4:06 PM, Rob Arthan r...@lemma-one.com wrote: Jon, On 18 Sep 2012, at 20:37, Jon Lockhart wrote: So I have run into an error again while working on my specification. This time it is with the second axiomatic definition, the one right after Roger helped me with last time. Using what he had done, and from the integer example in the tutorial notes, I set up the evidence for how I thought the system would want it to be given to it. Unfortunately this throws an exception and I can't seem to massage it to be what it wants. Attached is the spec and a document containing the error. In ProofPower-Z syntax, when you write down binding, you need to use the equals with a hat (or a double equals sign) between the signature variables and their values (as you did when you supplied the witness to an existential goal in an earlier proof). Also you forgot the prime on the bound variable name numOfButtons'. If you fix that and apply rewrite_tac your goal will be proved. Regards, Rob. elevatorSpecV5_P1.doc.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On Wednesday 19 Sep 2012 21:10, Jon Lockhart wrote: I moved on to the next area of my specification, which is the initializations of the states declared earlier, and I am stuck on the first one. No errors or anything, just not sure how to proceed to reduce the goal any further. As of now I actually think what I have done is made the goal more complex. Was using the z_there exists_tac to try and eliminate portions so then I could feed the goal a tac proving the last bit which is not a precondition. Unfortunately using the there exists tactic increased the goal length and just added more. I have tried setting the values to other items with no avail either in reducing the goal. z_exists_tac doesn't actually do much, it just substitutes in the witnesses you supplied. You have to do something else to actually simplify the result, usually rewrite. In this case asm_rewrite_tac simplifies the goal, and probably would have proved it if it was true. Looks to me like you missed a clause in the precondition: pushed={} Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, I thought that might come up, the idea that I missed pushed = {}. Since this is describing an initialization section for the system, would pushed = {} need to be a precondition? What I mean is is that when the subset pushed is created or generated, the system may very well fill it with garbage, but when the system initializes pushed must be set to the empty set. Does this then still need to be a precondition or does this become just a by product I have to prove of showing the preconditions of the init operation? Thanks, Jon On Wed, Sep 19, 2012 at 5:18 PM, Roger Bishop Jones r...@rbjones.com wrote: On Wednesday 19 Sep 2012 21:10, Jon Lockhart wrote: I moved on to the next area of my specification, which is the initializations of the states declared earlier, and I am stuck on the first one. No errors or anything, just not sure how to proceed to reduce the goal any further. As of now I actually think what I have done is made the goal more complex. Was using the z_there exists_tac to try and eliminate portions so then I could feed the goal a tac proving the last bit which is not a precondition. Unfortunately using the there exists tactic increased the goal length and just added more. I have tried setting the values to other items with no avail either in reducing the goal. z_exists_tac doesn't actually do much, it just substitutes in the witnesses you supplied. You have to do something else to actually simplify the result, usually rewrite. In this case asm_rewrite_tac simplifies the goal, and probably would have proved it if it was true. Looks to me like you missed a clause in the precondition: pushed={} Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

So I have run into an error again while working on my specification. This time it is with the second axiomatic definition, the one right after Roger helped me with last time. Using what he had done, and from the integer example in the tutorial notes, I set up the evidence for how I thought the system would want it to be given to it. Unfortunately this throws an exception and I can't seem to massage it to be what it wants. Attached is the spec and a document containing the error. Regards, Jon On Sat, Sep 15, 2012 at 1:07 PM, Jon Lockhart jal...@bucknell.edu wrote: Roger, Thanks for making that clear about how the system handles that. I was thinking that is what had happened but I wanted to make sure and get a clearer picture. Now time to keep pushing forward. Thanks, Jon On Fri, Sep 14, 2012 at 4:56 PM, Roger Bishop Jones r...@rbjones.comwrote: Jon, On Friday 14 Sep 2012 21:14, Jon Lockhart wrote: Now I have moved on to trying to do the same thing for masterReset, using the exact same code that Roger has implemented in my spec, but now I am getting an error when I try to push the consistency goal. That's because its a single specification for two constants, and you have already proven the consistency goal. Recall that the proof offered a composite witness, a binding with one component for each of the constituents of the signature of the axiomatic specification, both set to True. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com elevatorSpecV5_P1.doc.gz Description: GNU Zip compressed data errorEncountered.doc.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Tuesday 18 Sep 2012 20:37, Jon Lockhart wrote: So I have run into an error again while working on my specification. This time it is with the second axiomatic definition, the one right after Roger helped me with last time. Using what he had done, and from the integer example in the tutorial notes, I set up the evidence for how I thought the system would want it to be given to it. Unfortunately this throws an exception and I can't seem to massage it to be what it wants. Two problems. The first is that you use = in the binding display but ProofPower requires =^ (equal with hat on it). You also missed the prime off the last name in the signature. Once these are fixed rewrite solves the goal. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On 18 Sep 2012, at 20:37, Jon Lockhart wrote: So I have run into an error again while working on my specification. This time it is with the second axiomatic definition, the one right after Roger helped me with last time. Using what he had done, and from the integer example in the tutorial notes, I set up the evidence for how I thought the system would want it to be given to it. Unfortunately this throws an exception and I can't seem to massage it to be what it wants. Attached is the spec and a document containing the error. In ProofPower-Z syntax, when you write down binding, you need to use the equals with a hat (or a double equals sign) between the signature variables and their values (as you did when you supplied the witness to an existential goal in an earlier proof). Also you forgot the prime on the bound variable name numOfButtons'. If you fix that and apply rewrite_tac your goal will be proved. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Thanks guys for the help. Those were a couple of little errors that I overlooked. Regards, Jon On Tue, Sep 18, 2012 at 4:06 PM, Rob Arthan r...@lemma-one.com wrote: Jon, On 18 Sep 2012, at 20:37, Jon Lockhart wrote: So I have run into an error again while working on my specification. This time it is with the second axiomatic definition, the one right after Roger helped me with last time. Using what he had done, and from the integer example in the tutorial notes, I set up the evidence for how I thought the system would want it to be given to it. Unfortunately this throws an exception and I can't seem to massage it to be what it wants. Attached is the spec and a document containing the error. In ProofPower-Z syntax, when you write down binding, you need to use the equals with a hat (or a double equals sign) between the signature variables and their values (as you did when you supplied the witness to an existential goal in an earlier proof). Also you forgot the prime on the bound variable name numOfButtons'. If you fix that and apply rewrite_tac your goal will be proved. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, I had a brief look at the last spec that you posted. I also had a problem unzipping it, but despite a failure message got a decompression by opening the file in emacs. The file decompressed in this way had two issues in it. The first was that it terminated mid paragraph. The second was that there were lower case beta signs systematically appearing throughout. I used a repetitive edit to remove the betas and partially processed the result. Some issues arising were: 1. Semicolons are needed between declarations but not after tha last one in the declaration part. 2. You used the same name (Elevator_State) twice for schemas (perhaps there was a significant beta there or some other problem with the decompression. The second occurence is for an operation over the first so presumably it was decorated in some way). 3. Not all uses of BOOLEAN values have been translated to use True and False instead of 0 and 1, so the remainder give type errors. You may will find it hard work proving the consistency of your specification, even where it looks pretty obvious, and so there might be better value for you in using axiomatic mode (which amounts to assuming consistency) and working on more interesting proofs. You can always go back later and prove the consistency results. On the other hand, consistency proofs will be simpler than proving significant properties of the spec as a whole so it is a place to start learning proof. Its not clear what consistency goal you were attempting, but I'm guessing it was masterStop, in which case using masterStop as a witness won't work. You could use True. And then you will have to rewrite with the definition of True and that of BOOLEAN. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On Friday 14 Sep 2012 10:36, Phil Clayton wrote: On 14/09/12 10:05, Roger Bishop Jones wrote: I had a brief look at the last spec that you posted. I also had a problem unzipping it, ... This doesn't surprise me because the attachment was byte for byte the same as the previous attachment that didn't unzip! I guess Jon sent the wrong file or else something very strange is occurring. Possibly somewhere en-route has a problem with binary attachments. That used to happen a long time ago, but its not something I have seen recently. Perhaps a good idea to attach the ascii version, Jon. Do conv_ascii on your .doc file and attach the result. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On 14 Sep 2012, at 03:01, Jon Lockhart wrote: Phil, Moving them all to there own paragraph worked great. Now I am up to proving the consistency of the axioms, which is where I am run into my next stumbling block. Got the spec load and the consistency goal using the commands no problem. This generates a sub goal which looks relatively straight forward. It using the there exist symbol at the front of the goal, so my initial assumption is to use the z_there exists_tac, as seen in the provided spec. Unfortunately I can't unzip your attachment to check exactly what you are doing. There is minimal proof support for consistency goals in Z, since very few Z users have expressed much interest in proving consistency. Unfortunately just giving it masterStop is not enough, and I can't feed it a list of masterStop and masterReset. Next thought was there should be some tactic like this that also has list in it, but I can't seem to find one. When you set up the consistency goal for a Z axiomatic description, what you see is a mixture of HOL and Z and the existential quantifier is an HOL quantifier not a Z one. So you would need to use %exists%_tac rather than z_%exists%_tac. If the axiomatic description defines several global variables, the witness you need would be provided as a HOL tuple. As the witnesses for the individual variables are likely to be Z terms, you are already into some not entirely trivial mixed language working. I just tried a Z axiomatic description declaring three integers x, y, and z with defining property x y z 0. Here is the tactic that proves the consistency: a(%exists%_tac %%(%SZT%3%%, %SZT%2%%, %SZT%1%%)%% THEN PC_T1 z_library rewrite_tac[z'decl_def, z'dec_def]); Even when you translate that back into the extended character set (e.g., by pasting the bit between %% and %% into ProofPower), it is not very nice. So on the whole I don't think doing consistency proofs is not a good place to start learning proof in Z, because it will expose too much HOL to you. If you have a strong interest in doing consistency proofs later on, it would actually be quite easy to provide some tools to protect you from the HOL. Finally, there isn't a list flavour of %exists%_tac or z_%exists%_tac. It would be a minor convenience in HOL (where existentials with a list of bound variables are obtained by iterating existential quantifier over a single variable), but MAP_EVERY %exists%_tac does what you want. It is rarely what you want in Z, where you use a binding display as the witness for an existential quantifier that binds several variables and where iterated existential quantification is fairly rare. Regards, Rob.___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Gentlemen, First, I find it odd that the zipping is not working when before it was for Phil, and still is for me. I just generated a zip, emailed it to myself, and then unzipped it and got something that looks just fine, exactly what I zipped up. I have though created an ascii version of the document, and have attached on here along with another attempt at zipping the binary file. Let me know if you guys are able to use either of these. Second, I know that the rest of the document has not been corrected Roger for the new Boolean set up for true and false I have described. It has been corrected in my as of now official specification that I have in Word. I am trying to progress section by section or more like Zed paragraph to Zed paragraph, making the corrections that I have semantically checked already in the Word version, and then trying to prove that paragraph. That is why I was currently up to the axiomatic definitions and trying to prove them. After that is done, I will then try to prove the init conditions and everything. Once preconditions have all been proven, I want to move on to do more specific proofs on the specification. Third, Rob I guess I will head your advice at the moment and just reset the axiom consistency variable back to true after you guys look at this next round of files. My purpose and goal is to try and prove my specification, the states, the operations, etc. to show the validity of the specification before moving on to trying to code from the spec. If the consistency is not that big of an issue and can be looked over without harming the validity of the specification then I will do that, and just assume consistency. Just from rereading page 93 of the tutorial, it made it seem like the consistency proof was very straight forward. All the knowledge learned and gain through this process will be applied to a joint project me and my advisers are working on that is much more complex, but I got to start somewhere and this elevator example has smaller versions of a lot of the material we will see in the more complex project. Thanks, Jon On Fri, Sep 14, 2012 at 10:50 AM, Rob Arthan r...@lemma-one.com wrote: On 14 Sep 2012, at 03:01, Jon Lockhart wrote: Phil, Moving them all to there own paragraph worked great. Now I am up to proving the consistency of the axioms, which is where I am run into my next stumbling block. Got the spec load and the consistency goal using the commands no problem. This generates a sub goal which looks relatively straight forward. It using the there exist symbol at the front of the goal, so my initial assumption is to use the z_there exists_tac, as seen in the provided spec. Unfortunately I can't unzip your attachment to check exactly what you are doing. There is minimal proof support for consistency goals in Z, since very few Z users have expressed much interest in proving consistency. Unfortunately just giving it masterStop is not enough, and I can't feed it a list of masterStop and masterReset. Next thought was there should be some tactic like this that also has list in it, but I can't seem to find one. When you set up the consistency goal for a Z axiomatic description, what you see is a mixture of HOL and Z and the existential quantifier is an HOL quantifier not a Z one. So you would need to use %exists%_tac rather than z_%exists%_tac. If the axiomatic description defines several global variables, the witness you need would be provided as a HOL tuple. As the witnesses for the individual variables are likely to be Z terms, you are already into some not entirely trivial mixed language working. I just tried a Z axiomatic description declaring three integers x, y, and z with defining property x y z 0. Here is the tactic that proves the consistency: a(%exists%_tac %%(%SZT%3%%, %SZT%2%%, %SZT%1%%)%% THEN PC_T1 z_library rewrite_tac[z'decl_def, z'dec_def]); Even when you translate that back into the extended character set (e.g., by pasting the bit between %% and %% into ProofPower), it is not very nice. So on the whole I don't think doing consistency proofs is not a good place to start learning proof in Z, because it will expose too much HOL to you. If you have a strong interest in doing consistency proofs later on, it would actually be quite easy to provide some tools to protect you from the HOL. Finally, there isn't a list flavour of %exists%_tac or z_%exists%_tac. It would be a minor convenience in HOL (where existentials with a list of bound variables are obtained by iterating existential quantifier over a single variable), but MAP_EVERY %exists%_tac does what you want. It is rarely what you want in Z, where you use a binding display as the witness for an existential quantifier that binds several variables and where iterated existential quantification is fairly rare. Regards, Rob. elevatorSpecV5_P1.doc Description: MS-Word document elevatorSpecV5_P1.doc.gz Description: GNU Zip compressed

### Re: [ProofPower] Trying to Prove my Zed Specifications

On 14/09/12 15:50, Rob Arthan wrote: When you set up the consistency goal for a Z axiomatic description, what you see is a mixture of HOL and Z and the existential quantifier is an HOL quantifier not a Z one. So you would need to use %exists%_tac rather than z_%exists%_tac. If the axiomatic description defines several global variables, the witness you need would be provided as a HOL tuple. As the witnesses for the individual variables are likely to be Z terms, you are already into some not entirely trivial mixed language working. I just tried a Z axiomatic description declaring three integers x, y, and z with defining property x y z 0. Here is the tactic that proves the consistency: a(%exists%_tac %%(%SZT%3%%, %SZT%2%%, %SZT%1%%)%% THEN PC_T1 z_library rewrite_tac[z'decl_def, z'dec_def]); This has really confused me! I get a Z existential quantifier for the initial goal. Even when there are generic parameters, I still get a Z existential quantifier, it's just that the witness must be a HOL function. Are you sure you used z_push_consistency goal rather than push_consistency_goal? Perhaps there is a ProofPower issue on some platforms or am I just missing something? A while ago, I had an issue with z_push_consistency_goal where it failed to produce the expected Z statement - I can't remember exactly what went wrong. This issue was that the initial proof step it performs was sensitive to the environment - the proof context, I think. However, I can't reproduce the issue. Phil Even when you translate that back into the extended character set (e.g., by pasting the bit between %% and %% into ProofPower), it is not very nice. So on the whole I don't think doing consistency proofs is not a good place to start learning proof in Z, because it will expose too much HOL to you. If you have a strong interest in doing consistency proofs later on, it would actually be quite easy to provide some tools to protect you from the HOL. Finally, there isn't a list flavour of %exists%_tac or z_%exists%_tac. It would be a minor convenience in HOL (where existentials with a list of bound variables are obtained by iterating existential quantifier over a single variable), but MAP_EVERY %exists%_tac does what you want. It is rarely what you want in Z, where you use a binding display as the witness for an existential quantifier that binds several variables and where iterated existential quantification is fairly rare. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Thanks for the help. I from what you have just said I better understand about the consistency proofs for axioms in ProofPower, and more importantly Zed. I will probably in the future if I have complicated and none trivial axioms to prove, then I will just leave the variable set to true. In most of the specifications I have worked on and currently working on, I have only been uisng axioms as a way to declare global variables and constraints to the system, so that it gives the developer a more constrained box to work in when taking the specification and converting it to code. I will take a look at the axiomatic proof you did and see if I can't use it to help me finish proving the rest of my axioms before I move on to finishing the preconditions of my operations. Thanks, Jon On Fri, Sep 14, 2012 at 1:48 PM, Roger Bishop Jones r...@rbjones.com wrote: On Friday 14 Sep 2012 17:39, Jon Lockhart wrote: First, I find it odd that the zipping is not working when before it was for Phil, and still is for me. I just generated a zip, emailed it to myself, and then unzipped it and got something that looks just fine, exactly what I zipped up. I have though created an ascii version of the document, and have attached on here along with another attempt at zipping the binary file. Let me know if you guys are able to use either of these. The gzipped version is good this time. I now see the beginnings of your consistency proof which was not present in the last version. I have completed the proof. This involved using a Z binding display for the witness (of which the signature is as in the goal and each component is set to True) and rewriting the result with the specification of BOOLEAN, so it is just a one-liner as you would hope. Third, Rob I guess I will head your advice at the moment and just reset the axiom consistency variable back to true after you guys look at this next round of files. My purpose and goal is to try and prove my specification, the states, the operations, etc. to show the validity of the specification before moving on to trying to code from the spec. If the consistency is not that big of an issue and can be looked over without harming the validity of the specification then I will do that, and just assume consistency. Just from rereading page 93 of the tutorial, it made it seem like the consistency proof was very straight forward. I looked back to that passage and I see how it might be misread. There are two stages involved when not working in axiomatic mode. When an axiomatic specification is processed, instead of being asserted as an axiom, it is introduced with a consistency caveat and this modified specification is automatically proven consistent by the system. This consistency proof is trivial. However, to recover the intended theorem the consistency caveat has to be proven true, and in general this may not be trivial. In HOL this too is frequently done automatically (or rather the consistency proof is done automatically before the specification is stored so the caveat is not necessary), but the proofs are more difficult in Z and this is one area in which didn't get much attention in the original development project, and which has never been raised as a priority by ProofPower users since then. So these consistency proofs are not automated. Whether they are hard or difficult depends on the specification whose consistency is at stake. In the case you were attempting, the proof is indeed trivial, you just need to know how to go about it (as described above). (I attach a revised version of your document with the proof fixed). Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On 14/09/12 18:48, Roger Bishop Jones wrote: (I attach a revised version of your document with the proof fixed). In order for z_get_spec to drop the consistency hypothesis, it is necessary to use save_consistency_thm on the resulting theorem. So after the proof you need a line like: save_consistency_thm %SZT%masterStop%% (pop_thm ()); I tend to write such proofs with the following form, for some global variable C: save_consistency_thm %SZT%C%% ( z_push_consistency_thm %SZT%C%%; (* proof steps here *) pop_thm () ); Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, I see what you did there, and that makes since to me know. That is what I was trying to achieve, but I was not getting there. Thanks for clearing that up. Gentlemen, Now I have moved on to trying to do the same thing for masterReset, using the exact same code that Roger has implemented in my spec, but now I am getting an error when I try to push the consistency goal. :) z_get_spec ñmasterReset®; val it = ô (masterStop BOOLEAN ± masterReset BOOLEAN) ± true : THM :) z_push_consistency_goal ñmasterReset®; Exception Fail * Specification of z'masterReset is not of the form: `Consistent (Ì vs[x1,...,xn]·p[x1,...,xn]) ô ...' [z_push_consistency_goal.46007] * raised Is this because the that it has already because it was proven consistent with the masterStop? Thanks, Jon On Fri, Sep 14, 2012 at 2:07 PM, Phil Clayton phil.clay...@lineone.netwrote: On 14/09/12 18:48, Roger Bishop Jones wrote: (I attach a revised version of your document with the proof fixed). In order for z_get_spec to drop the consistency hypothesis, it is necessary to use save_consistency_thm on the resulting theorem. So after the proof you need a line like: save_consistency_thm %SZT%masterStop%% (pop_thm ()); I tend to write such proofs with the following form, for some global variable C: save_consistency_thm %SZT%C%% ( z_push_consistency_thm %SZT%C%%; (* proof steps here *) pop_thm () ); Phil __**_ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com elevatorSpecV5_P1.doc.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Phil, I tried performing the change you prescribed in my ProofPower spec and it fails to parse. I have included the attachment for your reference. Thanks, Jon On Thu, Sep 13, 2012 at 2:38 PM, Jon Lockhart jal...@bucknell.edu wrote: Phil, Attached is an updated version of my spec making the changes you suggested, minus having the changes provided in my natural language description. You were right in that FUZZ does not like using that since it is based off Spivey's Z guide and I don't think he allowed setting Boolean's like you discussed, and would be why when I tried implementing them as described in The Way of Zed the checker failed. However CZT, which is built on the Z Standard, does allow for it, so I am perfectly good there. CZT is a stricter type checker anyways. So I will go and get those changes made in my ProofPower version as well. Thanks for the info on the axiom checking and the patch. I did find that page, which I had remembered reading, and I will start there in trying to check my axioms. I will continue to move forward and there should probably be more emails from me here in the short term, as even with all that I have learned from the tutorials I am still learning, as there is a lot to ProofPower. Regards, Jon On Thu, Sep 13, 2012 at 9:05 AM, Phil Clayton phil.clay...@lineone.netwrote: Jon, On 13/09/12 04:16, Jon Lockhart wrote: Are you saying then for the Boolean block I have to just replace it with the one that you have provided in the email? Not only would you have to replace the Boolean block but also remove the integer comparison around the references to Boolean global variables. For example, the predicate masterStop = 0 must be changed to either ¬ masterStop or masterStop = False Seems odd to be to just through True and False in there like that where I am describing sets but if it works, then I am all for it, I just need to see or understand how to use it properly. To use this is very simple for the most part. In a predicate context, just treat Boolean expressions as though they were predicates. In an expression context, Boolean expressions can be combined to give other Boolean expressions as you would expect, e.g. a ∧ b. However, to create a Boolean expression from a predicate p, you need to write [ | p] It is probably worth understanding what is going on at least once. It is easiest to think in terms of sets. A schema is just a set of bindings. The empty schema [], which is the same as [ | true], is a set containing just the empty binding, i.e. {()}. So [] is much like the SML type 'unit', a type that has only one value. Thus Boolean is the set {{}, {()}} where {} represents false and {()} represents true, hence our definition of True and False. So an expression of type Boolean is a schema. When a schema S is used as a predicate, the predicate is θS ∈ S. For one of our Boolean expressions B as a predicate, the predicate is θB ∈ B which is equivalent to () ∈ B. So you can see how the corresponding predicate is derived. As for the version of ProofPower, I have version 2.9.1w2, which is what you were saying does not support ==. Looks like I might have to update here when the latest stable version is released on the site. If you feel inclined to try the latest patch, it is here, with instructions: http://www.lemma-one.com/**ProofPower/patches/patches.**htmlhttp://www.lemma-one.com/ProofPower/patches/patches.html I'm fairly familiar with the installation process, so it only takes me a few minutes to build a patched version. However, a new release may be around the corner - I don't know what Rob's plans are there. What I was saying on the masterStop / masterReset axiom, along with the minNumberFloors, maxNumberFloors, etc axioms, since I am using those as global variables essentially, is how do I prove them and preconditions on them like I have down for my States so far? Is is necessary too, or if I just get the spec of them they are already shown to be theorems? I see what you mean. Yes, for an axiomatic description, one wants to be sure that it is not introducing a contradiction into the theory, making the theory inconsistent. ProofPower has a mode of operation where it does not assume such axioms are consistent until they have been proved consistent. This works by showing that each axiom is a conservative extension to the theory, i.e. does not introduce an inconsistency. For Z, at the start of your theory, you would do set_flag (z_use_axioms, false); Note, then, that z_get_spec does not simply give you the axiom as a theorem. After an axiomatic description paragraph, start a consistency proof with e.g. z_push_consistency_goal %SZT%minNumberFloors%%; See section 5.3, page 93, of usr011.dvi for examples. Phil __**_ Proofpower mailing list Proofpower@lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On 13/09/12 21:32, Jon Lockhart wrote: I tried performing the change you prescribed in my ProofPower spec and it fails to parse. I have included the attachment for your reference. I think the attachment has a strange compression format or has been corrupted - gunzip reports unexpected end of file. I managed to extract enough by renaming to .xz and extracting with 7za though. (How did you create the .gz file?) The issue is that there can only be one abbreviation definition per paragraph. You can't lump BOOLEAN, True and False all together into one paragraph. Apologies if I misled you with my email presentation. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Phil, I see now, I did not know that. You can lump them together in the Word document when I am using those tools but that is b/c when it is parsed each is separated into its own paragraph on the back end. I will be sure to correct that and see where I can get from there. Thanks for the help. As for the zipped file I used the gzip command, which is short for gunzip. Was the first couple I sent you corrupted? Thanks, Jon On Thu, Sep 13, 2012 at 6:25 PM, Phil Clayton phil.clay...@lineone.netwrote: On 13/09/12 21:32, Jon Lockhart wrote: I tried performing the change you prescribed in my ProofPower spec and it fails to parse. I have included the attachment for your reference. I think the attachment has a strange compression format or has been corrupted - gunzip reports unexpected end of file. I managed to extract enough by renaming to .xz and extracting with 7za though. (How did you create the .gz file?) The issue is that there can only be one abbreviation definition per paragraph. You can't lump BOOLEAN, True and False all together into one paragraph. Apologies if I misled you with my email presentation. Phil __**_ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On 13/09/12 23:48, Jon Lockhart wrote: I see now, I did not know that. You can lump them together in the Word document when I am using those tools but that is b/c when it is parsed each is separated into its own paragraph on the back end. I will be sure to correct that and see where I can get from there. Thanks for the help. You're welcome. By the way, I don't think any dialect of Z allows multiple horizontal definitions in one paragraph. As for the zipped file I used the gzip command, which is short for gunzip. Was the first couple I sent you corrupted? No, all the other GZ attachments have been fine - it must have been corrupted somewhere. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On 13/09/12 00:24, Jon Lockhart wrote: Unfortunately the two extra sets I want to declare and add to the spec are causing parser errors in ProofPower. The sets I am trying to declare are TIMER == 0..5 and BOOLEAN == {0, 1} which is allowed in the normal standard and has been syntactically cleared by FUZZ and CZT through Anthony's Z Word Tools. Unfortunately ProofPower doesn't allow me to do such a thing and I am wondering what would be the proper protocol for adding such sets to a specification in ProofPower. These work in the version I have, 2.9.1w2.rda.120805, the latest patch which fixes the recent Xpp issue. (Generally it would be useful to see the error message you get.) ProofPower used to require ≜ (hat-equals) for an abbreviation definition but a recent patch allows the standard == to be used. If you are using the 'current release' 2.9.1w2, == is not supported. Can you check the version of ProofPower in the banner that is shown when it starts? My second question derives from this where right after the sets I list some axioms which are used to hold globals which I use in operations throughout the rest of my specification. They rely on the boolean set I just created or are just parameters for the sets in general. How would one go about proofing these or is it even necessary? I'm not sure I understand the question. The axiomatic description involving masterStop and masterReset is referring to the global variable BOOLEAN that was defined to be 0 .. 5 earlier. The constraint holds throughout the theory and is obtained as a theorem by z_get_spec %SZT%masterStop%% Phil P.S. A better way to define booleans in Z is as follows: BOOLEAN == ℙ [] True == [ | true] False == [ | false] This is standard Z. I don't know whether FuZZ accepts empty schemas. The main advantage is that the usual logical connectives can be used with such boolean expressions and the implicit conversion of schemas as predicates allows such a boolean expressions to be used where a predicate is required, and giving the expected predicate value. The specification is more readable as a result. For example, your expression if (elevatorRightHeading? = 1 ∧ elevatorGoingToFloor? = 1) then ... could just be if elevatorRightHeading? ∧ elevatorGoingToFloor? then ... To negate a value one can write ¬ elevatorRightHeading? rather than encouraging numerical tricks like (1 - elevatorRightHeading?) Note also that [] is a maximal set, so ℙ [] is too. Consequently type checking ensures that such boolean values can take no other values. Using BOOLEAN == {0, 1}, the constraint is a semantic one: type checking will not reject e.g. elevatorRightHeading? = 2 which, presumably, would be a mistake. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On 13/09/12 02:47, Phil Clayton wrote: BOOLEAN that was defined to be 0 .. 5 I meant to say {0, 1}, of course! ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Phil, Are you saying then for the Boolean block I have to just replace it with the one that you have provided in the email? Seems odd to be to just through True and False in there like that where I am describing sets but if it works, then I am all for it, I just need to see or understand how to use it properly. As for the version of ProofPower, I have version 2.9.1w2, which is what you were saying does not support ==. Looks like I might have to update here when the latest stable version is released on the site. What I was saying on the masterStop / masterReset axiom, along with the minNumberFloors, maxNumberFloors, etc axioms, since I am using those as global variables essentially, is how do I prove them and preconditions on them like I have down for my States so far? Is is necessary too, or if I just get the spec of them they are already shown to be theorems? Thanks, Jon Lockhart On Wed, Sep 12, 2012 at 9:53 PM, Phil Clayton phil.clay...@lineone.netwrote: On 13/09/12 02:47, Phil Clayton wrote: BOOLEAN that was defined to be 0 .. 5 I meant to say {0, 1}, of course! __**_ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On Monday 03 Sep 2012 21:03, Jon Lockhart wrote: Most of the tactics return the exact same goal and the comment printed with the goal is that it is alpha-convertible to its goal. The significance of this is simply that the proof step you have just done has not moved you forward. i.e. it says that what you ended up with is essentially the same as what you started with. I am assuming it is saying that this subgoal is alpha-convertible to the main goal I am trying to prove. Just the alpha-equivalent to the goal or subgoal from which it was obtained. Now I looked at the reference manual and there appears to be some commands that I can use to eliminate alpha-convertible components and that this is what I should use for simplifying the sub goal and thus proving it and the main goal. No this is a red herring. You are not reasoning from your subgoal to the main goal. You have to prove the subgoal independently of the main goal, and when you have proved them all you have a proved the main goal. So based on the scenario above and where I am at does anyone have any suggestions on what commands I should use to handle the alpha-conversion and completing the proof of the subgoal? Normally you would not need to do anything about alpha conversion, if you were within alpha conversion of the target then the system would sort that out for you automatically. So your problem here is that you have misunderstood the significance of the alpha conversion message. Forget about alpha conversion. No-one can help you at this point, because we don't know anything at all about what you are trying to prove. If you want help you should show us the problem you are working on. Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, Can you post the actual input that is failing, please. (To protect it in transit, either gzip your .doc file and attach it to your post, or use conv_ascii to convert it into ASCII). Regards, Rob. Regards, Rob. On 3 Sep 2012, at 01:47, Jon Lockhart wrote: Phil, Thanks for the reply. I have set it so up like that where the parent theory is z_library and my new theory is named something else. Just ran the print status again and that is what it says as well. Could it be one more minor thing is not loaded? Regards, Jon On Sep 2, 2012 8:43 PM, Phil Clayton phil.clay...@lineone.net wrote: Hi John, On 02/09/12 23:59, Jon Lockhart wrote: The problem I am having is this. I am trying to use the union operator in my specification. More specifically I am trying to and a individual item to a set in the predicate of a specification paragraph in z, which is allowed by the rules of the language. The PP system comes back with expection 62000 of the Z-Parser, saying that the union symbol from the palette is a free variable and those are not permitted in Z paragraphs. If ProofPower says that ∪ is a variable then the Z toolkit theory z_sets that defines the Z global variable (_ ∪ _) is not in scope, i.e. z_sets is not an ancestor theory of your current theory. Generally, Z specifications should always have the theory z_library as an ancestor, which brings all Z toolkit theories into scope. Typically your theory would start open_theory z_library; new_theory some_new_theory; ... If you need other theories in scope, add them as parents e.g. new_parent z_reals; Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Phil, After resetting the command window and rerunning the commands today, I was able to run my specification to the point where I was running into the exception with no problems. I must of somehow changed the proof context I guess, though the print status was coming up that is was ok. Not sure, but it was probably on my typing in a command wrong. Thanks for the help. I am sure I will be back with more questions today as I try to prove portions of my specification. Regards, Jon On Sun, Sep 2, 2012 at 9:00 PM, Phil Clayton phil.clay...@lineone.netwrote: Hi John, That sounds strange. It's probably easiest if you can cut your example down to a short script that produces the error, say containing just a single paragraph, and send a zipped version of that to the list. Phil On 03/09/12 01:47, Jon Lockhart wrote: Phil, Thanks for the reply. I have set it so up like that where the parent theory is z_library and my new theory is named something else. Just ran the print status again and that is what it says as well. Could it be one more minor thing is not loaded? Regards, Jon On Sep 2, 2012 8:43 PM, Phil Clayton phil.clay...@lineone.net mailto:phil.clayton@lineone.**net phil.clay...@lineone.net wrote: Hi John, On 02/09/12 23:59, Jon Lockhart wrote: The problem I am having is this. I am trying to use the union operator in my specification. More specifically I am trying to and a individual item to a set in the predicate of a specification paragraph in z, which is allowed by the rules of the language. The PP system comes back with expection 62000 of the Z-Parser, saying that the union symbol from the palette is a free variable and those are not permitted in Z paragraphs. If ProofPower says that ∪ is a variable then the Z toolkit theory z_sets that defines the Z global variable (_ ∪ _) is not in scope, i.e. z_sets is not an ancestor theory of your current theory. Generally, Z specifications should always have the theory z_library as an ancestor, which brings all Z toolkit theories into scope. Typically your theory would start open_theory z_library; new_theory some_new_theory; ... If you need other theories in scope, add them as parents e.g. new_parent z_reals; Phil __**_ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Hey Guys, So I got an actual proof question this time, and I can't seem to find any that I can use successfully from the reference document to solve my current question. I am currently trying to prove some statements about my specification, and in this case I am working on trying to prove the preconditions of one of the portions of the spec. After setting the goal and dong *a (rewrite_tac (map z_get_spec* spec I want to use*)); *and doing *a (REPEAT z_stip_tac); *I was given three subgoals to prove. I have gotten the first two using just *a (asm_prove_tac []);* but the last one none of the tactics seem to work for. Most of the tactics return the exact same goal and the comment printed with the goal is that it is alpha-convertible to its goal. I am assuming it is saying that this subgoal is alpha-convertible to the main goal I am trying to prove. Now I looked at the reference manual and there appears to be some commands that I can use to eliminate alpha-convertible components and that this is what I should use for simplifying the sub goal and thus proving it and the main goal. Unfortunately I can't seem to get to any of the commands working with Goals, i.e. I am having trouble accessing the goals to use them. So based on the scenario above and where I am at does anyone have any suggestions on what commands I should use to handle the alpha-conversion and completing the proof of the subgoal? Thanks, Jon On Mon, Sep 3, 2012 at 2:55 PM, Jon Lockhart jal...@bucknell.edu wrote: Phil, After resetting the command window and rerunning the commands today, I was able to run my specification to the point where I was running into the exception with no problems. I must of somehow changed the proof context I guess, though the print status was coming up that is was ok. Not sure, but it was probably on my typing in a command wrong. Thanks for the help. I am sure I will be back with more questions today as I try to prove portions of my specification. Regards, Jon On Sun, Sep 2, 2012 at 9:00 PM, Phil Clayton phil.clay...@lineone.netwrote: Hi John, That sounds strange. It's probably easiest if you can cut your example down to a short script that produces the error, say containing just a single paragraph, and send a zipped version of that to the list. Phil On 03/09/12 01:47, Jon Lockhart wrote: Phil, Thanks for the reply. I have set it so up like that where the parent theory is z_library and my new theory is named something else. Just ran the print status again and that is what it says as well. Could it be one more minor thing is not loaded? Regards, Jon On Sep 2, 2012 8:43 PM, Phil Clayton phil.clay...@lineone.net mailto:phil.clayton@lineone.**net phil.clay...@lineone.net wrote: Hi John, On 02/09/12 23:59, Jon Lockhart wrote: The problem I am having is this. I am trying to use the union operator in my specification. More specifically I am trying to and a individual item to a set in the predicate of a specification paragraph in z, which is allowed by the rules of the language. The PP system comes back with expection 62000 of the Z-Parser, saying that the union symbol from the palette is a free variable and those are not permitted in Z paragraphs. If ProofPower says that ∪ is a variable then the Z toolkit theory z_sets that defines the Z global variable (_ ∪ _) is not in scope, i.e. z_sets is not an ancestor theory of your current theory. Generally, Z specifications should always have the theory z_library as an ancestor, which brings all Z toolkit theories into scope. Typically your theory would start open_theory z_library; new_theory some_new_theory; ... If you need other theories in scope, add them as parents e.g. new_parent z_reals; Phil __**_ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Hi John, On 02/09/12 23:59, Jon Lockhart wrote: The problem I am having is this. I am trying to use the union operator in my specification. More specifically I am trying to and a individual item to a set in the predicate of a specification paragraph in z, which is allowed by the rules of the language. The PP system comes back with expection 62000 of the Z-Parser, saying that the union symbol from the palette is a free variable and those are not permitted in Z paragraphs. If ProofPower says that ∪ is a variable then the Z toolkit theory z_sets that defines the Z global variable (_ ∪ _) is not in scope, i.e. z_sets is not an ancestor theory of your current theory. Generally, Z specifications should always have the theory z_library as an ancestor, which brings all Z toolkit theories into scope. Typically your theory would start open_theory z_library; new_theory some_new_theory; ... If you need other theories in scope, add them as parents e.g. new_parent z_reals; Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Phil, Thanks for the reply. I have set it so up like that where the parent theory is z_library and my new theory is named something else. Just ran the print status again and that is what it says as well. Could it be one more minor thing is not loaded? Regards, Jon On Sep 2, 2012 8:43 PM, Phil Clayton phil.clay...@lineone.net wrote: Hi John, On 02/09/12 23:59, Jon Lockhart wrote: The problem I am having is this. I am trying to use the union operator in my specification. More specifically I am trying to and a individual item to a set in the predicate of a specification paragraph in z, which is allowed by the rules of the language. The PP system comes back with expection 62000 of the Z-Parser, saying that the union symbol from the palette is a free variable and those are not permitted in Z paragraphs. If ProofPower says that ∪ is a variable then the Z toolkit theory z_sets that defines the Z global variable (_ ∪ _) is not in scope, i.e. z_sets is not an ancestor theory of your current theory. Generally, Z specifications should always have the theory z_library as an ancestor, which brings all Z toolkit theories into scope. Typically your theory would start open_theory z_library; new_theory some_new_theory; ... If you need other theories in scope, add them as parents e.g. new_parent z_reals; Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Hi John, That sounds strange. It's probably easiest if you can cut your example down to a short script that produces the error, say containing just a single paragraph, and send a zipped version of that to the list. Phil On 03/09/12 01:47, Jon Lockhart wrote: Phil, Thanks for the reply. I have set it so up like that where the parent theory is z_library and my new theory is named something else. Just ran the print status again and that is what it says as well. Could it be one more minor thing is not loaded? Regards, Jon On Sep 2, 2012 8:43 PM, Phil Clayton phil.clay...@lineone.net mailto:phil.clay...@lineone.net wrote: Hi John, On 02/09/12 23:59, Jon Lockhart wrote: The problem I am having is this. I am trying to use the union operator in my specification. More specifically I am trying to and a individual item to a set in the predicate of a specification paragraph in z, which is allowed by the rules of the language. The PP system comes back with expection 62000 of the Z-Parser, saying that the union symbol from the palette is a free variable and those are not permitted in Z paragraphs. If ProofPower says that ∪ is a variable then the Z toolkit theory z_sets that defines the Z global variable (_ ∪ _) is not in scope, i.e. z_sets is not an ancestor theory of your current theory. Generally, Z specifications should always have the theory z_library as an ancestor, which brings all Z toolkit theories into scope. Typically your theory would start open_theory z_library; new_theory some_new_theory; ... If you need other theories in scope, add them as parents e.g. new_parent z_reals; Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Phil, Ok, let me try to restart and reload the system and see if that corrects it. If not then i will do as you say and send it out. You guys may have it though. I am currently using Anthony's example that came with ZWordTools bc it is simple and great for trying to get a handle on the tools. Thanks, Jon On Sep 2, 2012 9:00 PM, Phil Clayton phil.clay...@lineone.net wrote: Hi John, That sounds strange. It's probably easiest if you can cut your example down to a short script that produces the error, say containing just a single paragraph, and send a zipped version of that to the list. Phil On 03/09/12 01:47, Jon Lockhart wrote: Phil, Thanks for the reply. I have set it so up like that where the parent theory is z_library and my new theory is named something else. Just ran the print status again and that is what it says as well. Could it be one more minor thing is not loaded? Regards, Jon On Sep 2, 2012 8:43 PM, Phil Clayton phil.clay...@lineone.net mailto:phil.clayton@lineone.**net phil.clay...@lineone.net wrote: Hi John, On 02/09/12 23:59, Jon Lockhart wrote: The problem I am having is this. I am trying to use the union operator in my specification. More specifically I am trying to and a individual item to a set in the predicate of a specification paragraph in z, which is allowed by the rules of the language. The PP system comes back with expection 62000 of the Z-Parser, saying that the union symbol from the palette is a free variable and those are not permitted in Z paragraphs. If ProofPower says that ∪ is a variable then the Z toolkit theory z_sets that defines the Z global variable (_ ∪ _) is not in scope, i.e. z_sets is not an ancestor theory of your current theory. Generally, Z specifications should always have the theory z_library as an ancestor, which brings all Z toolkit theories into scope. Typically your theory would start open_theory z_library; new_theory some_new_theory; ... If you need other theories in scope, add them as parents e.g. new_parent z_reals; Phil __**_ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**comhttp://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On Saturday 25 Aug 2012 20:47, Jon Lockhart wrote: I did have a question on some of the outputs from the tutorial document. Currently I am on user013C and when I have placed some of the commands into the terminal, via the execute line command, the ProofPower output is not the same as is reported in the document. Is this due to some changes that have been made since this document was published in 2002? Also a few of the rewrite commands that were in the document threw exceptions. On my system usr013A-C all load OK (in fact if they didn't the build would have failed since I think they are loaded in creating the examples database). That is to say, if you start with a clean HOL database and do docsml on each of usr013A-C and then load file on each, they go through fine. So the possible reasons for your failures are: 1. You are starting with the wrong database or 2. you are copy and pasting something for which some prior script is essential but has not been executed. or 3. you are trying to execute something which is in the document for explanation but is not there to be executed in that context. (e.g. something in a GFT section rather than an SML section). If you can't figure it out from that then you will need to post exactly what you have done and what the result was. Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Dear All I've just got back from holiday (yes, thank you :-) ) and have been reading the discussion of ProofPower/Z Word Tools with interest. As Rob said, we have been discussing whether and how to integrate the two tools, and we did agree that a first step was to make PP work with Unicode. ZWT emits Unicode when set to typecheck with CZT, and yes it does allow things like Greek characters in names. We then discussed two levels of integration. The simplest would be a sort of batch integration, similar to the way that ZWT works with fuzz or CZT: it would simply hand the whole Unicode file over to PP to analyse using some sort of potted instruction. This would undoubtedly be the simplest way to get started, but is not really how PP is meant to work. Much better would be a tighter integration where ZWT was able to interactively pass selected parts of the spec to PP and return the results to Word. This is technically possible but quite a lot of work to do. Essentially this would mean that the Word document would be the master specification + proof and ZWT would be the UI to PP. Whichever way we do this there remains the question of the different dialects of Z accepted by PP, fuzz and CZT. In one sense this may not be much of a problem: for example requiring the user to have semicolons at the end of each line would not stop a specification going through either typechecker (although relying on newlines NOT terminating declarations obviously would be problematic). Even if the dialect were inconsistent with a typechecker, ZWT itself wouldn't mind as long as the lexis was consistent - the only likely problem here is that ZWT doesn't distinguish the different types of unboxed paragraph eg given sets vs free types. Overall I doubt whether this is really a huge issue. So, Rob, it sounds as if we ought to resurrect our discussions. What do you think? Incidentally, there is a stable development version of ZWT that is not yet released. Its main relevance is that it supports named theorem paras within the Z standard (as interpreted by CZT - the standard is a bit of a mess in this area). It also has a tool for converting from Spivey to Standard Z. I could release it but am working on a couple of other things as well. One is a more robust way of delimiting the Z so it's harder to break the document structure (or easier not to break it); the other is the perpetual Red Queen race to see if the tools will work with Office 2013 or Office 365 or whatever it is called this month. Anthony -Original Message- From: proofpower-boun...@lemma-one.com [mailto:proofpower-boun...@lemma-one.com] On Behalf Of Rob Arthan Sent: 13 August 2012 18:13 To: Jon Lockhart Cc: ProofPower List Subject: Re: [ProofPower] Trying to Prove my Zed Specifications On 13 Aug 2012, at 12:05, Jon Lockhart wrote: Gentlemen, I apologize I should of been more specific at the tasks that I was trying to accomplish and in describing where I am at so far. It seems the first point of business though from what Rob is saying is actually getting the specifications into the ProofPower environment, which at this point sounds like it needs to be done by hand, but I will explain it more closely Rob. That way you can tell me if I got a shot of importing them or if I am going to have to do a hand rewrite. So as you mentioned Rob, I am using Anthony's Z Word Tools for Word and I have written all my specifications in there so far. It is a fabulous writing tool, interfacing so well with Word, and providing all the structure I need to write the specifications I am working on. Now, I am not sure if you are aware of this, but the latest version of the Z Word Tools no longer requires an export of the specification to be used with FUZZ or CZT, those checkers are built right into the tool now and allow for typechecking of the specification as you are writing it, using either checker I think you will find that Z Word Tools is actually extracting the Z into a file and running Fuzz or CZT for you, so it feels like the typechecker is built in. You will find that the menu you use to do the typechecking has an item on it to export the Z as a file. Now of course, neither of these checkers run on .doc / .docx format files, and there are a whole host of other files generated when you save or run a check, including a LaTeX file of the specification. I was wondering if you thought this LaTeX file would be possible to import into the ProofPower system, or does it have to be in a special format of .tex to be of any use? I actually thought that the CZT unicode format might be a bit closer to what my prototype tools for dealing with UTF-8 can cope with. If you only have a few pages of Z to start with, then it will probably be quicker just to reenter it manually. If you have more it may be worth trying to cobble together something semi-automated. We should be able to do something much slicker in the slightly longer term. I have attached one of the specifications

### Re: [ProofPower] Trying to Prove my Zed Specifications

Rob, Thanks for the fix that really did the trick. I believe the database is saving and I have full access to the XPP tool bar and editing, including restarting the execution window. I did have a question on some of the outputs from the tutorial document. Currently I am on user013C and when I have placed some of the commands into the terminal, via the execute line command, the ProofPower output is not the same as is reported in the document. Is this due to some changes that have been made since this document was published in 2002? Also a few of the rewrite commands that were in the document threw exceptions. Thanks, Jon On Wed, Aug 22, 2012 at 5:22 PM, Rob Arthan r...@lemma-one.com wrote: On 18 Aug 2012, at 22:14, Jon Lockhart wrote: Rob, I got a trouble shooting question for you. Been going through the learning documentation this weekend, currently still on the first tutorial wanting to make sure I soak it all in before moving to HOL and Z, but I seem to be running into a problem with one of the commands. Every time I try to use the save_and_quit() ML command in the execution Window the whole system freezes up. Thanks to Jon for pointing this out and proviing further details. I now have a fix for this problem, whereby what caused a busy wait on some operating systems will actually stop xpp responding to the user on a recent Debian release. I have attached a patch which should work on any version downloaded in the last 18 months or so. To use the patch, copy it into /tmp say, then go to your ProofPower build directory (where config and install live) and do: gunzip -c /tmp/patch-2.9.1w2.rda.120821.gz | patch -p1 -b -B orig/ then do: PPTARGETS=xpp ./configure ./install -d Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On 18 Aug 2012, at 22:14, Jon Lockhart wrote: Rob, I got a trouble shooting question for you. Been going through the learning documentation this weekend, currently still on the first tutorial wanting to make sure I soak it all in before moving to HOL and Z, but I seem to be running into a problem with one of the commands. Every time I try to use the save_and_quit() ML command in the execution Window the whole system freezes up. Thanks to Jon for pointing this out and proviing further details. I now have a fix for this problem, whereby what caused a busy wait on some operating systems will actually stop xpp responding to the user on a recent Debian release. I have attached a patch which should work on any version downloaded in the last 18 months or so. To use the patch, copy it into /tmp say, then go to your ProofPower build directory (where config and install live) and do: gunzip -c /tmp/patch-2.9.1w2.rda.120821.gz | patch -p1 -b -B orig/ then do: PPTARGETS=xpp ./configure ./install -d Regards, Rob. patch-2.9.1w2.rda.120821.gz Description: GNU Zip compressed data ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On 19 Aug 2012, at 20:51, Jon Lockhart wrote: Roger, Yes, the xpp interface locks. The command executes and then I can't access any of the taps in the journal window, the ML command line will not close, nor can I use the palette I have open either. My first guess is that a dialogue window that has popped up but is hidden behind one of the other windows. Are you able to slide the windows around to look for such a thing? If this is the case, then please let me know what Linux distribution and desktop you are using and I will try to find out why the window manager isn't getting the stacking ordering right. If that isn't the problem, then we need to find where xpp is hanging. To do this, first install gdb if you don't already have it. Then reproduce the problem and find out the process id for the xpp process and do: gdb ProofPower Installation Directory/bin/xpp process id and then when gdb gives you its prompt, type where. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Rob, I have run into something interesting. None of the buttons work in the window, just as File, Edit, etc, nor do the buttons for closing, maximizing the window, etc., but I am able to move the window around no problem. I have moved the window everywhere, there is no other window around, so that rules out that. I also looked at the process id list to see if there was anything besides the one xpp, and there is not, so there is just the one running. I will try and get this gdb installed on my Debian imaged and get back to you. Thanks, Jon On Mon, Aug 20, 2012 at 1:01 PM, Rob Arthan r...@lemma-one.com wrote: Jon, On 19 Aug 2012, at 20:51, Jon Lockhart wrote: Roger, Yes, the xpp interface locks. The command executes and then I can't access any of the taps in the journal window, the ML command line will not close, nor can I use the palette I have open either. My first guess is that a dialogue window that has popped up but is hidden behind one of the other windows. Are you able to slide the windows around to look for such a thing? If this is the case, then please let me know what Linux distribution and desktop you are using and I will try to find out why the window manager isn't getting the stacking ordering right. If that isn't the problem, then we need to find where xpp is hanging. To do this, first install gdb if you don't already have it. Then reproduce the problem and find out the process id for the xpp process and do: gdb ProofPower Installation Directory/bin/xpp process id and then when gdb gives you its prompt, type where. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, Thanks. This looks like a very strange race condition. Do you get the same problem if you do Kill from the Command Menu or just quit xpp from the File Menu rather than run the save_and_quit command? If not, then a possible work-around is just not to use quit or save_and_quit. Regards, Rob. On 20 Aug 2012, at 20:17, Jon Lockhart wrote: Rob, Got it installed and this is what was reported when where was run. (gdb) where #0 0x7f1cfb516720 in __read_nocancel () at ../sysdeps/unix/syscall-template.S:82 #1 0x004117e3 in get_from_application (unused_p=0x0, unused_source=0x168f8a8, unused_id=0x7fff12456e68) at pterm.c:829 #2 0x7f1cfc171844 in XtAppProcessEvent () from /usr/lib/x86_64-linux-gnu/libXt.so.6 #3 0x7f1cfc1661dd in XtAppMainLoop () from /usr/lib/x86_64-linux-gnu/libXt.so.6 #4 0x0040c507 in main_window_go ( file_name=0x7fff12457535 ../zed/pp/doc/usr004.doc) at mainw.c:2111 #5 0x0041a3fe in main (argc=6, argv=0x7fff124570f8) at xpp.c:670 Thanks, Jon On Mon, Aug 20, 2012 at 3:11 PM, Jon Lockhart jal...@bucknell.edu wrote: Rob, I have run into something interesting. None of the buttons work in the window, just as File, Edit, etc, nor do the buttons for closing, maximizing the window, etc., but I am able to move the window around no problem. I have moved the window everywhere, there is no other window around, so that rules out that. I also looked at the process id list to see if there was anything besides the one xpp, and there is not, so there is just the one running. I will try and get this gdb installed on my Debian imaged and get back to you. Thanks, Jon On Mon, Aug 20, 2012 at 1:01 PM, Rob Arthan r...@lemma-one.com wrote: Jon, On 19 Aug 2012, at 20:51, Jon Lockhart wrote: Roger, Yes, the xpp interface locks. The command executes and then I can't access any of the taps in the journal window, the ML command line will not close, nor can I use the palette I have open either. My first guess is that a dialogue window that has popped up but is hidden behind one of the other windows. Are you able to slide the windows around to look for such a thing? If this is the case, then please let me know what Linux distribution and desktop you are using and I will try to find out why the window manager isn't getting the stacking ordering right. If that isn't the problem, then we need to find where xpp is hanging. To do this, first install gdb if you don't already have it. Then reproduce the problem and find out the process id for the xpp process and do: gdb ProofPower Installation Directory/bin/xpp process id and then when gdb gives you its prompt, type where. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, You are right that Rob is the man to answer your technical problem, but in the meantime I might be able to help you round it. save_and_quit(); is something that I never use. If your system otherwise seems OK then you should go right ahead and work through the tutorial. Why don't I use it? Well, whenever I am working interactively with ProofPower I just don't save the database. I always have a make system in the background ready to build in batch mode, and this uses proofpower with the -f option to run a script and then save it. So when I have a working script I create a new database using make. This must be possible with your system otherwise you would not have completed the build of ProofPower. When I resume work on an incomplete development I will enter the current document with xpp picking the database with all prior documents loaded, and then I use use_file to run the current script through to the point of failure where I was last working (and I force failure by just putting stop; in the script at the point I am working). Then I continue my interactive work. When I have a clean document I save it and then do a make to create a new database. You probably don't want to set up a makefile for working through the tutorial, but you can still work in a similar manner, i.e. instead of saving the database when you pause in the tutorial, just put stop here; in your script, save it, and quit xpp. When you come back use use_file to run your script through to your current position in the tutorial. (you will need to use docsml on the file first if it is not pure SML, but for the tutorial you can just work with an SML script). I presume you are looking at usr004, which is the gentlest introduction to ProofPower-HOL. Alternatively you could work through the ProofPower HOL course usr022 with its accompanying tutorial notes usr013, which is less gentle but I think, more systematic and has greater coverage (but doesn't actually mention save_and_quit()) Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On 18 Aug 2012, at 22:14, Jon Lockhart wrote: Rob, I got a trouble shooting question for you. Been going through the learning documentation this weekend, currently still on the first tutorial wanting to make sure I soak it all in before moving to HOL and Z, but I seem to be running into a problem with one of the commands. Every time I try to use the save_and_quit() ML command in the execution Window the whole system freezes up. There is no error being thrown, it just returns val it = (): TYPE, and then locks up. Have to either kill all the window proc id's or restart the system to get rid of them. Mostly it is restarting b/c kill sometimes will not remove them for some reason. I was working on the Peanissimo theory write up. Written it several times and get the lock up every time, any suggestions on trouble shooting? Are you saying that the xpp user interface locks up? If so that definitely shouldn't be happening. The ProofPower-ML session running in the xpp journal window should finish, but the xpp menus and so on should work as normal. Is that not what is happening? Aside: the source of this tutorial is in usr004.doc in the doc directory, so you don't need to type it in yourself. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Roger, Thanks I will look into the the make set up for when I am working on my own specifications and databases. Rob, Yes, the xpp interface locks. The command executes and then I can't access any of the taps in the journal window, the ML command line will not close, nor can I use the palette I have open either. Thanks, Jon On Sun, Aug 19, 2012 at 9:10 AM, Rob Arthan r...@lemma-one.com wrote: Jon, On 18 Aug 2012, at 22:14, Jon Lockhart wrote: Rob, I got a trouble shooting question for you. Been going through the learning documentation this weekend, currently still on the first tutorial wanting to make sure I soak it all in before moving to HOL and Z, but I seem to be running into a problem with one of the commands. Every time I try to use the save_and_quit() ML command in the execution Window the whole system freezes up. There is no error being thrown, it just returns val it = (): TYPE, and then locks up. Have to either kill all the window proc id's or restart the system to get rid of them. Mostly it is restarting b/c kill sometimes will not remove them for some reason. I was working on the Peanissimo theory write up. Written it several times and get the lock up every time, any suggestions on trouble shooting? Are you saying that the xpp user interface locks up? If so that definitely shouldn't be happening. The ProofPower-ML session running in the xpp journal window should finish, but the xpp menus and so on should work as normal. Is that not what is happening? Aside: the source of this tutorial is in usr004.doc in the doc directory, so you don't need to type it in yourself. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Rob, I got a trouble shooting question for you. Been going through the learning documentation this weekend, currently still on the first tutorial wanting to make sure I soak it all in before moving to HOL and Z, but I seem to be running into a problem with one of the commands. Every time I try to use the save_and_quit() ML command in the execution Window the whole system freezes up. There is no error being thrown, it just returns val it = (): TYPE, and then locks up. Have to either kill all the window proc id's or restart the system to get rid of them. Mostly it is restarting b/c kill sometimes will not remove them for some reason. I was working on the Peanissimo theory write up. Written it several times and get the lock up every time, any suggestions on trouble shooting? Thanks, Jon On Mon, Aug 13, 2012 at 3:44 PM, Rob Arthan r...@lemma-one.com wrote: On 13 Aug 2012, at 13:31, Jon Lockhart wrote: Rob, Ok so looks like I am looking to rewrite all my specifications again in ProofPower. A minor inconvenience but should not be a problem. That is likely the quickest way to get started. I will just pop up my specs on one screen and bring up ProofPower's XPP up on the other screen in my Linux VM, and I should be able to rewrite them with no problems. The only thing I can't seem to find is the symbol library in XPP. I have found where I can insert the various Zed structures, no problem, but there is supposed to be an XPP keyboard that has these symbols, based on the pictures in the documentation. Is this available in the editor version of XPP or do I need to run the full version of XPP to have access to that? The keyboard in the picture is the actual keyboard, although you may need to do a bit more work to set it up. There is a tool called the Palette in the Tools menu that lets you enter all the symbols with mouse clicks without having to do any more set-up and without having to learn the key combinations. If you do want to set up the keyboard have a read of section 4.3 of the Xpp manual and the comments at the head of the file app-defaults/XppKeyboard in the first instance. Once I get these in the system though, I definitely need to get some proofs written for them. That is where I am having a fair bit of trouble with the examples and documentation at the moment. I have a solid grasp of Z, and from Rogers email and the documentation, I can just write the proofs mostly in Z, which would save me some time in having to learn HOL right now, though I think I will learn it anyways for the future, just at a slower pace. In any case, the proof writing is not the issue, it is the writing in the ProofPower environment I guess I am hung up on, along with a few other minor things. I will look over all the documentation again on the site Rob, and continuing to see if I can get the examples operational so I can apply what is shown there to my open specifications. Good luck! And do keep asking if you have any more problems. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On Monday 13 Aug 2012 03:24, Jon Lockhart wrote: I have already written the specifications in Word using Z Word Tools, and they are already saved in a variety of formats. I have them transferred over to my linux image. What format do they need to be in for me to get to import them into XPP so I can begin the proof development. ProofPower and Word don't really go together. ProofPower works with LaTeX documents using a special encoding for non-ascii characters. There are no automatic conversions available from Word to this format, though there is an alternative fully ascii source format using keywords instead of special characters. The place to look for full details of ProofPower documents and the facilities associated with them is usr001 ProofPower - Document Preparation which is part of the PPTex option when building ProofPower. The ProofPower documentation is in directory doc of the installation, see index.html in that directory. My second question is once you get those specifications into XPP and the ProofPower tools, then how do you start writing the proofs on the Zed specs? Is it supposed to be in Zed terminology or in HOL? Look at the ProofPower documentation page and you will find tutorials on proof in HOL and in Z. Proofs of Z theorems will ideally stick to Z and not stray into HOL, but it doesn't always work out that way. It is generally recommended to learn how to do proofs in HOL first and then move on to Z, and the tutorial materials for Z assume that the student already knows about proof in HOL, If you don't know LaTeX or HOL then there is a pretty steep learning curve ahead to get into a position to do Z proofs in ProofPower. It is possible to cut out the LaTeX, but without the LaTeX your ProofPower-Z source files would not be printable documents and you would be maintaining two parallel sets of documents, a printable set in Word and sources for ProofPower in a different set of documents. Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On 13 Aug 2012, at 02:15, Roger Bishop Jones wrote: On Monday 13 Aug 2012 03:24, Jon Lockhart wrote: I have already written the specifications in Word using Z Word Tools, and they are already saved in a variety of formats. I have them transferred over to my linux image. What format do they need to be in for me to get to import them into XPP so I can begin the proof development. ProofPower and Word don't really go together. ProofPower works with LaTeX documents using a special encoding for non-ascii characters It is possible to cut out the LaTeX, but without the LaTeX your ProofPower-Z source files would not be printable documents and you would be maintaining two parallel sets of documents, a printable set in Word and sources for ProofPower in a different set of documents. Jon is using Anthony Hall's Z Word Tools, which actually go quite a long way to bridging this gap. Z Word Tools allows you to prepare a Z specification inside a Word document and project out the Z in a format suitable for processing by other tools such as Fuzz or CZT. Anthony and I have talked about adding ProofPower as a list of targets, but it got deferred pending some work I was doing on getting ProofPower to support UTF-8. I have a prototype converter from a UTF-8 format to the ProofPower formats, but it would require a bit of handcranking to get it to convert CZT input into ProofPower input. I don't know how much work would be involved in getting Z Word Tools to output something that ProofPower can eat (e.g., my UTF-8 format). Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On Monday 13 Aug 2012 13:12, Rob Arthan wrote: Jon is using Anthony Hall's Z Word Tools, which actually go quite a long way to bridging this gap. Z Word Tools allows you to prepare a Z specification inside a Word document and project out the Z in a format suitable for processing by other tools such as Fuzz or CZT. Anthony and I have talked about adding ProofPower as a list of targets, but it got deferred pending some work I was doing on getting ProofPower to support UTF-8. I have a prototype converter from a UTF-8 format to the ProofPower formats, but it would require a bit of handcranking to get it to convert CZT input into ProofPower input. I don't know how much work would be involved in getting Z Word Tools to output something that ProofPower can eat (e.g., my UTF-8 format). That's all very interesting, and it would be good to get ProofPower into a less eccentric position on document formats. I have myself recently found myself using utf8 in LaTeX documents (when I wanted to get some Greek in), and may find myself wanting to prepare documents which have both Greek and ProofPower as a result of furthering my modelling of aspects of Aristotle's Organon and Metaphysics. I see from reading a little about this in either or both of emacs and PERL that the support of arbitary encodings rather than specifically of one or more of the UTF variants seems to be thought desirable (and is realised I think in emacs). From this point of view one might consider making the ProofPower encoding respectable by doing whatever is needed for it to be supported by such generic software. It might then be possible to convert between ProofPower's encoding and others using some standard generic utility (perhaps emacs does this). [On further grubbing around I think the generic facilities support a fixed, if perhaps long, list of encodings. I haven't found anything which appears to work from a soft definition of an encoding.] Somewhere in this maze I think there are ways of telling that the greek alphabet does consist of alphabetic characters and hence perhaps should be admitted in ProofPower identifiers. When you speak of my UTF8 format, presumably you are talking about the mapping between the ProofPower extended characters and the unicode character codes (which wouldn't be specific to UTF8). Incidentally, my hacks for making HTML from ProofPower sources, though they once translated into image references, were switched a while back to use unicode entities (not UTF but ascii things like #;) so I do have a mapping between the two (though incomplete). Not good enough to be of any help to you, but I would fall in line with whatever mapping you have come up with if I ever find myself augmenting or fixing it. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Gentlemen, I apologize I should of been more specific at the tasks that I was trying to accomplish and in describing where I am at so far. It seems the first point of business though from what Rob is saying is actually getting the specifications into the ProofPower environment, which at this point sounds like it needs to be done by hand, but I will explain it more closely Rob. That way you can tell me if I got a shot of importing them or if I am going to have to do a hand rewrite. So as you mentioned Rob, I am using Anthony's Z Word Tools for Word and I have written all my specifications in there so far. It is a fabulous writing tool, interfacing so well with Word, and providing all the structure I need to write the specifications I am working on. Now, I am not sure if you are aware of this, but the latest version of the Z Word Tools no longer requires an export of the specification to be used with FUZZ or CZT, those checkers are built right into the tool now and allow for typechecking of the specification as you are writing it, using either checker. Now of course, neither of these checkers run on .doc / .docx format files, and there are a whole host of other files generated when you save or run a check, including a LaTeX file of the specification. I was wondering if you thought this LaTeX file would be possible to import into the ProofPower system, or does it have to be in a special format of .tex to be of any use? I have attached one of the specifications I was originally using to learn Z Word Tools, and it has passed all the typecheckers. This is the LaTeX file that is generated for the specification. Thanks, Jon On Mon, Aug 13, 2012 at 10:59 AM, Roger Bishop Jones r...@rbjones.comwrote: On Monday 13 Aug 2012 13:12, Rob Arthan wrote: Jon is using Anthony Hall's Z Word Tools, which actually go quite a long way to bridging this gap. Z Word Tools allows you to prepare a Z specification inside a Word document and project out the Z in a format suitable for processing by other tools such as Fuzz or CZT. Anthony and I have talked about adding ProofPower as a list of targets, but it got deferred pending some work I was doing on getting ProofPower to support UTF-8. I have a prototype converter from a UTF-8 format to the ProofPower formats, but it would require a bit of handcranking to get it to convert CZT input into ProofPower input. I don't know how much work would be involved in getting Z Word Tools to output something that ProofPower can eat (e.g., my UTF-8 format). That's all very interesting, and it would be good to get ProofPower into a less eccentric position on document formats. I have myself recently found myself using utf8 in LaTeX documents (when I wanted to get some Greek in), and may find myself wanting to prepare documents which have both Greek and ProofPower as a result of furthering my modelling of aspects of Aristotle's Organon and Metaphysics. I see from reading a little about this in either or both of emacs and PERL that the support of arbitary encodings rather than specifically of one or more of the UTF variants seems to be thought desirable (and is realised I think in emacs). From this point of view one might consider making the ProofPower encoding respectable by doing whatever is needed for it to be supported by such generic software. It might then be possible to convert between ProofPower's encoding and others using some standard generic utility (perhaps emacs does this). [On further grubbing around I think the generic facilities support a fixed, if perhaps long, list of encodings. I haven't found anything which appears to work from a soft definition of an encoding.] Somewhere in this maze I think there are ways of telling that the greek alphabet does consist of alphabetic characters and hence perhaps should be admitted in ProofPower identifiers. When you speak of my UTF8 format, presumably you are talking about the mapping between the ProofPower extended characters and the unicode character codes (which wouldn't be specific to UTF8). Incidentally, my hacks for making HTML from ProofPower sources, though they once translated into image references, were switched a while back to use unicode entities (not UTF but ascii things like #;) so I do have a mapping between the two (though incomplete). Not good enough to be of any help to you, but I would fall in line with whatever mapping you have come up with if I ever find myself augmenting or fixing it. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com Elevator_Zed_Tools_V1.tex Description: TeX document ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On 13 Aug 2012, at 12:05, Jon Lockhart wrote: Gentlemen, I apologize I should of been more specific at the tasks that I was trying to accomplish and in describing where I am at so far. It seems the first point of business though from what Rob is saying is actually getting the specifications into the ProofPower environment, which at this point sounds like it needs to be done by hand, but I will explain it more closely Rob. That way you can tell me if I got a shot of importing them or if I am going to have to do a hand rewrite. So as you mentioned Rob, I am using Anthony's Z Word Tools for Word and I have written all my specifications in there so far. It is a fabulous writing tool, interfacing so well with Word, and providing all the structure I need to write the specifications I am working on. Now, I am not sure if you are aware of this, but the latest version of the Z Word Tools no longer requires an export of the specification to be used with FUZZ or CZT, those checkers are built right into the tool now and allow for typechecking of the specification as you are writing it, using either checker I think you will find that Z Word Tools is actually extracting the Z into a file and running Fuzz or CZT for you, so it feels like the typechecker is built in. You will find that the menu you use to do the typechecking has an item on it to export the Z as a file. Now of course, neither of these checkers run on .doc / .docx format files, and there are a whole host of other files generated when you save or run a check, including a LaTeX file of the specification. I was wondering if you thought this LaTeX file would be possible to import into the ProofPower system, or does it have to be in a special format of .tex to be of any use? I actually thought that the CZT unicode format might be a bit closer to what my prototype tools for dealing with UTF-8 can cope with. If you only have a few pages of Z to start with, then it will probably be quicker just to reenter it manually. If you have more it may be worth trying to cobble together something semi-automated. We should be able to do something much slicker in the slightly longer term. I have attached one of the specifications I was originally using to learn Z Word Tools, and it has passed all the typecheckers. This is the LaTeX file that is generated for the specification. Thanks. This reminds me that one of the bigger problems is that ProofPower has different rules for newlines than Spivey and the Standard Z. Specifically, ProofPower requires semicolons at the end of declarations and to separate stacked predicates in the predicate parts of schemas. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On 13 Aug 2012, at 10:59, Roger Bishop Jones wrote: On Monday 13 Aug 2012 13:12, Rob Arthan wrote: Jon is using Anthony Hall's Z Word Tools, which actually go quite a long way to bridging this gap. Z Word Tools allows you to prepare a Z specification inside a Word document and project out the Z in a format suitable for processing by other tools such as Fuzz or CZT. Anthony and I have talked about adding ProofPower as a list of targets, but it got deferred pending some work I was doing on getting ProofPower to support UTF-8. I have a prototype converter from a UTF-8 format to the ProofPower formats, but it would require a bit of handcranking to get it to convert CZT input into ProofPower input. I don't know how much work would be involved in getting Z Word Tools to output something that ProofPower can eat (e.g., my UTF-8 format). That's all very interesting, and it would be good to get ProofPower into a less eccentric position on document formats. I agree. I have myself recently found myself using utf8 in LaTeX documents (when I wanted to get some Greek in), and may find myself wanting to prepare documents which have both Greek and ProofPower as a result of furthering my modelling of aspects of Aristotle's Organon and Metaphysics. I see from reading a little about this in either or both of emacs and PERL that the support of arbitary encodings rather than specifically of one or more of the UTF variants seems to be thought desirable (and is realised I think in emacs). From this point of view one might consider making the ProofPower encoding respectable by doing whatever is needed for it to be supported by such generic software. Surely just accepting and outputting UTF-8 will achieve that, won't it? It might then be possible to convert between ProofPower's encoding and others using some standard generic utility (perhaps emacs does this). [On further grubbing around I think the generic facilities support a fixed, if perhaps long, list of encodings. I haven't found anything which appears to work from a soft definition of an encoding.] Somewhere in this maze I think there are ways of telling that the greek alphabet does consist of alphabetic characters and hence perhaps should be admitted in ProofPower identifiers. That is somewhat orthogonal to how I would plan to do the ProofPower side of this in the first instance. When you speak of my UTF8 format, presumably you are talking about the mapping between the ProofPower extended characters and the unicode character codes (which wouldn't be specific to UTF8). Yes. Incidentally, my hacks for making HTML from ProofPower sources, though they once translated into image references, were switched a while back to use unicode entities (not UTF but ascii things like #;) so I do have a mapping between the two (though incomplete). Not good enough to be of any help to you, but I would fall in line with whatever mapping you have come up with if I ever find myself augmenting or fixing it. When I got some time. I will tidy up the little prototype converter I wrote and make it available for you to have a look at. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

Rob, Ok so looks like I am looking to rewrite all my specifications again in ProofPower. A minor inconvenience but should not be a problem. I will just pop up my specs on one screen and bring up ProofPower's XPP up on the other screen in my Linux VM, and I should be able to rewrite them with no problems. The only thing I can't seem to find is the symbol library in XPP. I have found where I can insert the various Zed structures, no problem, but there is supposed to be an XPP keyboard that has these symbols, based on the pictures in the documentation. Is this available in the editor version of XPP or do I need to run the full version of XPP to have access to that? Once I get these in the system though, I definitely need to get some proofs written for them. That is where I am having a fair bit of trouble with the examples and documentation at the moment. I have a solid grasp of Z, and from Rogers email and the documentation, I can just write the proofs mostly in Z, which would save me some time in having to learn HOL right now, though I think I will learn it anyways for the future, just at a slower pace. In any case, the proof writing is not the issue, it is the writing in the ProofPower environment I guess I am hung up on, along with a few other minor things. I will look over all the documentation again on the site Rob, and continuing to see if I can get the examples operational so I can apply what is shown there to my open specifications. Thanks, Jon On Mon, Aug 13, 2012 at 1:12 PM, Rob Arthan r...@lemma-one.com wrote: On 13 Aug 2012, at 12:05, Jon Lockhart wrote: Gentlemen, I apologize I should of been more specific at the tasks that I was trying to accomplish and in describing where I am at so far. It seems the first point of business though from what Rob is saying is actually getting the specifications into the ProofPower environment, which at this point sounds like it needs to be done by hand, but I will explain it more closely Rob. That way you can tell me if I got a shot of importing them or if I am going to have to do a hand rewrite. So as you mentioned Rob, I am using Anthony's Z Word Tools for Word and I have written all my specifications in there so far. It is a fabulous writing tool, interfacing so well with Word, and providing all the structure I need to write the specifications I am working on. Now, I am not sure if you are aware of this, but the latest version of the Z Word Tools no longer requires an export of the specification to be used with FUZZ or CZT, those checkers are built right into the tool now and allow for typechecking of the specification as you are writing it, using either checker I think you will find that Z Word Tools is actually extracting the Z into a file and running Fuzz or CZT for you, so it feels like the typechecker is built in. You will find that the menu you use to do the typechecking has an item on it to export the Z as a file. Now of course, neither of these checkers run on .doc / .docx format files, and there are a whole host of other files generated when you save or run a check, including a LaTeX file of the specification. I was wondering if you thought this LaTeX file would be possible to import into the ProofPower system, or does it have to be in a special format of .tex to be of any use? I actually thought that the CZT unicode format might be a bit closer to what my prototype tools for dealing with UTF-8 can cope with. If you only have a few pages of Z to start with, then it will probably be quicker just to reenter it manually. If you have more it may be worth trying to cobble together something semi-automated. We should be able to do something much slicker in the slightly longer term. I have attached one of the specifications I was originally using to learn Z Word Tools, and it has passed all the typecheckers. This is the LaTeX file that is generated for the specification. Thanks. This reminds me that one of the bigger problems is that ProofPower has different rules for newlines than Spivey and the Standard Z. Specifically, ProofPower requires semicolons at the end of declarations and to separate stacked predicates in the predicate parts of schemas. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

### Re: [ProofPower] Trying to Prove my Zed Specifications

On 13 Aug 2012, at 13:31, Jon Lockhart wrote: Rob, Ok so looks like I am looking to rewrite all my specifications again in ProofPower. A minor inconvenience but should not be a problem. That is likely the quickest way to get started. I will just pop up my specs on one screen and bring up ProofPower's XPP up on the other screen in my Linux VM, and I should be able to rewrite them with no problems. The only thing I can't seem to find is the symbol library in XPP. I have found where I can insert the various Zed structures, no problem, but there is supposed to be an XPP keyboard that has these symbols, based on the pictures in the documentation. Is this available in the editor version of XPP or do I need to run the full version of XPP to have access to that? The keyboard in the picture is the actual keyboard, although you may need to do a bit more work to set it up. There is a tool called the Palette in the Tools menu that lets you enter all the symbols with mouse clicks without having to do any more set-up and without having to learn the key combinations. If you do want to set up the keyboard have a read of section 4.3 of the Xpp manual and the comments at the head of the file app-defaults/XppKeyboard in the first instance. Once I get these in the system though, I definitely need to get some proofs written for them. That is where I am having a fair bit of trouble with the examples and documentation at the moment. I have a solid grasp of Z, and from Rogers email and the documentation, I can just write the proofs mostly in Z, which would save me some time in having to learn HOL right now, though I think I will learn it anyways for the future, just at a slower pace. In any case, the proof writing is not the issue, it is the writing in the ProofPower environment I guess I am hung up on, along with a few other minor things. I will look over all the documentation again on the site Rob, and continuing to see if I can get the examples operational so I can apply what is shown there to my open specifications. Good luck! And do keep asking if you have any more problems. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com