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.

## Advertising

`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