Re: [ProofPower] Trying to Prove my Zed Specifications

[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  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

[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  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

[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

[Jon Lockhart]

Roger,

That linear arithmetic command worked great and finished off the solution
no problem. Unfortunately I realized I needed to show that the starting and
calling floors were greater than zero not greater than or equal to zero. 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.

Regards,
Jon


On Mon, Nov 5, 2012 at 9:20 AM, Jon Lockhart  wrote:

> 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"  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
>>
>


errorEncountered.doc.gz
Description: GNU Zip compressed data


newElevatorSpec.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Jon 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"  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

[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

[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

[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  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 
> Date: Sun, Oct 21, 2012 at 6:29 PM
> Subject: Re: [ProofPower] Trying to Prove my Zed Specifications
> To: Roger Bishop Jones 
> Cc: ProofPower List 
>
>
> 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 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 u

Re: [ProofPower] Trying to Prove my Zed Specifications

[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  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

[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

[Jon Lockhart]

Roger,

I tried using that before, and ProofPower gave me an exception. I asked
about it in the beginning from Rob, and he said == worked in the latest
update on the source page, which I believe I have a few versions older. I
tried updating myself, but my advisor has some odd permissions so he have
to do it, and he just hasn't yet, so untill he does I am stuck with the ^=.

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 Thu, Oct 18, 2012 at 6:03 AM, Rob Arthan  wrote:

>
> On 17 Oct 2012, at 07:21, Roger Bishop Jones wrote:
>
> The binding display for your witness uses "=" but should use
> "=^" (equal with hat).
>
>
> As an aside, you can now also use "==" like the Z standard. This is a bit
> easier to find on the keyboard when you are in a hurry doing a proof.
>
> 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

[Rob Arthan]

On 17 Oct 2012, at 07:21, Roger Bishop Jones wrote:
> The binding display for your witness uses "=" but should use 
> "=^" (equal with hat).

As an aside, you can now also use "==" like the Z standard. This is a bit 
easier to find on the keyboard when you are in a hurry doing a proof.

Regards,

Rob.___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Jon 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 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
>>
>
>


elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Jon 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  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 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

[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  wrote:

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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger 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

[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  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 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 at

Re: [ProofPower] Trying to Prove my Zed Specifications

[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  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

Re: [ProofPower] Trying to Prove my Zed Specifications

[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

[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  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

[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

[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 wrote:

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


elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger 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

[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  wrote:

> Jon,
>
> On Tuesday 09 Oct 2012 20:22, Jon Lockhart wrote:
>
> > I am having a little trouble getting the axioms created,
> > moving the static portions of the Button_State to an
> > axiom from the schema. I can't seem to get the proof to
> > operate properly. Any suggestions?
>
> The problem is that the existential goal you are trying to
> prove has decorations on the names of the variables, but the
> witness you have supplied does not.
>
> This is a point of difference between proving the non-
> emptyness of a schema and the consistency of an axiomatic
> specification.
>
> Because the names in the signature of the axiomatic spec
> have already been introduced as global variables (aka
> constants), they cannot be used as the names in the
> existential which must be proven to establish the
> consistency of the axiomatic specification.
> So they get primed.
>
> When z exists tac complains that it can't match the witness
> against the signature of the existential, first check that
> the names you have used in the binding are exactly those in
> the existential you are trying to prove, then check that the
> expressions have the right type.
>
> regards,
> Roger Jones
>
>


elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data


errorEncountered.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger 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

[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  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 wrote:
>
>>
>> On Friday 28 Sep 2012 22:26, Jon Lockhart wrote:
>>
>> > I have two questions on that then. First, from a since
>> > and style standpoint, if I wanted to make everything
>> > neat in the spec I would place the no changing sets in
>> > the axiom after the state schema, but for functionality
>> > standpoint, if I wanted to use them in the predicate
>> > section of the schema they would need to go before it.
>> > So what would you see as being the better option? The
>> > second is would I prove their consistency just like I
>> > did the global variables?
>>
>> First I should repeat my caveat. This is not a style of
>> specification which I have used or studied, so my views on
>> this may be eccentric.
>>
>> If you are using ProofPower you have to present the
>> specification so that every global variable is specified
>> before it is used.  There may be tools which can reorder the
>> specification for you, but ProofPower doesn't.
>> I'm not entirely sure what you meant by "in the axiom after
>> the state schema", I hope you didn't mean in the predicate
>> of the state schema!
>>
>> Yes, consistency proofs are the same as the ones you have
>> been doing.
>> When you say "just like the global variables", you do them
>> like global variables because they will actually be global
>> variables.
>>
>> > I do see a problem though in that I don't want those sets
>> > to be accessed by anyone, only if the schema is included
>> > in the beginning of the operation.
>>
>> It won't be possible to change them, but they will be global
>> variables so any part of the specification after they have
>> been introduced could access them.
>>
>> > Could we resolve this
>> > matter by using the schema paragraphs? So we would
>> > create two schema descriptions of Button_State for
>> > example and then the first contains the static and the
>> > second the dynamic sets.
>>
>> I think that is a good way of organising this material.
>> But the nub of the original suggestion was that they might
>> be taken out of the signature of the operations, and in
>> order for them to be accessible in defining the operations on
>> the state they would have to be made into global variables
>> (which is appropriate for something the specification regards
>> as fixed in value).
>>
>> So if you did define a schema containing what one might
>> consider configuration data, you would have to use that
>> schema to introduce the names in its signature as global
>> variables so that they could then be accessed in you
>> operation specifications (or in your definition of state).
>>
>> > Then when accessing an
>> > operation the static or does not change symbol is placed
>> > in front of the static Button_State schema, allowing
>> > access to the sets, but not allowing change, and this
>> > way only when the name is provided in the description is
>> > the information accessible. Would that work to
>> > accomplish the same goal?
>>
>> You could do something like this, though its not what I
>> intended to suggest.
>> If I understand you correctly you are suggesting that the
>> signature of the operation contains certain fixed data as
>> well as the components  which are subject to change (and any
>> input or output values).
>>
>> I have never seen this done, and so I imagine this is a
>> larger departure from normal practice than I was advocating.
>> It has some disadvantages relative to the method I intended
>> to suggest.
>>
>> Generally it is a good idea to try and structure the
>> specification so that the size of signatures does not get
>> very large.
>> It is a disadvantage of Z that the syle of specification
>> encourages all the state of the system to be represented in
>> the flat signature of a single state schema,
>> You can split this up into many parts and use schema
>> inclusion to make this seem better structured in the
>> specification, but when you come to reasoning with it you
>> will be 

Re: [ProofPower] Trying to Prove my Zed Specifications

[Jon Lockhart]

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  wrote:

>
> On Friday 28 Sep 2012 22:26, Jon Lockhart wrote:
>
> > I have two questions on that then. First, from a since
> > and style standpoint, if I wanted to make everything
> > neat in the spec I would place the no changing sets in
> > the axiom after the state schema, but for functionality
> > standpoint, if I wanted to use them in the predicate
> > section of the schema they would need to go before it.
> > So what would you see as being the better option? The
> > second is would I prove their consistency just like I
> > did the global variables?
>
> First I should repeat my caveat. This is not a style of
> specification which I have used or studied, so my views on
> this may be eccentric.
>
> If you are using ProofPower you have to present the
> specification so that every global variable is specified
> before it is used.  There may be tools which can reorder the
> specification for you, but ProofPower doesn't.
> I'm not entirely sure what you meant by "in the axiom after
> the state schema", I hope you didn't mean in the predicate
> of the state schema!
>
> Yes, consistency proofs are the same as the ones you have
> been doing.
> When you say "just like the global variables", you do them
> like global variables because they will actually be global
> variables.
>
> > I do see a problem though in that I don't want those sets
> > to be accessed by anyone, only if the schema is included
> > in the beginning of the operation.
>
> It won't be possible to change them, but they will be global
> variables so any part of the specification after they have
> been introduced could access them.
>
> > Could we resolve this
> > matter by using the schema paragraphs? So we would
> > create two schema descriptions of Button_State for
> > example and then the first contains the static and the
> > second the dynamic sets.
>
> I think that is a good way of organising this material.
> But the nub of the original suggestion was that they might
> be taken out of the signature of the operations, and in
> order for them to be accessible in defining the operations on
> the state they would have to be made into global variables
> (which is appropriate for something the specification regards
> as fixed in value).
>
> So if you did define a schema containing what one might
> consider configuration data, you would have to use that
> schema to introduce the names in its signature as global
> variables so that they could then be accessed in you
> operation specifications (or in your definition of state).
>
> > Then when accessing an
> > operation the static or does not change symbol is placed
> > in front of the static Button_State schema, allowing
> > access to the sets, but not allowing change, and this
> > way only when the name is provided in the description is
> > the information accessible. Would that work to
> > accomplish the same goal?
>
> You could do something like this, though its not what I
> intended to suggest.
> If I understand you correctly you are suggesting that the
> signature of the operation contains certain fixed data as
> well as the components  which are subject to change (and any
> input or output values).
>
> I have never seen this done, and so I imagine this is a
> larger departure from normal practice than I was advocating.
> It has some disadvantages relative to the method I intended
> to suggest.
>
> Generally it is a good idea to try and structure the
> specification so that the size of signatures does not get
> very large.
> It is a disadvantage of Z that the syle of specification
> encourages all the state of the system to be represented in
> the flat signature of a single state schema,
> You can split this up into many parts and use schema
> inclusion to make this seem better structured in the
> specification, but when you come to reasoning with it you
> will be reasoning with objects which have very large
> signatures, and this make comprehension of what's going on
> more difficult.
> In ProofPower is can lead to performance problems, and may
> lead to hard to understand diagnostics from the type
> inference system.
>
> Another problem which may arise is in the schema calculus.
> I have not looked into it, but operations like composition
> may not do the right thing with the extra com

Re: [ProofPower] Trying to Prove my Zed Specifications

[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

[Jon Lockhart]

Roger,

That is an interesting point you bring up. It is very true that there are
static sets in there that are subsets in there that we do not want to
change. We would only really want to change pushed set, adding and removing
buttons from it. Same for the other states, they have subsets we would not
want changing in the specification. I like the idea of moving them out of
the scheme blocks and into axiomatic blocks.

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?

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.
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. 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?

Regards,
Jon

On Wed, Sep 26, 2012 at 4:35 AM, Roger Bishop Jones  wrote:

> 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

[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

[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  wrote:

> Jon,
>
> On Sunday 23 Sep 2012 22:32, Jon Lockhart wrote:
>
> > I tried adding the exclamation point to the end of the
> > pushed' line, but if gave me a paser error saying free
> > types here not allowed. I have provided exactly the what
> > the paragraph looked like I tried to parse and the error
> > that was reported in the errorEncountered document.
>
> The perils of not carefully quoting!
> The exclamation mark was not intended to be in the formal
> text, it was just my exclamation.
>
> The point I was making was just that you had said "push'={}"
> and it should have been "pushed'={}"!
>
> > I went back to just having the two exclamation points on
> > pushed and Button_State, in the predicate and
> > declaration section of the schema box respectively, and
> > this generated a monster of subgoals when I tried the
> > provided proof strategy. Obviously there should not be
> > that much to prove, especially when everything is the
> > same, except for push just being set to the empty set.
>
> Should be "pushed"!
>
> Make sure you have no occurrences of "push" and if you still
> have a problem with the proof post it.
>
> > I
> > have also gone back and reviewed Jacky's "The Way of
> > Zed" and he uses the delta operator to signify there are
> > changes being made to the states, though he never
> > discusses initialization, but there appears to be some
> > disconnect between the authors, though I know Spivey and
> > Woodcock should probably be followed so I like to stick
> > with what they say is best practice.
>
> I don't have access to Jacky's book so I can't comment.
>
> > As for the Init and State blocks that I am trying to and
> > have proven, should there be a change there so that the
> > proof is not of precondition but of consistency? As you
> > have mentioned, and I have agreed with, it is really
> > pointless to do the precondition proofs for the states
> > when they are static and not changing, everything
> > remains the same, and they are only showing the
> > information provided is consistent.
>
> Yes, try proving:
>
> ∃ Init ∙ true
> and
> ∃ State ∙ true
>
> Both should be trivial proofs.
>
> Roger
>


elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data


errorEncountered.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

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

___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Jon 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  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

[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

[Rob Arthan]

On 22 Sep 2012, at 00:11, Jon Lockhart wrote:

> 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 don't recognise that error message. Is your state variable called "push" or 
something a little different? Please try again and report back if you really 
can't get things to work.

> 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. 


I am not quite sure what you mean. ProofPower and the ISO Standard don't impose 
any conventions on how you use schemas to specify a system. If you want to use 
the style where initialisation schemas specify an after-state (with primes), 
then you may.

Regards,

Rob.




___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Jon 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  wrote:

> On Friday 21 Sep 2012 11:52, Roger Bishop Jones wrote:
> > I checked Spivey (Understanding Z)
>
> In fact it was "The Z Notation" I checked.
>
> Roger
>
> ___
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger 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

[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

[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 wrote:

> 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
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Jon 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 wrote:

> 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
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Phil 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

[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

[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  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

[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

[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  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  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

[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  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

[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

[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

[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  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 wrote:
>
>> Jon,
>>
>> On Friday 14 Sep 2012 21:14, Jon Lockhart wrote:
>>
>> > Now I have moved on to trying to do the same thing for
>> > masterReset, using the exact same code that Roger has
>> > implemented in my spec, but now I am getting an error
>> > when I try to push the consistency goal.
>>
>> That's because its a single specification for two constants,
>> and you have already proven the consistency goal.
>>
>> Recall that the proof offered a composite witness, a binding
>> with one component for each of the constituents of the
>> signature of the axiomatic specification, both set to True.
>>
>> Roger
>>
>> ___
>> Proofpower mailing list
>> Proofpower@lemma-one.com
>> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
>>
>
>


elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data


errorEncountered.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Jon Lockhart]

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  wrote:

> 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
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger Bishop Jones]

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

Re: [ProofPower] Trying to Prove my Zed Specifications

[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 wrote:

> 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
>


elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Phil 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

[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  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

[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

[Roger Bishop Jones]

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


elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Jon 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  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


e

Re: [ProofPower] Trying to Prove my Zed Specifications

[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

[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

[Phil Clayton]

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.


Phil


___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Roger 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

[Jon Lockhart]

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 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. So that is where I am at right now.

Thanks,
Jon


On Thu, Sep 13, 2012 at 7:30 PM, Phil Clayton wrote:

> 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
>


elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Phil 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

[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 wrote:

> 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
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Phil 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

[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  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 wrote:
>
>> 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.**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%>%;
>>

Re: [ProofPower] Trying to Prove my Zed Specifications

[Phil Clayton]

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.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
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[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 wrote:

> 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
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Phil 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

[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

[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"  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

[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

[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  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 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" >> > 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

[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 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" > > 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

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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Phil 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" 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

[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"  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

[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

[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 wrote:

> 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 go

Re: [ProofPower] Trying to Prove my Zed Specifications

[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 sligh

Re: [ProofPower] Trying to Prove my Zed Specifications

[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

[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  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

[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

[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  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  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 /bin/xpp 
> 
> and then when gdb gives you its prompt, type "where".
> 
> Regards,
> 
> Rob.
> 
> 
> 
> 
> 

___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Jon 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  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 /bin/xpp 
>
> and then when gdb gives you its prompt, type "where".
>
> Regards,
>
> Rob.
>
>
>
>
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Rob 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 /bin/xpp 

and then when gdb gives you its prompt, type "where".

Regards,

Rob.




___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] Trying to Prove my Zed Specifications

[Jon 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  wrote:

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

Re: [ProofPower] Trying to Prove my Zed Specifications

[Rob 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

[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

[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  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

[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

Re: [ProofPower] Trying to Prove my Zed Specifications

[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  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

[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

[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

[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 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 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

[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

[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

[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

[ProofPower] Trying to Prove my Zed Specifications

[Jon Lockhart]

Hello Community,

I was wondering if I could get some help with trying to start to write up
proofs for some Zed specifications I have already written.

I have read the documentation on the site, and tried playing with the
examples provided, but I am still have a fair amount of difficulty. Rather
than flounder around, I figure I ask for help.

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.

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?

Any help would appreciated in getting things rolling.

Thanks,
Jon Lockhart
___
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com