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 }
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:
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:
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])
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