软件分析代写 | Software Analysis & Verification Homework 5

本次美国代写主要为软件分析的homework

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 satisfies 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


程序代写代做C/C++/JAVA/安卓/PYTHON/留学生/PHP/APP开发/MATLAB


blank

本网站支持淘宝 支付宝 微信支付  paypal等等交易。如果不放心可以用淘宝交易!

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


如果您使用手机请先保存二维码,微信识别。如果用电脑,直接掏出手机果断扫描。

blank

发表评论