1 Method Calls

1.1 Method Calls

Method Calls Method Calls

Slide 1

Method Calls

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 1 / 25

1
 Method Calls Method Calls

An Example Program with a Method Call

1 void sort(int[] b)
2 // PRE: b 6= null (P1 )
3 // POST: b[..) ∼ b[..)pre ∧ Sorted( b[..) ) (Q1 )
4 {
5 ...
6 }
Slide 2

7
8 int smallest(int[] a)
9 // PRE: a 6= null ∧ a.length > 0 (P2 )
10 // POST: r = min( a[..)pre ) (Q2 )
11 {
12 // MID: a[..) ≈ a[..)pre ∧ a 6= null ∧ a.length > 0 (M1 )
13 sort(a);
14 // MID: a[..) ∼ a[..)pre ∧ Sorted( a[..) ) ∧ a.length > 0 (M2 )
15 int res = a[0];
16 // MID: a[..) ∼ a[..)pre ∧ res = min( a[..) ) (M3 )
17 return res;
18 }

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 2 / 25

The code above does not modify the input parameter a, so you do not need to distinguish
between a, apre or aold throughout.
However, this program can potentially update the contents of the array a, so we do have
to take some care to track the values of these contents throughout.
Up until the point where we call sort(a) we can see that the array’s contents are unmodi-
fied, but after this method call we only know that the array’s contents are a permutation
of its original contents.

2
 Method Calls Method Calls

Reasoning about Method Calls

How do we show that a method call satisfies its caller’s specification?
1 // MID: P
2 someMethod(v1 , ..., vn );
3 // MID: Q
We have to show that P satisfies the method’s pre-condition and that in
Slide 3

turn the method’s post-condition satisfies Q.

P −→ R[ x 7→ v ]
P [ v[..) 7→ v[..)old ] ∧ S[ x 7→ v ][ v[..)pre →
7 v[..)old ] −→ Q
{ P } someMethod(v1 , ..., vn ); { Q }
where
void someMethod(type x1 , ..., type xn )
// PRE: R
// POST: S
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 3 / 25

Recall that we use the notation x to refer to the abstract variables x1 , ..., xn in the
method’s specification and similarly v to refer to the concrete values v1 , ..., vn used at
its call point in our code.
Recall also that we write P [ x 7→ y ] to represent the predicate P with all free occurrences
of x replaced with y.
The substitutions of [ x 7→ v ] in R and S ensure that we replace the abstract variables in
the method’s specification with the concrete values used at its call point in our code.
The additional substitutions of [ v[..) 7→ v[..)old ] in P and [ v[..)pre 7→ v[..)old ] in S account
for the potential update in program state caused by the method call. We have to take
particular care with the method post-condition S to remember that any reference to an
array’s contents a[..)pre refers to the contents of that array before the method is called.
Java is call by value, so no variable of any primitive type (int, bool, char, etc.) can be
updated by the method call. However, when we pass variables of reference type (in this
course just arrays, but in general any object reference) the contents of these references
can be updated.
i.e. when we pass an array to a method, we could modify the contents of that array (but
not the array reference itself).
Important: the substitutions [ v[..)pre 7→ v[..)old ] in S takes place after the call value
substitutions [ x 7→ v ] to ensure that there is no ambiguity in the effect of these two sets
of substitutions.

3
 Method Calls Method Calls

Reasoning about Method Calls

To reason about a method call:
we must show that pre-condition R[ x 7→ v ] is established before the call
we may assume that post-condition S[ x 7→ v ] will hold after the call
1 code1;
2 // MID: P
Slide 4

3 someMethod(v1 , ..., vn );
4 // MID: Q
5 code2;
where
void someMethod(type x1 , ..., type xn )
// PRE: R
// POST: S
It is the ”responsibility” of code1 to establish R[ x 7→ v ] through P .
In return, code2 may assume S[ x 7→ v ] “for free” as part of Q.
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 4 / 25

