Considere o seguinte programa, que visa trocar a posição das entradas x x , y y e z z , de tal forma que transforme uma terna ( x , y , z ) (x,y,z) , ...

Considere o seguinte programa, que visa trocar a posição das entradas x, y e z, de tal forma que transforme uma terna (x,y,z) em (z,x,y):

v1:=x
v2:=y
x:=z
y:=v1
z:=v2

Ao fazer a demonstração de correção desse programa, assinale a alternativa que corresponde à pré-condição da sétima linha a seguir:

{x=a, y=b, z=c}
v1:=x
{v1=a, y=b, z=c}
v2:=y
{v1=a, v2=b, z=c}
x:=z
y:=v1
{x=c, y=a, v2=b}
z:=v2
{x=c, y=a, z=b}