Roger,
Got that error corrected, thanks for the input. Encounterd a few more hang
ups on doing the proof but those were eliminated by grabbing the spec for
elevator on the rewrite tactic. Same for floor.
Now I am back to the Init operations. I have attached the specification
again for you veiwing, but if I remember correctly we were going with using
the There Exists proof still on these like we did for the States.
Any direction on how to finish these up so I may move on to the actual
operations would be greatly appreciated.
Regards,
Jon
On Sat, Oct 13, 2012 at 12:28 PM, Roger Bishop Jones r...@rbjones.comwrote:
Jon,
On Friday 12 Oct 2012 20:35, Jon Lockhart wrote:
I got back to the specification today, and moved on to
proving the elevator state schema, Elevator_State, and I
moved the static component elevator to an axiom, similar
to the static components of button. Unfortunately I get
a weird sub goal pop up that says {} = elevator after
I work on the existence proof. Is this b/c I used the
empty set as the witness to the elevator axiom proof?
No, its because you set both moving and stopped to the empty
set, and this can only be the case if there are no
elevators.
Your spec doesn't say there are no elevators, so you can't
prove it.
You need to supply a witness for which the union of moving
and stopped can be proven to be elevators, even though
you don't know what elevators is.
One way to do that is to use the state in which everything
is stopped, i.e. in which moving = {} and stopped =
elevators.
I haven't checked that that satisfies the rest of the
predicate, but I guess that's probable.
Roger
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
