Roger,

Thanks for the help. I from what you have just said I better understand
about the consistency proofs for axioms in ProofPower, and more importantly
Zed. I will probably in the future if I have complicated and none trivial
axioms to prove, then I will just leave the variable set to true. In most
of the specifications I have worked on and currently working on, I have
only been uisng axioms as a way to declare global variables and constraints
to the system, so that it gives the developer a more constrained box to
work in when taking the specification and converting it to code.

I will take a look at the axiomatic proof you did and see if I can't use it
to help me finish proving the rest of my axioms before I move on to
finishing the preconditions of my operations.

Thanks,
Jon


On Fri, Sep 14, 2012 at 1:48 PM, Roger Bishop Jones <r...@rbjones.com> wrote:

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

Reply via email to