So I have run into an error again while working on my specification. This
time it is with the second axiomatic definition, the one right after Roger
helped me with last time. Using what he had done, and from the integer
example in the tutorial notes, I set up the evidence for how I thought the
system would want it to be given to it. Unfortunately this throws an
exception and I can't seem to massage it to be what it wants.

Attached is the spec and a document containing the error.

Regards,
Jon


On Sat, Sep 15, 2012 at 1:07 PM, Jon Lockhart <jal...@bucknell.edu> wrote:

> Roger,
>
> Thanks for making that clear about how the system handles that. I was
> thinking that is what had happened but I wanted to make sure and get a
> clearer picture.
>
> Now time to keep pushing forward.
>
> Thanks,
> Jon
>
>
>
> On Fri, Sep 14, 2012 at 4:56 PM, Roger Bishop Jones <r...@rbjones.com>wrote:
>
>> 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
>>
>
>

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

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