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