Let me just say that this is for a university project. I do not expect an answer but more of a "hint".

I have a schema of a Supermarket that holds a sequence of queues:

+-- Supermarket-------
|queues: seq Queue

And here is how I've defined a queue:

+-- Queue ----------
|length: ℕ

I wish to define a schema that returns the total number of customers, waiting in line. Thus far I have:

|Ξsupermarket: Supermarket
|totalCustomers!: ℕ
|totalCustomers = total θ supermarket

I'm struggling with defining the total function. It needs to "loop" every customer in every queue and sum their lengths. Here is what I have so far: total = q: Queue ⦁ q.length ↦ q.length

Any idea?

  • 1
    $\begingroup$ I am unfamiliar with Z notation, but looking here I believe you can do something in the spirit of $\text{total } s = \text{if } s = \langle\rangle \text{ then } 0 \text{ else } (\text{head } s).\text{length} + (\text{total tail } s)$. $\endgroup$
    – orlp
    Commented Jan 4, 2021 at 3:59

2 Answers 2


I am not aware of the Z notation but here's what you have to do:
step 1: initialize a variable total to 0
step 2: loop through all queues
step 3: add the length of every queue to total


To specify the $\mathit{TotalQueueCustomers}$ operation it helps to know that, in Z (and VDM and B), a sequence is a function from a finite prefix of the positive integers to the element type. Here your element type is $\mathit{Queue}$. To express the sum of the $\mathit{length}$ components of all the $\mathit{Queue}$s in your $\mathit{queues}$ you would want to write the Z-equivalent of this big sum in mathematics: $$\sum_{i=1}^{\#\mathit{queues}}\mathit{queues}(i).length$$ where $\# s$ is the length of sequence $s$ and $z.a$ is component $a$ of schema $z$. Your operation becomes the following.

| ΞSupermarket
| totalCustomers!: ℕ
| totalCustomers! = Σi ∙ (1 ≤ i ≤ #queues | queues(i).length)

Note that it includes just two copies of Supermarket, the plain one and a primed one. No need to give them new names (as you did with supermarket).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.