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

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

Reply via email to