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