In practice, we will usually need to hold on to some additional information about the
state that is not affected by the method call. This will be captured by P and Q in the
above proof outline.

4
 Method Calls Method Calls

Method Call - Example

1 void sort(int[] b)
2 // PRE: b 6= null (P1 )
3 // POST: b[..) ∼ b[..)pre ∧ Sorted( b[..) ) (Q1 )
4 {
5 ...
6 }
Slide 5

7
8 int smallest(int[] a)
9 // PRE: a 6= null ∧ a.length > 0 (P2 )
10 // POST: r = min( a[..)pre ) (Q2 )
11 {
12 // MID: a[..) ≈ a[..)pre ∧ a 6= null ∧ a.length > 0 (M1 )
13 sort(a);
14 // MID: a[..) ∼ a[..)pre ∧ Sorted( a[..) ) ∧ a.length > 0 (M2 )
15 int res = a[0];
16 // MID: a[..) ∼ a[..)pre ∧ res = min( a[..) ) (M3 )
17 return res;
18 }

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 5 / 25

Method Calls Method Calls

Reasoning about smallest - Proof Obs. (Informal)

The correctness of the smallest method relies on the following argument:
line 12: The pre-condition of smallest must establish the mid-condition M1 .
i.e. P2 −→ M1
line 13: The mid-condition M1 must establish the pre-condition of sort.
i.e. M1 −→ P1
Slide 6

line 14: The post-condition of sort must establish the mid-condition M2 .

i.e. M1 ∧ Q1 −→ M2
line 16: The mid-condition M2 and code must establish mid-condition M3 .
i.e. M2 ∧ int res = a[0]; −→ M3
line 18: The mid-condition M3 and return code must establish the
post-condition of smallest.
i.e. M3 ∧ return res; −→ Q2
Important: care must be taken to track the effects of the code.
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 6 / 25

5
 Method Calls Method Calls

Reasoning about smallest - Care with Variables

Remember, a naive translation of the arguments can lead to incorrect

proof obligations.

We must carefully track which variable values we are referring to. Are they
current values, old values or initial values with respect to the code?
Slide 7

We achieve this by substituting the variables in method specifications (pre-

and post-conditions) by the arguments that were passed to them and by
tracking the state modified by the code

e.g. on line 14, when we use the post-condition of sort to establish M2 ,

we are given:

Q1 [ b 7→ a, b[..)pre 7→ a[..)old ] ←→ a[..) ∼ a[..)old ∧ Sorted( a[..) )

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 7 / 25

6
 Method Calls Method Calls

Reasoning about smallest - Proof Obs. (Explicit)

The correctness of the smallest method relies on the following argument:
line 12: The pre-condition of smallest must establish the mid-condition M1 .
( P2 [ a[..) 7→ a[..)pre ] ∧ a[..) ≈ a[..)pre ) −→ M1
line 13: The mid-condition M1 must establish the pre-condition of sort.
M1 −→ P1 [ b 7→ a ]
Slide 8

line 14: The post-condition of sort must establish the mid-condition M2 .

( M1 [ a[..) 7→ a[..)old ] ∧ Q1 [ b 7→ a, b[..)pre 7→ a[..)old ] ) −→ M2
line 16: The mid-condition M2 and code must establish mid-condition M3 .
( M2 [ res 7→ resold ] ∧ res = a[0] ) −→ M3
line 18: The mid-condition M3 and return code must establish the
post-condition of smallest.
( M3 ∧ r = res ) −→ Q2 [a 7→ apre ]

Important: we only substitute non identity cases.

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 8 / 25

We discuss the development of each of these proof obligations over the following slides.
The exact number of obligations which we will have to prove is determined by the number
of mid-conditions in our code and the number of method calls we make.
Each mid-condition will require a corresponding proof obligation to establish that it
holds. Each method call will require an additional proof obligation to establish that the
method’s pre-condition.

7
 Method Calls Method Calls

Reasoning about smallest - Proof Obs. (Final)

