[ a < b ]
x := a;
[ a < b, x = a ]
y := b;
[ a < b, x = a , y = b]

[ a + b <= 2y-2 < a + b + 1] #invarianta

while x < y do
[ x < y, a + b <= 2y-2 <= a + b + 1]
x := x + 1;
[x + 1 < y, a + b <= 2y-2 <= a + b + 1]
y := y - 1
[x + 1 < y - 1, a + b <= 2y-4 <= a + b + 1]
done
[ x + 1 < y - 1, a + b <= 2y-4 <= a + b + 1, x >= y]
[ x + 1 < y - 1, a + b <= 2y-4 <= a + b + 1, x > y - 1]
[ x < y - 2, a + b <= 2y-4 <= a + b + 1, x > y - 1]
[ a + b <= 2x <= a + b + 1]