Java Reference

In-Depth Information

Definition of stronger/weaker
:
P
is stronger than
Q
and
Q
is

weaker than
P
if
P => Q
is always true.

An
inference rule
allows us to infer that some
conclusion
is true based on

some initial
premises
. We write an inference rule in this form:

inference rule
: Provided
premise 1
,
premise 2
,

we conclude:
conclusion

For example, the first inference rule below allows us to strengthen the precondi-

tion, while the second allows us to weaken the postcondition:

Strengthen precondition rule
: Provided
P=>Q
,
{
Q
}
S
{
R
}

we conclude:
{
P
}
S
{
R
}

Weaken postcondition rule
: Provided
R=>T
,
{
Q
}
S
{
R
}

we conclude:
{
Q
}
S
{
T
}

IV.3

Axiomatic definition of statements

We now define the skip statement, assignment statement, sequence of state-

ments, conditional statements, and while-loop using Hoare triples. We call the

definitions
axioms
because they are “truths” that we take to hold without formal

proof. This is necessarily a brief introduction, and some explanations as well as

some of the nuances are left untold. We first introduce notation. The notation:

[v\e]R

denotes a copy of assertion
R
in which each occurrence of variable
v
has been

replaced by expression
e
. For example:

[v\v+1](v ≥ w)
is
v+1 ≥ w

[v\x+y](x*v = v)
is
x*(x+y) = (x+y)

We extend this notation to the following, to denote a copy of R in which v and

w have been simultaneously replaced by expressions —extension to more than

two variables is assumed as well:

[v,w\e,f]R

denotes a copy of expression
R
in which occurrences of
v
and
w
have been simul-

taneously replaced by expressions
e
and
f
. Here are examples:

[v,w\w,v](v ≥ w)
is
w ≥ v

[x,n= x+b[n],n+1](x
is the sum of
b[0..n-1])

is

x+b[n]
is the sum of
b[0..n+1-1])

which can be rewritten as

x
is the sum of
b[0..n-1])

Search WWH ::

Custom Search