# Z Notation: sequence of sequences - find sum

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:

+--TotalQueueCustomers----
|Ξ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?

• 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)$.
– orlp
Commented Jan 4, 2021 at 3:59

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.

+-TotalQueueCustomers------------------------------------------------
| Ξ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).