Dealing with Verification Problems

So you've written your specification and asked Perfect Developer to verify it. After several minutes, the system has successfully discharged most of the proof obligations; but it pronounces that it finds a small number of obligations either unprovable or too hard. What should you do?

Firstly     don't panic.

Press the green button to start calming down, and read on:

It is quite normal to find that a small percentage of obligations is not proven, so that you need to work at achieving 100% proof.

How to start?

A proof obligation may go unproven for either of these reasons:

it may be untrue under some conditions

it may be true under all conditions, but beyond the current capability of Perfect Developer's prover.

Your first task should be to work out for yourself whether you think the obligation is provable in principle from the information available:

How would you persuade a fellow developer that the proof obligation represents a universal truth? Remember that when you are faced with a failed proof obligation within a particular class method, the only things that you (or the prover) can assume when the method is called are that:

The method precondition is satisfied;

The parameters to the method satisfy their type constraints;

The class invariant is satisfied;

The class variables satisfy their type constraints.

If you decide it isn't provable, you need to correct your specification or implementation. Often the correction may be as simple as adding a new precondition, class invariant or post-assertion that you now realize you were assuming all along, but which had not previously been stated.

On the other hand, if you believe that the obligation is provable, then you need to help Perfect Developer find the proof. You do this by splitting the proof into smaller obligations.

Techniques to use:

The following techniques may be used to simplify or split proof obligations, making them easier for both you and Perfect Developer to understand.

When declaring preconditions, assertions, class invariants and loop invariants, declare multiple terms in preference to a conjunction

Whenever you declare a precondition, assertion, class invariant, loop invariant or 'satisfy' condition, Perfect allows you to provide multiple expressions (separated by commas) after the appropriate keyword. This is almost equivalent to bracketing each expression and then combining them using the '&' operator. So declaring:

means the same as:

However, there is one important difference. When multiple comma-separated terms are used, each term will give rise to a separate proof obligation; whereas if you use '&', the entire invariant will be treated as a single term and give rise to a single proof obligation.

It is better to obtain multiple obligations instead of a single, complex obligation. Not only are the individual obligations slightly easier to prove, but if the system fails to prove one of them, the problem term is pinpointed.

Use exact types and declare classes 'final' except where you need to extend them

Consider the fragments:

In the first case, the call x.f(p) is statically bound and the prover can expand the call using the result expression defined in the declaration of f. In the second case, the call y.f(p) is dynamically bound (unless f is declared final in class T or one of its ancestors) and the prover cannot expand the call unless the precise type of y is known at the point of call. The best that the prover can do is to assume any postassertion that was provided in the declaration of f applicable to class T.

If you do need to have a hierarchy of classes derived from class T, you must ensure that sufficient information is declared in the postassertions of all member functions, operators, selectors and schemas to make the required properties provable when these methods are called. Otherwise, it is simplest to declare classes final and not to use from.

Use references only where you need to

References in a specification or implementation make verification much harder. Only use references where you genuinely need two or more references to the same object, such that any change to the object through one reference will become visible through the other(s).

Where there is more than one reference to the same type in some context, consider carefully whether such references should ever be able to refer to the same object. Where the answer is no, add a precondition, class invariant or assertion stating that the references are not equal.

Use intermediate assertions in implementations and expressions

If you have a long implementation and the system fails to prove that the implementation satisfies the specification or yields the correct return value, consider whether you can help the prover by using assertions to state conditions that should be true in between statements. The prover will attempt to prove each such assertion, and each assertion (whether proven or not) will be assumed correct when attempting to prove obligations generated for subsequent statements.

If the location of a proof failure falls immediately after a conditional, try moving the proof obligation into each branch of the conditional

Consider the following:

Suppose the prover reports: "Unable to prove: Specification satisfied at end of implementation" for this schema. Because the implementation ends with a conditional statement, we can split this proof obligation into a separate obligation for each branch, like this:

At any done statement, Perfect Developer will generate the proof obligation that the current state satisfies the postcondition. So we will get one proof obligation for each branch of the if statement, instead of one for the state after executing the if statement.

Here are some variations on this theme, starting with the one we have just illustrated:

Failing obligation	Context	Action
Specification satisfied at end of implementation	Schema implementation ending in if..fi, or done immediately after if..fi	Insert "done;" at the end of each branch of the if..fi
Class invariant satisfied at end of implementation (of a schema or constructor)	As above	As above
Return value satisfies specification	value statement with a conditional expression	Replace "value ([g1]: e1, [g2]: e2, ...)" by "if [g1]: value e1; [g2]: value e2; ... fi"
Assertion valid	assert statement following if..fi	Put a copy of the assert statement at the end of each branch of the if..fi
Precondition satisfied	Method call following if..fi	Determine the exact precondition from the warning message, then append a corresponding assert statement to each branch of the if..fi
Class invariant satisfied at method call	As above	Determine the exact class invariant from the warning message, then append a corresponding assert statement to each branch of the if..fi

If all else fails, try using proof lists in assertions

Any assertion (whether an embedded assertion or a post-assertion) can have a proof list attached like this:

assert e1 proof p1; p2; ... pn end

Each element in the proof list may be either an assertion or a let-declaration. The final element may also be a conditional proof (which is like a conditional statement, except that each branch is a guarded proof list instead of a guarded statement list). See the Language Reference Manual for full details.

The assertions within a proof list are treated as lemmas that the system tries to prove, assuming all previous lemmas in the process. The prover will then attempt to prove the original expression (e1 in this example) assuming all the lemmas.

End of Process Tutorials