OnProgrammingforCorrectness/10_.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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{mathtools}
\DeclareMathAlphabet{\mathpzc}{OT1}{pzc}{m}{it}
\title{The Hoare Triple}
\author{Krystal Maughan }
\date{April 28th 2017}

\begin{document}

\maketitle

\section{The Hoare Triple : Composition}
Compositions are typically  represented as \( f \circ g \).
(Read as f of g). They are also typically non-commutative.
\\
\\
Functions that are invertible are isomorphic.
\\
\\
ie. Each element in one group can be mapped to an element
\\
in another group $\rightarrow$ one to one.
Injective and Surjective
\\
at the same time = isomorphic.
\section{Homework 2.3.4.1-1}
Compute wp("$i := i - 1$", $i \geq 0$).
\\
\\
$i - 1 \geq 0$
\\
\\
$ i \geq 1$
\\
\\
$ i > 0$
\\
\\
\section{Homework 2.3.4.1-2}
Compute wp("$i : = i + 1$", $i = j$).
\\
\\
$j = i + 1$
\\
\\
\\
\section{Homework 2.3.4.1-3}
Compute wp("$i : = i + 1; j : = j + i$", $i = j$).
\\
\\
$j = 0$
\\
\\
\section{Homework 2.3.4.1-4}
Compute wp("$i : 2i + 1; j := j + i$", $i = j$).
\\
\\
$j = 0$
\\
\\
\section{Homework 2.3.4.1-5}
Compute wp("$j : = j + i; i : = 2i + 1$", $i = j$).
\\
\\
$j = i + 1$
\\
\\
$ i = j - 1$
\\
\\
\section{Homework 2.3.4.1-6}
Compute wp("$t : = i; i : = j; j : = t$", $i = \hat{i}$ $\land$ $j = \hat{j}$
\\
\\
$i = $ $ \hat{j}$ $\land$ $ j = $ $ \hat{i}$
\\
\\
\section{Homework 2.3.4.1-7}
Compute wp("$i : = 0; s : = 0$", $0 \leq i < n \land s = $ ($\Sigma j | 0 \leq j < i : b(j)))$.
\\
\\
$ 0 < n$
\\
\\
$ 0 \leq 0 < n \land 0 = $ ($\Sigma j | 0 \leq j < 0 : b(j))$
\\
\\
\\
\\
\section{Homework 2.3.4.1-8}
Compute wp("$s : = s + b(i); i : i + 1$", $0 \leq i \leq n \land s = $ ($\Sigma j | 0 \leq j < i : b(j)))$.
\\
\\
$0 \leq i + 1 \leq n \land s + b(i) = $ ($\Sigma j | 0 \leq j < i + 1 : b(j))$
\\
\\
$0 \leq i + 1 \leq n \land s = $ ($\Sigma j | 0 \leq j < i : b(j)$)
\\
\\
\end{document}