QCP Tutorials Specification Annotations

Shanghai Jiao Tong University Cao Qinxiang Research Group

T1-2 · Specification Annotations

Using Assertion Annotations for Verification

If a program is relatively simple and the property to be verified is also straightforward, QCP can often complete the verification automatically. The examples such as add listed in T1-1 fall into this category. However, when programs become more complex -- even just by including loop structures -- QCP cannot complete the verification automatically. Users can employ assertion annotations to assist QCP in completing the verification. Among all assertion annotations, the most important is the loop invariant annotation.

Example: A Simple Loop

The following program implements addition using a C for loop.

int slow_add(int x, int y)
  /*@ Require
        0 <= x && x <= 100 && 
        0 <= y && y <= 100
      Ensure
        __return == x + y
   */
{
  int i;
  /*@ Inv Assert
        y == y@pre + i && x == x@pre &&
        0 <= i && i <= x@pre &&
        0 <= x@pre && x@pre <= 100 && 
        0 <= y@pre && y@pre <= 100
   */
  for (i = 0; i < x; ++ i) {
    y ++;
  }
  return y;
}

The annotation beginning with Inv Assert is the loop invariant. It states that every time the program checks the for loop condition i < x, the program variables satisfy this condition. This is illustrated in the figure below.

image-1-2
image-1-2

In this assertion, x@pre and y@pre denote the values of the two parameters at the time they were passed into the function. In other words, the assertion states: the current value of y equals the initial value of y plus i, and i is in the range from 0 to x. Based on this loop invariant, QCP only needs to check the following 3 conditions to confirm that this C function indeed implements addition:

  • After the initialization i = 0, the program state satisfies the invariant y == y@pre + i && x == x@pre && 0 <= i && i <= x@pre (properties regarding x@pre and y@pre themselves are omitted here for brevity, and likewise below);
  • If the program state satisfies the invariant y == y@pre + i && x == x@pre && 0 <= i && i <= x@pre and the loop body will be entered (i.e., i < x is true), then after executing the loop body y ++ and ++ i, the loop invariant still holds;
  • If the program state satisfies the invariant y == y@pre + i && x == x@pre && 0 <= i && i <= x@pre and the loop body will not be entered (i.e., i < x is false), then executing the return y statement after the loop guarantees that the Ensure condition __return == x@pre + y@pre holds.

Since x@pre and y@pre are both known to be in the range 0 to 100, it is straightforward to verify that all three properties hold, and QCP can verify this automatically.