Hello Community,

I was wondering if I could get some help with trying to start to write up
proofs for some Zed specifications I have already written.

I have read the documentation on the site, and tried playing with the
examples provided, but I am still have a fair amount of difficulty. Rather
than flounder around, I figure I ask for help.

I have already written the specifications in Word using Z Word Tools, and
they are already saved in a variety of formats. I have them transferred
over to my linux image. What format do they need to be in for me to get to
import them into XPP so I can begin the proof development.

My second question is once you get those specifications into XPP and the
ProofPower tools, then how do you start writing the proofs on the Zed
specs? Is it supposed to be in Zed terminology or in HOL?

Any help would appreciated in getting things rolling.

Jon Lockhart
Proofpower mailing list

Reply via email to