Hey!!

Let $\text{Val} = \{0, 1\}^8$, $\text{Adr} = \{0, 1\}^{32}$ and $\text{Mem} = \text{Val}^{\text{Adr}}$.

The addition modulo $2^8$ of two numbers in binary system of length $8$, is given by the mapping:

$$\text{add}_{\text{Val}} : \text{Val}\times \text{Val}\rightarrow \text{Val} \\ (u,v) \mapsto \text{bin}_8 ((\text{Num}_2(u)+\text{Num}_2(v))\mod 2^8)$$

The addition modulo $2^{32}$ of two numbers in binary system of length $32$ and $8$, is given by the mapping:

$$\text{add}_{\text{Adr}} : \text{Adr}\times \text{Val}\rightarrow \text{Adr} \\ (a,v) \mapsto \text{bin}_{32} ((\text{Num}_2(a)+\text{Num}_2(v))\mod 2^{32})$$

A queue is a data structure with the operations „enqueue“, „dequeue“ and „first“.

In our memory model a queue can be represented with at most $2^8$ values by an address. The address and the next field save an pointer at the beginning and the end of the queue. The pointer gives the address relative to the basic address +2.

The mappings init_queue, is_empty, enqueue, dequeue and first are defined as follows:

For each memory $m \in \text{Mem}$, each address $a \in \text{Adr}$ and each value $v \in \text{Val}$, the init_queue(m, a) initializes a queue at $a$ in $m$, is_empty(m, a) checks if the queue at $a$ in $m$ is empty or not, enqueue(m, a, v) places the value $v$ in the queue at $a$ in $m$, dequeue(m, a) takes the oldest value from the queue at $a$ in $m$ and first(m, a) gives the oldest value of the queue at $a$ in $m$.

Let $m\in \text{Mem}$ and $a = \text{bin}_{32}(0)$. I want to compute the value of

first(dequeue(enqueue(enqueue(init_queue(m, a), a, 00101111), a, 00001100), a), a)

First the most inner function is init_queue(m, a). This initializes a queue at $a$ in $m$.

Then we have to compute the mapping enqueue(init_queue(m, a), a, 00101111).

For that we have to compute the $a'=\text{add}_{\text{Adr}}(a,1)$ and $a^{\star}=\text{add}_{\text{Adr}}(a,\text{bin}_8(2))$. How can we do that? I haven't really understood the function $\text{add}$...