1
$\begingroup$

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?

Improve this question
$\endgroup$
1
  • 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
    Jan 4, 2021 at 3:59

1 Answer 1

Reset to default
0
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

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

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