During the verification of a program with procedures, when a procedure call is encountered, the procedure's contract is evaluated. We assume that the user has supplied the procedure contracts, although it may also be possible to infer contracts (especially the ensures clause).

In our example, to satisfy the second property of the program, we introduce a boolean variable

boolean loggingOn = false;

The procedure contract for p2() then looks like this:

requires  loggingOn = false
modifies  loggingOn
ensures   loggingOn = false 

Now consider the first property:

(open (read+write)* close)*

In order to define procedure contracts for readContent() and p1() to ensure that this property is satisfied, we introduce an object called FileState which has a typestate. In typestate systems, the type of an object is allowed to change during its lifetime in the computation.

Therefore FileState has type file and two states, open and closed.

Using this notion, we can write the procedure contracts for the two methods as follows:

readContent():
  requires  FileState = open

p1():
  requires  FileState = closed
  modifies  FileState
  ensures   FileState = open