# 软件分析代写 | Software Analysis & Veriﬁcation Homework 5

Problem 1: Hoare Triples
Are the following Hoare triples valid? And why? Be careful to distinguish between partial correctness
and total correctness.
1-1 fX = 0 ^ Y = 1g X := X + 1; Y := Y + 1 fX = 1 ^ Y = 2g
Solution 
1-2 f>g while X  0 do X := X + 1 end fX  0g
Solution 
1-3 [>] while X > 0 do X := X 1 end [X  0]
Solution 
1-4 f>g while X > 0 do X := X 1 end fX = 0g
Solution 

Problem 2: Weakest Liberal Precondition
2-1 Compute wlp(if X > 0 then Y := X else Y := X; Y > 5).
Solution 
2-2 Compute wlp(while X > 0 do X := X + 1 end;X  0) (The given invariant I is true).
Solution 

Problem 3: Decorated Programs
The beauty of Hoare logic is that it is compositional : the structure of proofs exactly follows the
structure of programs. This suggests that we can record the essential ideas of a proof (leaving out
some low-level calculational details) by “decorating” a program with appropriate assertions on each of
its commands. Such a decorated program carries within it an argument for its own correctness.
For example, consider the program (where m and p denote two constant integers):
X := m;
Z := p;
while :(X = 0) do
Z := Z 1;
X := X 1
end
To show that the above program satisﬁes precondition > and postcondition Z = p m, we decorate
the above as the following:
f>g  fm = mg
X := m;
fX = mg  fX = m ^ p = pg
Z := p;
fX = m ^ Z = pg  fZ X = p mg
while :(X = 0) do
fZ X = p m ^ X = 0g  f(Z 1) (X 1) = p mg
Z := Z 1;
fZ (X 1) = p mg
X := X 1
fZ X = p mg
end
fZ X = p m ^ :(X = 0)g  fZ = p mg

Concretely, a decorated program consists of the program commands interleaved with assertions
– either a single assertion, or possibly two assertions separated by an implication “” (we use this
strange notation to distinguish from our reduction relation !). To check that a decorated program
represents a valid proof, we check that each individual command is locally consistent with its nearby
assertions, following the standard Hoare rules, e.g.
fm = mg X := m fX = mg
is valid by rule Asgn. Note that this hoare triple must not only be valid, but also be an instantiation
of some Hoare rule. To convince yourself, carefully check that every such triples are indeed valid, and
they are instantiations of the standard Hoare rules.
Now, it’s your turn. Here is a program P that squares X by repeated addition:
Y := 0;
Z := 0;
while :(Y = X) do
Z := Z + X;
Y := Y + 1
end

E-mail: itcsdx@outlook.com  微信:itcsdx