line 12: The pre-condition of smallest must establish the mid-condition M1 .

( P2 [ a[..) 7→ a[..)pre ] ∧ a[..) ≈ a[..)pre ) −→ M1
Slide 9

a 6= null ∧ a.length > 0 ∧ a[..) ≈ a[..)pre

−→
a[..) ≈ a[..)pre ∧ a 6= null ∧ a.length > 0

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 9 / 25

In this first obligation we have to remember that the pre-condition P2 only describes the
variables that were passed into the method call. In order to use the pre-condition in our
proof, we must substitute all of the variables for their initial pre versions.
Moreover, as no code has been executed so far in the method, we gain the implicit
information that a[..) ≈ a[..)pre .

8
 Method Calls Method Calls

Reasoning about smallest - Proof Obs. (Final)

line 13: The mid-condition M1 must establish the pre-condition of sort.

M1 −→ P1 [ b 7→ a ]
Slide 10

a[..) ≈ a[..)pre ∧ a 6= null ∧ a.length > 0

−→
a 6= null

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 10 / 25

In this proof obligation, the [ b 7→ a ] substitution for P1 on line 13 is handling the fact
that the sort method is defined in terms of the integer array parameter b, but it has
been called with the integer array reference a.
We always have to perform this substitution of the abstract variables from the method’s
specification to the concrete values used in the method call in the code we are reasoning
about.
In this obligation no code is actually being executed, so we do not need to worry about
the current (x) or old (xold ) states of the variables.

9
 Method Calls Method Calls

Reasoning about smallest - Proof Obs. (Final)

line 14: The post-condition of sort must establish the mid-condition M2 .

( M1 [ a[..) 7→ a[..)old ] ∧ Q1 [ b 7→ a, b[..)pre 7→ a[..)old ] ) −→ M2
Slide 11

a[..)old ≈ a[..)pre ∧ a 6= null ∧ a.length > 0

∧ a[..) ∼ a[..)old ∧ Sorted( a[..) )
−→
a[..) ∼ a[..)pre ∧ Sorted( a[..) ) ∧ a.length > 0

This proof relies on the following property:

a[..) ∼ b[..) ∧ b[..) ≈ c[..) −→ a[..) ∼ c[..)

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 11 / 25

In this obligation we are considering the effect of the call to the sort method. This means
that we must track the state of the input array both before and after the method call.
The same ”call value for specification variable” substitution as in the previous proof
obligation from line 13 ([ b 7→ a ]) is happening for Q1 in this proof obligation for line 14.
However, in this case we also have the extra substitution [ b[..)pre 7→ a[..)old ], which is
handling the fact that we are passing an array reference into the varsort method.
The Java method call semantics (”call by value”) ensures that the call to sort cannot
modify the variables for any primitive type (int, bool, char, etc.).
Similarly, sort cannot change the value of a reference variable (e.g. a in our example),
but the contents of such a reference (e.g. the array elements) could be updated (indeed,
they are rearranged in this example).
This means that some care is needed to track what is going on.
The [ b[..)pre 7→ a[..)old ] substitution is helping us with this. It says that any reference
to the initial/provided array contents (b[..)pre ) in the post-condition of sort is actually
referring to the contents of the array a at the point the method call was made (i.e.
a[..)old ). This allows us to carry though information about the array’s contents from the
mid-condition M1 (note the similar substitution occurring there), as we still know what
the state of the program was before the method call.

10
 Method Calls Method Calls

Reasoning about smallest - Proof Obs. (Final)

line 16: The mid-condition M2 and code must establish mid-condition M3 .

( M2 [ res 7→ resold ] ∧ res = a[0] ) −→ M3
Slide 12

a[..) ∼ a[..)pre ∧ Sorted( a[..) ) ∧ a.length > 0 ∧ res = a[0]

−→
a[..) ∼ a[..)pre ∧ res = min( a[..) )

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 12 / 25

