[an error occurred while processing this directive]

Analytic Verification

Definitions

Preconditions, invariants, and postconditions are all statements about the state of computation in the code near a segment of code. A precondition is a statement placed before the segment that must be true prior to entering the segment in order for it to work correctly. Preconditions are often placed either before loops or at the entry point of functions and procedures. A postcondition is a statement placed after the end of the segment that should be true when the execution of the segment is complete. Postconditions are often placed either after loops or at exit points of functions and procedures.

An invariant is a statement placed in a code segment that should be true each time the the loop execution reaches that point. Invariants are often used in a loops and recursions. In object-oriented programming, invariants can refer to the state of an object, and they should be true at all times except during the execution of methods for the object.

If an invariant is placed at the beginning of a while or do..while loop whose condition test does not change the state of the computation (that is, it has no side effects), then the invariant should also be true at the bottom of the loop.

Using Preconditions, Postconditions, and Invariants to Check Loops

The correctness of a loop can be ascertained by making the following sequence of checks:

If the loop satisfies the above checks then the postcondition must be true whenever the precondition is true, provided that the loop terminates. Since it it possible for a loop to run forever, one more check is needed:

An Example: The Graph Search Algorithm

The following iterative algorithm searchs the vertices and edges of a graph that are reachable from the starting vertex v. Bookkeeping about visitation is omitted. 
    visit v
    put all of the edges that leave v into the dispenser
    -- Preconditions:
        -- v is visited.  Every other vertex in the graph is unvisited.
        -- Every edge in the graph that goes from v to another vertex
        -- is in the dispenser.
    while the dispenser is not empty
        -- Invariant:
            -- Every edge in the graph that goes from a visited
            -- vertex to an unvisited vertex is in the dispenser.
        retrieve and remove edge e from the dispenser
        let w be the head of e
        if w has not been visited
            visit e
            visit w
            put all of the edges that leave w into the dispenser
        endif
    endwhile
    -- Postcondition:
        -- There are no edges in the graph that go from a
        -- visited vertex to an unvisited vertex.

Checking Correctness of the Graph Search Algorithm

Here, the invariant is just a rephrasing of the precondition.

This means that you assume that the invariant is true at the beginning of the loop body, and you check that it must therefore be true at the end. Usually, the invariant is falsified early in the loop code in order to make progress towards termination, and the remaining code is designed to reestablish the invariant.

For the graph search loop, the truth of the invariant can be changed in two ways: an edge can be added or removed from the dispenser, or the visited status of its end vertices can be changed. There are two cases to consider, depending on the truth of the if statement condition.

If the head of e has not been visited then the removal of e from the dispenser can falsify the invariant. But then later code changes the status of its head vertex so that at the end of the loop the removed edge does not go from a visited vertex to an unvisited vertex. Changing the status of the head vertex to visited also can make more edges that go from visited vertices to unvisited vertices, but all edges that leave the head of e are added to the dispenser, so the invariant is not falsified in the end.

If the head of e has been visited then its removal does not falsify the invariant. And in this case, the visited status of vertices is unchanged, so the invariant remains true.

If the dispenser is empty (this is the loop termination condition), and it contains all edges in the graph that go from a visited vertex to an unvisited vertex (this is the invariant), then there cannot be any such edges in the graph.

A vertex can only be visited once due to the if statement inside the loop. Since an edge is only entered into the dispenser when its head vertex is visited, and each iteration of the loop removes one edge, the number of iterations is bounded by the number of directed edges in the graph.

In the graph search algorithm, the precondition is guaranteed by the code preceding the loop, so the postcondition is always ensured.

Conclusion

One important conclusion can be drawn from the postcondition for the graph search: if there is a path from v to a vertex w in the graph then the algorithm must visit w. To see this, suppose that it is false. Then there must be a first unvisited vertex x along the path. x cannot be v since v is visited. But this is impossible since it implies that there is an edge from a visited vertex to an unvisited vertex - the edge in the path that leads to x.

This conclusion could have been used as the postcondition. In fact, it is a better postcondition because it addresses the purpose of the graph search more directly.

[an error occurred while processing this directive]