OnProgrammingforCorrectness/8_.tex at master · kammitama5/OnProgrammingforCorrectness · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
\documentclass{article}
\usepackage[utf8]{inputenc}

\title{The Hoare Triple}
\author{Krystal Maughan }
\date{April 2017}

\begin{document}

\maketitle

\section{The Hoare Triple : Assignment to a Simple Variable}
Homework 2.3.3.1
\\
\\
Prove the following code segment correct
\\
\\
$\left\{Q : s = 0 \land 0 \leq n \right\}$
\\
\\
$ S : k: = 0$
\\
\\
$\left\{R : s = (\Sigma i | 0 \leq i < k : b(i)) \land 0 \leq k \leq n \right\}$
\\
\\
$Q \Rightarrow $ $wp("S", R)$
\\
\\
$<$ instantiate $S$ and $R$ $>$
\\
\\
$Q \Rightarrow$ $wp("k := 0", s = $ $(\Sigma i | 0 \leq i < k : b(i)) \land 0 \leq k \leq n)$
\\
\\
$<$ definition of wp(: =) $>$
\\
\\
$Q \Rightarrow$ $( s = {(\Sigma i | 0 \leq i < k : b(i)) \land 0 \leq  k \leq n)}_{(0)}^{k}$
\\
\\
$<$ definition of ${R}_{E}^{k}$ $>$
\\
\\
$Q \Rightarrow $ ($s = (\Sigma i | 0 \leq i < 0 : b(i)) \land 0 \leq 0 \leq n)$
\\
\\
$<$ instantiate $Q$; sum over empty range; algebra $>$
\\
\\
$(s = 0 \land 0 \leq n) \Rightarrow (s = 0 \land 0 \leq n)$
\\
\\
$<$ $\Rightarrow -$simplification $>$
\\
\\
T

\end{document}