OnProgrammingforCorrectness/20_.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
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath}
\usepackage{mathtools}
\DeclareMathAlphabet{\mathpzc}{OT1}{pzc}{m}{it}
\title{Abstraction}
\date{May 10th 2017}
\DeclareMathAlphabet{\mathpzc}{OT1}{pzc}{m}{it}

\begin{document}

\maketitle

\section{Homework 4.1.1.1-1}
Match the predicate with the corresponding predicate:
\\
\\
1.) $d = (\Sigma i | 0 \leq i < n : x(i) \times y(i))$
\\
\\
Ans:
\\
$d = x^{T}y$
\\
\\
2.) $d = (\Sigma i | 0 \leq i < k : x(i) \times y(i)) + (\Sigma i | k \leq i < n : x(i) \times y(i)) \land 0 \leq k \leq n$
\\
\\
Ans:
\\
$d = x^{T}_{T} y_{T} + x^{T}_{B}$ $y_{B}$
\\
\\
3.) $d = (\Sigma i | 0 \leq i < k : x(i) \times y(i)) \land 0 \leq k \leq n$
\\
\\
Ans:
\\
$d = x^{T}_{T}$ $y_{T}$
\\
\\
4.) $d = (\Sigma i | k \leq i < n : x(i) \times y(i)) \land 0 \leq k \leq n$
\\
\\
Ans:
\\
$d = x^{T}_{B}$ $y_{B}$
\\
\\
\\
\\
\\
\\
\\
\\
\section{Homework 4.1.1.1-2}
Complete the dot product annotated algorithm:
\\
\\
$\lbrace (0 \leq n)\rbrace$
\\
\\
$k := 0$
\\
\\
$ x \rightarrow \left(\frac{x_{T}}{x_{B}}\right)$ and $y \rightarrow \left(\frac{y_{T}}{y_{B}}\right)$, where $x_{T}$ and $y_{T}$ have no elements.
\\
\\
$d := 0$
\\
\\
$\lbrace (\forall i | 0 \leq i < k : x(i) \times y(i)) \land (0 \leq k \leq n) \rightarrow d = x^{T}_{T}$ $y_{T}\rbrace$
\\
\\
while $k < n$ do
\\
\\
$\lbrace d = (\forall i | 0 \leq i < k : x(i) \times y(i)) \land (0 \leq k \leq n) \land (k < n) \rightarrow d = x^{T}_{T}y_{T} \rbrace$
\\
\\
$d := d + x(k) \times y(k)$
\\
\\
$k := k + 1$
\\
\\
$\lbrace d = (\forall i | 0 \leq i < k : x(i) \times y(i)) \land (0 \leq k \leq n) \rightarrow d = x^{T}_{T} y_{T}\rbrace$
\\
\\
endwhile
\\
\\
$\lbrace d = (\forall i | 0 \leq i < k : x(i) \times y(i)) \land (0 \leq k \leq n) \land \neg(k < n) \rightarrow d = x^{T}_{T} y_{T}\rbrace$
\\
\\
$\lbrace d = (\Sigma i | 0 \leq i < n : x(i) \times y(i)) \rightarrow d = x^{T} y$


\end{document}