Z Notation

The Z notation is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general. Developed at Oxford University.

Z Notation for Set Comprehension

For set comprehension, for we have the notation $\{⟨term⟩\cdot ⟨signature⟩\mid ⟨wff⟩\}$

• $⟨term⟩$ = term in Predicate Logic, i.e., an expression using variables and functions that returns a value.
• $⟨signature⟩$ lists the variables used in $⟨term⟩$ and their types, can be omitted if we are doing Untyped Predicate Logic
• $⟨wff⟩$ = any wff formula in predicate logic with the variables used in $⟨term⟩$ as free variables in the formula

$\{x\mid x\in nat\wedge x\le 6\}$ can be written as $\{x•x:nat\mid x\le 6\}$ which can be shortened to $\{x:nat\mid x\le 6\}$.

$\{x+y•x,y:nat\mid x\le 2\wedge y\le 1\}$ is the set $\{0,1,2,3\}$

States

In Z, we think of the execution of a system as a sequence of states (trace) $stat{e}_0\to stat{e}_1\to stat{e}_2\to \dots$ where each state is a mapping from variables (state elements) to values.

We specify the behaviour of the system by describing in logic what are valid steps of the system.

Z Specification

In a Z system specification, we describe:

1. Generic and free types for data manipulated by the system (optional).
2. Constants (elements that aren’t changed by the system) and their types (optional).
3. State space (set of possible states): the system elements, their types and Invariants about relationships between the system elements.
4. Initial state (optional).
5. Operations and how these change the elements of the system
   1. Use $\Delta$NameOfSchema, which is equivalent to writing
      • NameOfSchema
      • NameOfSchema’

Schema Inclusion

We use the schema inclusion to define the initial system state.

Input and Output

In Z, we use the following notation for inputs and outputs:

• “?” as in p? means p? is an input
• “!” as in q! means q! is an output

Local Variable

We can use a local variable, such as in the example below

Exceptions

I will probably need to add this in the exam.

Notice that for the errors, we don’t use a $\Delta$Schema. Rather we use a $\Xi$ “zai” schema to represent the fact that operations on state variables do not change the state.

• You could also just use a standard $\Delta$Schema and just specify that all the states don’t change, but this is much quicker
• You output error! : Errors

Working with Relations

If the tuple is part of a TOTAL function $f$ (you CANNOT do this if it is a non-total function):

• Use $f(x)$ to get the 2nd element associated with $x$

Else (for relation/non-total function)

• Use $R(|\{x\}|)$ to get the SET of possible second elements associated with a 1st element $x$
  • Extract an arbitrary element using $y\in R(|\{x\}|)$

3. Use $dom(R▷\{y\})$ or $R^{\sim }(|\{y\}|)$ to get the SET of possible 1st elements associated with a 2nd element $y$

In Practice

So what I see is that there are a few steps

1. Define your types

[ People,CdnPCs,Ridings ] // Way 1: generic types used in the specification
Errors ::= TooYoung|NotCanadian // Way 2: Enumerated types

2. List Out Constants as a Schema

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

3. List out State Space Schema

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 . x in Voted => Age(x) >= MinAge;;
  // all candidates have to be above minAge
  forall x . x in dom(CandidateToRiding) => Age(x) >= MinAge;;
end

4. List out initial State as a Schema

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

5. Add all of your operations
   1. This is where there are the key logics for your functions
   2. Don’t forget to add exceptions
      1. There should be exception handling schemas for every precondition that can be violated. These schemas can be combined when the same error message is appropriate for multiple exceptions

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 if c in candidates & (forall d . 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