Exercícios

1.

Considere o programa da figura 4.2. Faça manualmente a prova do seguinte invariante:

$$l0 \Rightarrow x=0$$

2.

Considere o programa da figura 4.6. Prove manualmente a validade de $\Box x>0$. Prove manualmente a validade de $l2 \Rightarrow x=10$ de acordo com as duas estratégias apresentadas anteriormente. Repita estas provas no STeP.

  

Figure 4.6: Exemplo de um ciclo

local x:int where x=1

l0: while (x<10) do [l1: x:=x+1];
l2:

3.

Considere o programa da figura 4.7, que tem como objectivo fazer a divisão inteira entre x e y, colocando o quociente em z e o resto em w. Prove a correção parcial desse programa, que pode ser especificada através da fórmula

$$l5 \Rightarrow x = z \times y + w \land 0 \leq w < y$$

  

Figure 4.7: Divisão inteira

in x,y : int where x>0 /\ y>0
local t : int where t=x
out z,w : int where (z,w)=(0,0)

l1: while (t>0) do
        l2: if (w+1 = y) 
                then
                l3: (z,w,t) := (z+1,0,t-1)
                else
                l4: (z,w,t) := (z,w+1,t-1);
l5:

4.

Considere o programa da figura que tem como objectivo calcular a parte inteira da raiz quadrada de um número x. Prove a correção parcial desse programa, que pode ser especificada através da fórmula

  

Figure 4.8: Raiz quadrada

in x : int where x>=0
local u,w : int where (u,w)=(1,1)
out z : int where z=0

l0: while (w<=x) do 
        l1: (z,u,w) := (z+1, u+2, w+u+2);
l2:

5.

Prove a exclusão mútua no programa da figura 1.6.

6.

Prove a exclusão mútua no programa da figura 4.9.

  

Figure 4.9: Exclusão mútua com canais

local get, put: channel of bool;

Sem :: [
    local x : bool;
    s1: loop forever do [
        s2: get ==> x;
        s3: put ==> x
    ];
    s4:
]       

||

P1 :: [
    local y : bool where y = true;
    p0: loop forever do [
        p1: noncritical;
        p2: get <== y;
        p3: critical;
        p4: put <== y
    ];
    p5:
]

||

P2 :: [
    local z : bool where z = true;
    m0: loop forever do [
        m1: noncritical;
        m2: get <== z;
        m3: critical;
        m4: put <== z
    ];
    m5:
]