OnProgrammingforCorrectness/5_.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
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{amssymb}
\title{The Hoare Triple}
\author{Krystal Maughan }
\date{April 27th 2017}

\begin{document}

\maketitle

\section{The Hoare Triple}
Homework 2.2.3.1
\\
\\
\\
\\
For each of the below code segments, determine the weakest
\\
\\
precondition (by examination):
\\
\\
\\
\\
1. wp("$x : = y$", $x = 5$) =
\\
\\
$ y = 5$
\\
\\
Explanation: y has to be 5 for this to hold
\\
\\
$\therefore $  it is the weakest precondition
\\
\\
\\
\\
2. wp("$x:=x + 1$", $0 \leq x \leq 1$) =
\\
\\
$-1 \leq x \leq 0$
\\
\\
Explanation: to hold for the range specified
\\
\\
x has to be one less than the range specified
\\
\\
so start at -1 up to (and including) 0
\\
\\
\\
\\
\\
3. wp("$x:=y$", $x = y$) =
\\
\\
TRUE
\\
\\
Explanation: For all values of x, y is TRUE
\\
\\
\\
\\
4. wp("$x: = 4$", $x = 5$) =
\\
\\
FALSE
\\
\\
Explanation: 4 is never 5 so no input will satisfy this
\end{document}