This obligation concerns the execution of the code int res = a[0]; which is a variable
declaration and assignment instruction. This means that we need to track the current
and old values of any variables modified by the code.
However, the variable res does not actually exist before this code is executed, so there
are no statements about the value of this variable in M2 and thus the substitution does
not actually change M2 at all.

11
 Method Calls Method Calls

Reasoning about smallest - Proof Obs. (Final)

line 18: The mid-condition M3 and return code must establish the
post-condition of smallest.
( M3 ∧ r = res ) −→ Q2 [a 7→ apre ]
Slide 13

a[..) ∼ a[..)pre ∧ res = min( a[..) ) ∧ r = res

−→
r = min( apre [..)pre )

(Don’t forget a = apre throughout this program)

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 13 / 25

This last obligation simply tracks the assignment of the return value for the method. As
this assignment has no other side effects, we do not need to track the old values of any of
our program state. However, we do need to be sure that the method’s post-condition is
satisfied w.r.t. the original input parameter values (remember that Java is call-by-value).
Thankfully, this still results in a fairly straightforward proof obligation, so long as we
remember the the code does not modify the input array reference parameter a. Thus, we
can freely assume that a = apre throughout the method’s body.

12
 Method Calls Method Calls

What about sort?

We have been able to reason about the correctness of smallest without

knowing the implementation details of sort
Slide 14

This is known as modular verification

We have assumed that sort satisifes its specification

but could there still be a problem...?

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 14 / 25

Modular verification is a very helpful property of our program reasoning, as this allows
us to break down complex systems into smaller, more manageable chunks.
We can then reason about these chunks independently (with each chunk assuming that
the others satisfy their specifications) and once all chunks have been verified we can then
establish the correctness of the whole system.

13
 Method Calls Method Calls

What about sort?

Can anyone propose a problematic implementation of the sort method

that still satisfies its specification?
1 void sort(int[] b)
// PRE: b 6= null (P1 )
Slide 15

3 // POST: b[..) ∼ b[..)pre ∧ Sorted( b[..) ) (Q1 )

4 {
5

7 sort(b);
8

10 }

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 15 / 25

Recall that our intuitive interpretation of the Hoare Triple

{ P } code { Q }
is of the form:

“If property P holds before the execution of code, then after the execution
of code property Q will hold”.

The problem here is that we are only verifying the behaviour of our code after it has
executed. If our code never terminates, then we have nothing to prove.
This is known as the “Partial Correctness Interpretation of Hoare Triples”.
If we care also about guaranteeing termination, then we would be talking instead about
Total Correctness.

14
 Method Calls Method Calls

Total vs. Partial Correctness

Partial Correctness: if the code is executed in a state satisfying its

precondition, then if it terminates it must reach a state that satisfies its
postcondition.
Slide 16

Total Correctness: as partial correctness above, but we also know that the
code will terminate.

Why do we distinguish between partial correctness and total correctness?

Some reasons include:

Different Proof Obligations
Desired Property Types
Non-Terminating Code

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 16 / 25

There are several reasons why we distinguish between partial and total correctness.
Firstly, depending on the code in question, it may be quite hard to prove one of partial
correctness or termination, even though the other might be easy. In fact, in some cases
one of these proofs might actually be impossible (e.g. The Halting Problem).
Secondly, there might be some properties of your code that are more important to you
than termination. For example, you might not know if your code will terminate, but still
want to be able to prove that if it does terminate then it will have solved your problem.
Thirdly, there are some pieces of code that are legitimately non-terminating (web-servers,
operating systems, etc...) but we may still want or need to verify their correctness.
There are probably also many other good reasons for the distinction.

15
 Method Calls Method Calls

Reasoning about Method Calls

What if the method has a return value?
1 // MID: P
2 res = someMethod(v1 , ..., vn );
3 // MID: Q
Just as with assignment, we must carefully track the modification of the
Slide 17

variable res. This requires some additional substitutions in our assertions:

 P −→ R[ x 7→ v ] 
