Re: [ProofPower] Trying to Prove my Zed Specifications

2012-11-12 Thread Jon Lockhart
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

2012-11-07 Thread Jon Lockhart
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

2012-11-06 Thread Roger Bishop Jones
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

2012-11-05 Thread Roger Bishop Jones
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

2012-11-05 Thread Roger Bishop Jones
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

2012-11-05 Thread Jon Lockhart
Roger,

Thank you very much. I will take a look a this tactic.

Regards,
Jon
On Nov 5, 2012 4:27 AM, Roger Bishop Jones r...@rbjones.com wrote:

 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

2012-11-04 Thread Jon Lockhart
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

2012-10-21 Thread Jon Lockhart
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

2012-10-18 Thread Roger Bishop Jones
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

2012-10-17 Thread Roger Bishop Jones
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

2012-10-17 Thread Jon Lockhart
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

2012-10-17 Thread Jon Lockhart
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

2012-10-17 Thread Jon Lockhart

 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

2012-10-16 Thread Roger Bishop Jones
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

2012-10-16 Thread Jon Lockhart
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

2012-10-16 Thread Jon Lockhart
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

2012-10-15 Thread Jon Lockhart
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

2012-10-14 Thread Roger Bishop Jones
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

2012-10-13 Thread Roger Bishop Jones
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

2012-10-13 Thread Jon Lockhart
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

2012-10-12 Thread Jon Lockhart
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

2012-10-09 Thread Jon Lockhart
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

2012-10-09 Thread Roger Bishop Jones
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

2012-10-02 Thread Roger Bishop Jones

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

2012-09-26 Thread Roger Bishop Jones
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

2012-09-25 Thread Jon Lockhart
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

2012-09-23 Thread Jon Lockhart
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

2012-09-22 Thread Roger Bishop Jones
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

2012-09-21 Thread Roger Bishop Jones
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

2012-09-21 Thread Roger Bishop Jones
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


Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-21 Thread Jon Lockhart
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

2012-09-20 Thread Jon Lockhart
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

2012-09-20 Thread Phil Clayton

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

2012-09-20 Thread Jon Lockhart
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

2012-09-20 Thread Jon Lockhart
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

2012-09-19 Thread Jon Lockhart
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

2012-09-19 Thread Roger Bishop Jones
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

2012-09-19 Thread Jon Lockhart
 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

2012-09-18 Thread Jon Lockhart
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

2012-09-18 Thread Roger Bishop Jones
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

2012-09-18 Thread Rob Arthan
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

2012-09-18 Thread Jon Lockhart
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

2012-09-14 Thread Roger Bishop Jones
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

2012-09-14 Thread Roger Bishop Jones
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

2012-09-14 Thread Rob Arthan

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

2012-09-14 Thread Jon Lockhart
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

2012-09-14 Thread Phil Clayton

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

2012-09-14 Thread Jon Lockhart
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

2012-09-14 Thread Phil Clayton

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

2012-09-14 Thread Jon Lockhart
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

2012-09-13 Thread Jon Lockhart
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

2012-09-13 Thread Phil Clayton

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

2012-09-13 Thread Jon Lockhart
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

2012-09-13 Thread Phil Clayton

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

2012-09-12 Thread Phil Clayton

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

2012-09-12 Thread Phil Clayton

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

2012-09-12 Thread Jon Lockhart
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

2012-09-04 Thread Roger Bishop Jones
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

2012-09-04 Thread Rob Arthan
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

2012-09-03 Thread Jon Lockhart
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

2012-09-03 Thread Jon Lockhart
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

2012-09-02 Thread Jon Lockhart
Rob,

I have a question for you about a particular exception I am running into.
So I have gone through all the tutorial documents, and even after all that
I realize I have a long way to go with getting the hang of things, but I am
currently trying to enter in a small example to try and begin performing
some proofs on it and get comfortable before moving on to my much larger
specifications that I need to prove for my dissertation. I have tried
looking for the answer to the exception in the reference manual, but it is
very large and my search inquiries seem to be coming up empty.

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. I certainly do not
want it to be a variable either, I want to use it as a set operator.

Do I need to typecast this symbol as something, such as an ML or HOL object
inside the Z paragraph?

Any help would be greatly appreciated.

Thanks,
Jon

On Sun, Aug 26, 2012 at 6:53 AM, Anthony Hall anth...@anthonyhall.orgwrote:

 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

Re: [ProofPower] Trying to Prove my Zed Specifications

2012-09-02 Thread Phil Clayton

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

2012-09-02 Thread Jon Lockhart
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

2012-09-02 Thread Phil Clayton

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

2012-09-02 Thread Jon Lockhart
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

2012-08-26 Thread Roger Bishop Jones
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

2012-08-26 Thread Anthony Hall
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

2012-08-25 Thread Jon Lockhart
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

2012-08-22 Thread Rob Arthan

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

2012-08-20 Thread Rob Arthan
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

2012-08-20 Thread Jon Lockhart
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

2012-08-20 Thread Rob Arthan
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

2012-08-19 Thread Roger Bishop Jones
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

2012-08-19 Thread Rob Arthan
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

2012-08-19 Thread Jon Lockhart
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

2012-08-18 Thread Jon Lockhart
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

2012-08-13 Thread Roger Bishop Jones
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

2012-08-13 Thread Rob Arthan

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

2012-08-13 Thread Roger Bishop Jones
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

2012-08-13 Thread Jon Lockhart
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

2012-08-13 Thread Rob Arthan

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

2012-08-13 Thread Rob Arthan

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

2012-08-13 Thread Jon Lockhart
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

2012-08-13 Thread Rob Arthan

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