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 <r...@lemma-one.com> 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.
>

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