P [ v[..) 7→ v[..)old ][ res 7→ resold ] ∧ res = r
−→ Q
∧ S[ x 7→ v ][ v[..)pre 7→ v[..)old ][ res 7→ resold ]
{ P } res = someMethod(v1 , ..., vn ); { Q }
where
type someMethod(type x1 , ..., type xn )
// PRE: R
// POST: S
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 17 / 25

The additional substitutions of [ res 7→ resold ] in S and P and the extra conjunct res = r
account for the update in program state caused by the assignment of the method’s return
value. The rest of the rule is the same as before.
Important: the substitution [ res 7→ resold ] must take place after all other substitutions
to properly reflect the order of execution of the code. That is, the method is run in a
state where the variable res still has its old value.

16
 Method Calls Method Calls

Reasoning about Method Calls with Returns

To reason about a method call with a return value:
we must show that pre-condition R[ x 7→ v ] is established before the call
we may assume that post-condition S[ x 7→ v ] will hold after the call
and also that res = r after the call
1 code1;
Slide 18

2 // MID: P
3 res = someMethod(v1 , ..., vn );
4 // MID: Q
5 code2;
where
type someMethod(type x1 , ..., type xn )
// PRE: R
// POST: S
It is the ”responsibility” of code1 to establish R[ x 7→ v ] through P .
In return, code2 may assume S[ x 7→ v ] ∧ res = r “for free” in Q.
Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 18 / 25

The requirements on the pre-condition are the same as in the case where there is not
return value, but we have an additional update to the program state to be aware of after
the call is complete.

17
 Method Calls Method Calls

Method Call with Return - Example

1 int increment(int i) int decrement(int i)
2 // PRE: true (Pinc ) // PRE: true (Pdec )
3 // POST: r = i + 1 (Qinc ) // POST: r = i − 1 (Qdec )
4 { ... } { ... }
5
6 int pointlessUpDown(int x)
Slide 19

7 // PRE: true (P )
8 // POST: r = x (Q)
9 {
10 x = increment(x);
11 // MID: x = xpre + 1 (M1 )
12 x = decrement(x);
13 // MID: x = xpre (M2 )
14 return x;
15 }

We assume that both increment and decrement are totally correct

w.r.t their respective method specifications

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 19 / 25

The code above does modify the input parameter x, so we will need to be careful to track
the value of this variable throughout.

18
 Method Calls Method Calls

Reasoning about pointlessUpDown - Proof Obs.

The correctness of pointlessUpDown relies on the following argument:
line 10: The pre-condition of pointlessUpDown must establish the
pre-condition of increment.
( P [ x 7→ xpre ] ∧ x = xpre ) −→ Pinc [ i 7→ x ]
Slide 20

line 11: The post-condition of increment must establish mid-condition M1 .

( (P [ x 7→ xpre ] ∧ x = xpre )[ x 7→ xold ] ∧ Qinc [ i 7→ xold ] ∧ x = r ) −→ M1
line 12: The mid-condition M1 must establish the decrement pre-condition .
M1 −→ Pdec [ i 7→ x ]
line 13: The post-condition of decrement must establish mid-condition M2 .
( M1 [ x 7→ xold ] ∧ Qdec [ i 7→ xold ] ∧ x = r ) −→ M2
line 15: The mid-condition M2 and return code must establish the
post-condition of pointlessUpDown.
( M2 ∧ r = x ) −→ Q[x 7→ xpre ]

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 20 / 25

We discuss the development of each of these proof obligations over the following slides.
By omitting the trivial mid-condition before the method call to increment we avoid
having to establish that this holds. However we do still have to prove that the pre-
condition of increment holds before it is called and must now establish this directly
from the pre-condition of pointlessUpDown.
The method call to decrement incurs an extra proof obligation that checks that its pre-
condition is satisfied before it is called (as usual), but we will see that this is relatively
trivial in this instance.

19
 Method Calls Method Calls

Reasoning about pointlessUpDown - Proof Obs.

