Jon,

On 13/09/12 00:24, Jon Lockhart wrote:
Unfortunately the two extra sets I want to
declare and add to the spec are causing parser errors in ProofPower. The
sets I am trying to declare are TIMER == 0..5 and BOOLEAN == {0, 1}
which is allowed in the normal standard and has been syntactically
cleared by FUZZ and CZT through Anthony's Z Word Tools. Unfortunately
ProofPower doesn't allow me to do such a thing and I am wondering what
would be the proper protocol for adding such sets to a specification in
ProofPower.


These work in the version I have, 2.9.1w2.rda.120805, the latest patch which fixes the recent Xpp issue. (Generally it would be useful to see the error message you get.) ProofPower used to require ≜ (hat-equals) for an abbreviation definition but a recent patch allows the standard == to be used. If you are using the 'current release' 2.9.1w2, == is not supported. Can you check the version of ProofPower in the banner that is shown when it starts?


My second question derives from this where right after the
sets I list some axioms which are used to hold globals which I use in
operations throughout the rest of my specification. They rely on the
boolean set I just created or are just parameters for the sets in
general. How would one go about proofing these or is it even necessary?

I'm not sure I understand the question. The axiomatic description involving masterStop and masterReset is referring to the global variable BOOLEAN that was defined to be 0 .. 5 earlier. The constraint holds throughout the theory and is obtained as a theorem by
  z_get_spec %SZT%masterStop%>%

Phil

P.S. A better way to define booleans in Z is as follows:

BOOLEAN == ℙ []
True == [ | true]
False == [ | false]

This is standard Z. I don't know whether FuZZ accepts empty schemas. The main advantage is that the usual logical connectives can be used with such boolean expressions and the implicit conversion of schemas as predicates allows such a boolean expressions to be used where a predicate is required, and giving the expected predicate value. The specification is more readable as a result. For example, your expression

  if (elevatorRightHeading? = 1 ∧ elevatorGoingToFloor? = 1) then ...

could just be

  if elevatorRightHeading? ∧ elevatorGoingToFloor? then ...

To negate a value one can write

  ¬ elevatorRightHeading?

rather than encouraging numerical tricks like

  (1 - elevatorRightHeading?)

Note also that [] is a maximal set, so ℙ [] is too. Consequently type checking ensures that such boolean values can take no other values. Using BOOLEAN == {0, 1}, the constraint is a semantic one: type checking will not reject e.g.

  elevatorRightHeading? = 2

which, presumably, would be a mistake.


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to