OnProgrammingforCorrectness/17a_.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
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}

\author{Krystal Maughan }
\date{May 4th 2017}

\begin{document}

\section{Evaluating Polynomial Function}
$\mathbf{Homework}$ $\mathbf{3.5.2.1}$
\\
\\
Derive the correct loop guard $G$ from:
\\
$\left\{P_{inv} \land \neg G : y = (\Sigma i | k \leq i \leq n : p(i)x^{i - k}) \land 1 \leq k \leq n + 1 \land \neg G\right\}$
\\
$\left\{ R : (\Sigma i | 1 \leq i \leq n : p(i) x^{i - 1})\right\}$
\\
\\
$ 1 < k$
\\
$k \neq 1$
\\
\\
$\mathbf{Homework}$ $\mathbf{3.5.2.2}$
\\
\\
Indicate which of the following is a correct initialization for:
\\
$\left\{ Q : 0 \leq n\right\}$
\\
$k : = $
\\
$ y : = $
\\
$\left\{P_{inv} : y = (\Sigma i | k \leq i \leq n : p(i) x^{i - k}) \land 1 \leq k \leq n + 1\right\}$
\\
\\
$k := n$
\\
$y := p(n)$
\\
\\
$k := n + 1$
\\
$y := 0$
\\
\\
$\mathbf{Homework}$ $\mathbf{3.5.2.3}$
\\
\\
Indicate which is the correct initialization from:
\\
$\left\{P_{inv} \land G: y = (\Sigma i | k \leq i \leq n : p(i) x^{i - k}) \land 1 \leq k \leq n + 1 \land 1 < k\right\}$
\\
$k := k - 1$
\\
$y := ...$
\\
$\left\{P_{inv} : y = (\Sigma i | k \leq i \leq n : p(i) x^{i - k}) \land 1 \leq k \leq n + 1\right\}$
\\
\\
$k := k - 1$
\\
$y := p(k) + y \times x$

\end{document}