line 10: The pre-condition of pointlessUpDown must establish the

pre-condition of increment.
( P [ x 7→ xpre ] ∧ x = xpre ) −→ Pinc [ i 7→ x ]
Slide 21

true ∧ x = xpre
−→
true

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 21 / 25

In this first obligation we have to remember that the pre-condition P only describes the
variables that were passed into the method call. In order to use the pre-condition in our
proof, we must substitute all of the variables for their initial pre versions.
Moreover, as no code has been executed so far in the method, we gain the implicit
information that x = xpre . We also do not need to worry about the current (x) or old
(xold ) states of the variables.
However, we do need to substitute the call value of x into the pre-condition Pinc of the
increment method.

20
 Method Calls Method Calls

Reasoning about pointlessUpDown - Proof Obs.

line 11: The post-condition of increment must establish mid-condition M1 .

( (P [ x 7→ xpre ] ∧ x = xpre )[ x 7→ xold ] ∧ Qinc [ i 7→ xold ] ∧ x = r ) −→ M1
Slide 22

true ∧ xold = xpre ∧ r = xold + 1 ∧ x = r

−→
x = xpre + 1

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 22 / 25

In this obligation we are considering the effect of the call to the increment method. This
means that we must track the state of the program both before and after the method
call. Thus, in the post-condition Qinc we replace the method’s argument variable i with
the call value x.
Note that as well as knowing the post-condition of the increment method, we also still
know what the state of the program was before the method call, which in this case was
actually the precondition P .
We must remember that the pre-condition P only describes the variables that were passed
into the pointlessUpDown method call. So, as before, in order to use the pre-condition
in our proof, we must substitute all of the variables for their initial pre versions.
Again, since no code was executed before our increment method call, we had the implicit
information that x = xpre before the call. However, we must also update any reference to
the variable x from before the method call to xold to reflect that x is assigned the return
value of the increment method call by the code.

21
 Method Calls Method Calls

Reasoning about pointlessUpDown - Proof Obs.

line 12: The mid-condition M1 must establish the decrement pre-condition .

M1 −→ Pdec [ i 7→ x ]
Slide 23

x = xpre + 1
−→
true

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 23 / 25

In this obligation no code is actually being executed, so we do not need to worry about
the current (x) or old (xold ) states of the variables.
However, we do need to substitute the call value of x into the pre-condition Pdec of the
decrement method.

22
 Method Calls Method Calls

Reasoning about pointlessUpDown - Proof Obs.

line 13: The post-condition of decrement must establish mid-condition M2 .

( M1 [ x 7→ xold ] ∧ Qdec [ i 7→ xold ] ∧ x = r ) −→ M2
Slide 24

xold = xpre + 1 ∧ r = xold − 1 ∧ x = r

−→
x = xpre

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 24 / 25

In this obligation we are considering the effect of the call to the increment method. This
means that we must track the state of the program both before and after the method
call. Thus, in the post-condition Qdec we replace the method’s argument variable i with
the call value x.
Note that as well as knowing the post-condition of the decrement method, we also still
know what the state of the program was before the method call (i.e. M1 ). However, we
must update any reference to the variable x from before the method call to xold to reflect
that x is assigned the return value of the increment method call by the code.

23
 Method Calls Method Calls

Reasoning about pointlessUpDown - Proof Obs.

line 15: The mid-condition M2 and return code must establish the
post-condition of pointlessUpDown.
( M2 ∧ r = x ) −→ Q[x 7→ xpre ]
Slide 25

x = xpre ∧ r = x
−→
r = xpre

Drossopoulou & Wheelhouse (DoC) Discrete Mathematics, Logic & Reasoning 25 / 25

This last obligation simply tracks the assignment of the return value for the overall
pointlessUpDown method. As this assignment has no other side effects, we do not need
to track the old values of any of our program state.
However, we do need to be sure that the method’s post-condition Q is satisfied w.r.t. the
original value for the integer input parameter x (i.e. xpre ).

24