`WP`

refers both to a method to formally verify properties of the analyzed
code and the name of the analyzer’s plug-in that implements this method. WP is a
static analysis technique, like the value analysis, but involving theorem
proving. For a short introduction describing how it works see
Short Introduction to WP Computation.

The purpose of this chapter is mainly to explain in which cases WP can be used with a minimal amount of manual work required. This does not mean that it cannot be used in more complex situations, but then it requires more knowledge about the WP computation and/or competences in performing manual proofs using proof assistants such as Coq.

The easiest way to run WP is to do it in the GUI by selecting the annotation to
prove, right-clicking to open the pop-up menu, and choosing the *Prove Property
by WP* option.

However, when the analysis evolves, it is usually more practical to run WP from the command line, save the project, and extract the status of the properties from the information file to just check that the results are still the same.

The command line to run WP and save the project looks like:

```
tis-analyzer -load project.state -wp-fct f1 -wp-prop f1_p1_wp, f1_p2_wp \
-then -wp-fct g,h -wp-prop f_pre_wp \
...
-then -save project.wp.state
```

This command line:

opens a previously saved project

`project.state`

: it doesn’t need to include value analysis results, and even doesn’t have to include an entry point. All it needs is the body of the functions where the properties to verify are, and probably some specifications for the functions called from these functions.tries to verify the properties named

`f1_p1_wp`

and`f1_p2_wp`

in the`f1`

function,then tries to verify the property

`f_pre`

in`g`

and`h`

.Notice that

`f_pre`

is supposed to be a precondition of`f`

, and that it is checked in`g`

and`h`

which are supposed to be some of`f`

callers;saves the results in the

`project.wp.state`

project.

Notice that a `_wp`

suffix is used in the names of the properties that
are checked with WP. See Naming the Annotations to understand why naming
conventions are useful.

This is an example of how to use WP, but the plug-in provides many other
options if needed. Please use the `-wp-help`

option to list them, and
refer to the documentation for more details.

To know how to extract the status of the properties from the
`project.wp.state`

project, see Information about the Properties.

Let us give very simple explanations about WP for the one that knows nothing about it, because it might be necessary to understand how it works in order to use it when suitable.

To verify that a property is true at a program point, the WP principle
is to propagate it backward and to compute a formula that is such that,
if it can be proved to be true, then it ensures that the initial
property is true as well. The computed formula is then sent to some
automatic prover(s). For instance, `tis-analyzer`

comes with
`alt-ergo`

, but more provers can be added.

An example is easier to understand:

```
const int X = 10;
void f1(int x)
{
int y = x + 1;
int z = 2 * y;
L: //@ assert y_val: y > X;
...
}
```

To ensure that `y_val`

is true at L, WP computes that one have to
prove that `(x+1 > X)`

when entering the function. Notice that the
`z`

assignment has no effect since WP knows that it doesn’t modify
`y`

value. This can be automatically proved if a precondition gives:

```
//@ requires r_x_ge_X: x >= X;
```

This is because the final computed formula is:

```
x >= X ==> x+1 > X;
```

which is easily proved by any automatic prover.

It doesn’t work with the precondition:

```
//@ requires r_x_ge_15: x >= 15;
```

This is because WP only works on the function source code, which means that it has no information about the value of X. To solve this kind of problem, one can add:

```
//@ requires r_X_val: X == 10;
```

This precondition is easily validated by the value analysis and
can be used by WP to finished the proof with `r_x_ge_15`

.

In this simple case, the initial property and the computed formula are
equivalent, but it is not always the case. WP just ensures that **if**
the computed formula is true, **then** the property is true each time
its program point is reached.

To prove a `loop invariant`

property, the WP computation is very
similar, but decomposed into two goals:

- establishment: the property must be true when reaching the loop. This is similar to an assert before the loop.
- preservation: if the property is true at the beginning of an iteration, it is still true at the end.

Example:

```
//@ requires n < 100;
int main(int n)
{
int i; int * p;
for (i = 0, p = T; i < n; i++, p++) {
*p = 3;
}
...
}
```

The following property remove the alarm about the validity of the
`(*p)`

assignment in the loop:

```
//@ loop invariant li_1: p == T+i;
```

Moreover it can be proved by WP:

the establishment has to be proved before entering the loop, but after the initialization part. So the proof obligation is:

T == T + 0

the preservation formula is similar to:

p == T + i ==> p + 1 == T + (i + 1)

Both formula are trivially true.

In the first example in Short Introduction to WP Computation, the `z`

assignment has
no effect on the WP computation since WP knows that it doesn’t modify
`y`

value. But it is different when pointers are involved. For
instance:

```
void f(int * px, int x, int * py, int y)
{
*px = x;
*py = y;
//@ assert a_px: *px == x;
//@ assert a_py: *py == y;
...
}
```

WP is able to prove `a_py`

, but not to prove `a_px`

. The reason is
that it doesn’t know whether the assignment to `(*py)`

modifies
`(*px)`

value or not. The `a_px`

can be proved only with the
precondition:

```
//@ requires \separated (px, py);
```

It tells that there is no intersection between `(*px)`

and
`(*py)`

locations in the memory.

In the context of adding annotations to remove alarms, except in very simple cases, it is not recommended to use WP when possibly overlapping pointers are involved since it may take some time to provide enough information.

The other problem is when there are some function calls between the property and the statements that makes it true. Remember that WP only work on the source code of the property function, and on the specifications of the called functions.

```
extern int X;
void g (void);
void f(int x, int y)
{
if (x > y && x > X) {
g ();
//@ assert ax1: x > y;
//@ assert ax2: x > X;
...
}
...
}
```

WP is able to prove `ax1`

since there is no way for `g`

to modify
either `x`

or `y`

, but `ax2`

cannot be proved since `g`

may
modify `X`

.

There are two solutions to solve the problem:

add an

`assigns`

property for`g`

to specify the modified data.For instance,

`ax2`

is proved when adding://@ assigns \nothing;

This is not the preferred method since

`assigns`

are difficult to prove: it requires to know the modified data for each statement of`g`

. The computed dependencies may help to justify the`assigns`

property, but beware that this information is context dependent.add a postcondition about the involved data. For instance:

specifying that

`X`

is not modified by`g`

://@ ensures X == \old (X);

or specifying that

`X`

decrease://@ ensures X < \old (X);

Both solutions enable to prove `ax2`

.

The WP could seem useless if not used in complex cases, but it is not true: even when properties look trivial, it is useful to formally prove them, since it is so easy to make a mistake.

Let us look at an example:

```
//@ ensures e_res_ok: min <= \result <= max;
int bounds(int min, int x, int max)
{
int res = x;
if (x < min) res = min;
if (x > max) res = max;
return res;
}
```

The postcondition seems reasonably easy to justify, but WP is unable to prove it. WP computes a proof obligation equivalent to:

```
if (x > max) then min <= max /\ max <= max
else if (x < min) then min <= min /\ min <= max
else min <= x /\ x <= max
```

After simplifying the formula, it appears that the information
`(min <= max)`

is missing, so this postcondition cannot be proved
without a precondition. It then has to be added and checked in every
context where the function is called to ensure that the post-condition
is verified.

The advice here is to use WP only in simple cases because complex cases needs expertise and require a lot of time. But we have seen that even for properties that look trivial, it is better to formally prove them, since it is so easy to make a mistake. Moreover, manual justification of trivial properties may look a little silly.

One must be especially careful when it seems that WP **should** be able
to prove something, and doesn’t, since it may hide a problem somewhere.
It is always better to understand if it is really a WP weakness, or
something else.