Verification: Loop's PC

Considering the next program:

int foo(intx) {
     while (x < 2)_Invariant(x <= 5) {
          x = x + 1;
     }
     _Assert(x);
     return x;
}

If I’m not mistaken, the precondition of this program is the invariant (x <= 5) using the lecture script’s rules. When I want to check the correctness of a program, I need to check that PC and all VCs are valid.

The program itself seems to be correct without any assumption. However, its pre-condition can be unsatisfied when x > 5.
It is reasonable, since inputs greater than 5 are not models of preconditions, and hence we should assume x<=5, i.e. assume the invariant.

Was the mistake that I didn’t assume the invariant? If no, then what is my mistake?

My takeaway from the lecture notes is that you simply can’t mechanically prove partial or total correctness for while-programs unless you use invariant and termination annotations and even then you need good ones.

I calculated pc ... true = x <= 5 and vc ... true = true . Basically mechanized verification tells you, given your invariant annotation, that the program terminates and x == 0 if you start with x <= 5.

Ask yourself this question: If you used the invariant False would you expect the verifier to tell you that the program is (partially) correct?

1 Like

A more sensible invariant would be \mathtt{true}. I think this should work.

Yes, you need to pick invariant cleverly. Most don’t work.

1 Like

In case this helps: If you let the invariant vary (let’s call it i) you get this:

pc ... true = i
vc ... true = (x < 2) => i => i[x+1/x]

So verifying the program for every input requires i(x) to be true for all values of x. The conjunction of pc and vc is:

total = i && ((x < 2) => i => i[x+1/x]) = (i && x >= 2) || (i && i[x+1/x])

Using some stolen notation:

V(p) = \{x \in \mathbb{Z}\mid p(x)\}

for a predicate p\colon \mathbb{Z} \to \text{bool}, we get:

V(total) = \{x\in \mathbb{Z}\mid x \ge 2 \wedge i(x)\} \cup \{x \in \mathbb{Z}\mid i(x) \wedge i(x+1)\}

Basically it looks like induction but the predicate i is “reverse”-inductive, i.e. \forall x^\mathbb{Z}.i(x) \Rightarrow i(x - 1). If instead you had that \forall x^\mathbb{Z}.i(x) \Rightarrow i(x + 1) one of the following holds:

  • V(i) = \emptyset, i.e i = \text{false}.
  • V(i) = \mathbb{Z}, i.e. i = \text{true}.
  • \emptyset \subset V(i) \subset \mathbb{Z}, by which I mean proper inclusions.

In the last case I claim that V(i) must have a least element.

Proof: Assume V(i) had no least element. Let x\in V(i), which exists since V(i)\neq \emptyset, and y\in\mathbb{Z}. If x\le y we get y\in V(i) by the inductive property of i. Otherwise we have y < x, but y can not be less than all elements of V(i) because otherwise V(i)\subseteq \mathbb{Z}_{>y}, i.e. V(i) would have a least element, a contradiction. (Note: subsets of well-ordered sets with the induced order are well-ordered again; \mathbb{N} \cong \mathbb{Z}_{>y} as posets via shifting)
Thus there is x_0\in V(i) s.t. x_0 <= y, but by the inductive property of i this yields x\in V(i). As x was arbitrary we get that V(i) = \mathbb{Z}, a contradiction. \square

This means that there is v\in V(i) s.t. V(i) = V(v \le x), and hence:

V(total) = \{x\in \mathbb{Z} \mid v \lor 2 \le x\} \cup \{x \in \mathbb{Z}\mid v \le x\} = V(v \le x)

For the original “reverse”-inductive predicate i the negation \neg i must be inductive, hence V(\neg i) = V(v < x) for some v\in V(\neg i). Applying the rule V(\neg p) = V(p)^c gives that V(i) = V(x \le v). Then V(total) = V(2 \le x \le v) \cup V(x < v) which is either V(x < v) or V(x \le v).

I can’t fully judge what I came up with (too many things are static, like the assertion at the end, the loop body being empty except for the increment, etc.), but the intuition I get from it is that if you make your invariant inductive/“reverse”-inductive you can either prove correctness for all inputs or the set of inputs where you can’t prove correctness is necessarily infinite.

1 Like