Many properties hold after some procedure invocations, but do not hold in the initial state and during calls to auxiliary procedures.

To address this question, we can introduce an auxiliary boolean variable 'ok' that determines whether the invariant should be true in the current state or not. Instead of

invariant I(x,y)

we use invariant

invariant (ok --> I(x,y))

To 'turn off' the invariant (e.g. before a call to an auxiliary procedure), simply execute an assignment

x = false;

To 'turn on' the invariant, execute

x = true;

The following code with global invariant successfully verifies, but without the use of 'ok' the invariant would not be true after calling changeX.

var x : Int, y : Int;
var ok : boolean; // used only in specifications
invariant ok --> (0 <= x & x <= y)

proc changeBoth()
requires true
modifies x,y
ensures true
{
  ok = false;
  changeX();
  changeY();
  ok = true;
}

proc changeX()
requires true
modifies x
ensures (x == old(x) + 1)
{
   x = x + 1;
}

proc changeY()
requires true
modifies y
ensures (y == old(y) + 1)
{
   y = y + 1;
}