2. 
    1. $(\text{even}(x))\wedge x\geq 0$ 
    2. $x\geq 0\wedge y=10(10-x)$
    3. $y\in\{1,2,4,8,16,32,64,128\}$
    4. $\text{allzeros}=(\forall i : 0\leq i < k : a[i]=0)\wedge k\leq N$
    5. $(\text{found}\implies a[k-1]=0)\land k\geq 0$
3. 
    1. We see that $\text{wlp}(x:=x-2)\text{even}(x)=even(x)$, hence $\text{even}(x)$ is a fixed point and the wlp of the loop is $\text{even}(x)$
    2. I will name the statement given above as $T$. I will then define define$$\text{wlp}(T,Q)=\left(g_{1}\implies \text{wlp}(S_1,Q)\right)\wedge \dots \wedge (g_{n}\implies\text{wlp}(S_{n},Q))\wedge ((\neg g_{1}\wedge \dots \wedge \neg g_{n})\implies Q)$$
    3. $a(e_{1} \text{repby} e_{2})[e_{3}]:=e_{1}=e_{3}\to e_{2}|a[e_3]$