george: User Manual

[ Introduction ] [ File Structure ] [ #check PROP ] [ #check PRED ] [ #check PREDTYPES ] [ #check SEM (etc) ] [ #check TP ]
[ #check ND ] [ #check ST ] [ Arithmetic ] [ Sets ] [ #check Z ] [ #check PC ]
[ Contributions by Students ] [ Credits ] [ Keywords ]

Z (#check Z)

A Z specification consists of some type declarations and some schemas. Comments (// ...) can appear anywhere in the specification.

Type Declarations (optional)

There are two kinds of type declarations. The first lists the generic types used in the specification. For example: 

{Books,People}

The second is the enumerated types used in the specification. For example, 

Msg ::= Overdue | Missing

Requests ::= Help | Information

Types cannot be used in expressions within the schemas.

Schemas

Every schema has the form: 

schema Name begin
   signature1
   signature2
   ...
   signaturen
pred
   wff1 ;;
   wff2 ;;
   ...
   wffn ;; 
end

The name of used for describing the initial state constraints must be 'Initial'.

The signature part or the predicate part can be empty.

The predicate part contains well-formed formulas in predicate logic and set theory. Formulas are seperated by ";;". Every a formula must end with ";;".

A signature contains declarations, which can be of the following forms:

Schema Signature
Name
Delta Name
Xi Name
Name: Type
Name?: Type
Name!: Type

The possible types used in a signature are:

Name Syntax
Natural Numbers nat
Power set pow(Q)
Relation P <-> Q
Total Function P --> Q
Total Injective (1-1) Function P >--> Q
Total Surjective (onto) Function P -->> Q
Total Bijective Function P >-->> Q
Non-total Function P -|-> Q
Non-total Injective (1-to-1) Function P >-|-> Q
Non-total Surjective (onto) Function f: P -|->> Q
Non-total Bijective Function P >-|->> Q

Here is an example of a Z specification in george for the voting example: 

   

#u nday
#a 

#check Z

{ People,CdnPCs,Ridings }

Errors ::= TooYoung|NotCanadian

schema Constants begin
  MinAge:nat
  Age:People --> nat
  PC:People -|-> CdnPCs
  Cdns:pow(People)
  Riding:CdnPCs -->> Ridings
pred
  MinAge = 18;;
end

schema VotingSystem begin
  CandidateToRiding:People -|-> Ridings
  VotesForCandidate:People -|-> nat
  RegisteredVoters:Ridings --> pow(People)
  Voted:pow(People)
pred
  // Candidates have to be in both relations
  dom(CandidateToRiding) = dom(VotesForCandidate);;
  // anyone who has voted has to be a registered Voter
  Voted sube gen_U(ran(RegisteredVoters));;
  // Candidates have to be Canadian
  dom(CandidateToRiding) sube Cdns;;
  // Registered Voters have to be Cdn
  gen_U(ran(RegisteredVoters)) sube Cdns;;
  // all voters have to be above minAge
  forall x:People . x in Voted => Age(x) >= MinAge;;
  // all candidates have to be above minAge
  forall x:People . x in dom(CandidateToRiding) => Age(x) >= MinAge;;
end

schema Initial begin
  VotingSystem
pred
  CandidateToRiding = empty;;
  VotesForCandidate = empty;;
  // all ridings have empty sets of registered voters
  ran(RegisteredVoters) = {empty};;
  Voted = empty;;
end

schema AddCandidate begin
  Delta VotingSystem
  candidate?:People
  riding?:Ridings
pred
  // pre: candidate is Canadian
  candidate? in Cdns;;
  // pre: candidate is above minAge
  Age(candidate?) > MinAge;;
  // pre: candidate lives in the riding
  (candidate?, riding?) in PC ; Riding;;
  // pre: not already a candidate
  !(candidate? in dom(CandidateToRiding));;
  // post: add the candidate to the list of candidates
  CandidateToRiding' = CandidateToRiding union {(candidate?, riding?)};;
  VotesForCandidate' = VotesForCandidate union {(candidate?, 0)};;
  RegisteredVoters' = RegisteredVoters;;
  Voted = Voted';;
end

schema RegisterVoter begin
  Delta VotingSystem
  voter?:People
  // riding is a local variable
  riding:Ridings
pred
  // pre: voter is MinAge or over
  Age(voter?) >= MinAge;;
  // pre: voter is Canadian
  voter? in Cdns;;
  // pre: voter has a postal code
  voter? in dom(PC);;
  // figure out the riding of the voter; local var useful here
  (voter?, riding) in PC ; Riding;;
  // pre: voter has not already registered
  !(voter? in RegisteredVoters(riding));;
  // post conditions:
  RegisteredVoters' = RegisteredVoters (+) {(riding, RegisteredVoters(riding) union {voter?})};;
  CandidateToRiding' = CandidateToRiding;;
  VotesForCandidate' = VotesForCandidate;;
  Voted = Voted';;
end

schema Vote begin
  Delta VotingSystem
  voter?:People
  candidate?:People
  // local variable
  riding:Ridings
pred
  // pre: hasn't voted already
  !(voter? in Voted);;
  // voter? has an address
  voter? in dom(PC);;
  // set the value of local var; voter must have an address for this pair to exist
  (voter?, riding) in PC ; Riding;;
  // pre: voter has registered
  voter? in RegisteredVoters(riding);;
  // pre: candidate they want to vote for is a candidate in this riding
  (candidate?, riding) in CandidateToRiding;;
  // post conditions:
  VotesForCandidate' = VotesForCandidate (+) {(candidate?, VotesForCandidate(candidate?) + 1)};;
  Voted' = Voted union {voter?};;
  CandidateToRiding' = CandidateToRiding;;
  RegisteredVoters' = RegisteredVoters;;
end

schema DetermineWinner begin
  Xi VotingSystem
  riding?:Ridings
  winners!:pow(People)
  // local variable
  candidates:pow(People)
pred
  // could be a tie vote, so could have a set of winners
  candidates = dom(CandidateToRiding |> {riding?});;
  candidates != empty;;
  // post condition:
  winners! = { c:People if c in candidates & (forall d:People . d in candidates => VotesForCandidate(c) >= VotesForCandidate(d)) };;
end

schema RegisterVoterTooYoung begin
  Xi VotingSystem
  voter?:People
  error!:Errors
pred
  // pre:
  Age(voter?) < MinAge;;
  // post:
  error! = TooYoung;;
end

schema RegisterVoterNotCanadian begin
  Xi VotingSystem
  voter?:People
  error!:Errors
pred
  // pre:
  !(voter? in Cdns);;
  // post:
  error! = NotCanadian;;
end

What does george check?