Инвариант петли и вариант для петли

Question

Каким должен быть цикл, инвариантный, а также вариант для данного цикла с точки зрения логики Хоара?

{True}

x := 0; 
y := 0; 
while (x < a) 
  x := x + 2; 
  y := y + 1;

{x = 2 ∗ y}

I thought of variant as (a-x)/2 and loop invariant as (x=2*y & x<=a)but is it correct?

---