Цикл-инвариантная логика Hoare

Question

Каким будет цикл-инвариант для цикла ниже?

{x<7}

while (y < n) {

    y := y + 1;

    x := x + 1;

    if (x = 7) then x := 0 
    else x := x
}
{x<7}

И какой будет вариант для этого же цикла?