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 in Predicate Logic, i.e., an expression using variables and functions that returns a value.
  • lists the variables used in and their types, can be omitted if we are doing Untyped Predicate Logic
  • = any wff formula in predicate logic with the variables used in as free variables in the formula

can be written as which can be shortened to .

is the set


In Z, we think of the execution of a system as a sequence of states (trace) 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 NameOfSchema, which is equivalent to writing
      • NameOfSchema
      • NameOfSchema’

Schema Inclusion

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

Screen Shot 2022-12-11 at 4.52.47 PM.png

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 Screen Shot 2022-12-11 at 4.54.20 PM.png


I will probably need to add this in the exam.

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

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

Screen Shot 2022-12-11 at 5.42.08 PM.png

Working with Relations

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

  • Use to get the 2nd element associated with

Else (for relation/non-total function)

  • Use to get the SET of possible second elements associated with a 1st element
    • Extract an arbitrary element using
  1. Use or to get the SET of possible 1st elements associated with a 2nd element

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
  1. List Out Constants as a Schema
schema Constants begin
  Age:People --> nat
  PC:People -|-> CdnPCs
  Riding:CdnPCs -->> Ridings
  MinAge = 18;;
  1. List out State Space Schema
schema VotingSystem begin
  CandidateToRiding:People -|-> Ridings
  VotesForCandidate:People -|-> nat
  RegisteredVoters:Ridings --> pow(People)
  // 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;;
  1. List out initial State as a Schema
schema InitialVotingSystem begin
  CandidateToRiding = empty;;
  VotesForCandidate = empty;;
  // all ridings have empty sets of registered voters
  ran(RegisteredVoters) = {empty};;
  Voted = empty;;
  1. 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
  // 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';;
schema RegisterVoter begin
  Delta VotingSystem
  // riding is a local variable
  // 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';;
schema Vote begin
  Delta VotingSystem
  // local variable
  // 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;;
schema DetermineWinner begin
  Xi VotingSystem
  // local variable
  // 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)) };;
schema RegisterVoterTooYoung begin
  Xi VotingSystem
  // pre:
  Age(voter?) < MinAge;;
  // post:
  error! = TooYoung;;
schema RegisterVoterNotCanadian begin
  Xi VotingSystem
  // pre:
  !(voter? in Cdns);;
  // post:
  error! = NotCanadian;;