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.


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.

Attachment: elevatorSpecV5_P1.doc
Description: MS-Word document

Attachment: elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to