-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathctufit-thesis.tex
307 lines (255 loc) · 10.2 KB
/
ctufit-thesis.tex
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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
%% This is the ctufit-thesis example file. It is used to produce theses
%% for submission to Czech Technical University, Faculty of Information Technology.
%%
%% Get the newest version from
%% https://gitlab.fit.cvut.cz/theses-templates/FITthesis-LaTeX
%%
%%
%% Copyright 2021, Eliska Sestakova and Ondrej Guth
%%
%% This work may be distributed and/or modified under the
%% conditions of the LaTeX Project Public Licenese, either version 1.3
%% of this license or (at your option) any later version.
%% The latest version of this license is in
%% https://www.latex-project.org/lppl.txt
%% and version 1.3 or later is part of all distributions of LaTeX
%% version 2005/12/01 or later.
%%
%% This work has the LPPL maintenance status `maintained'.
%%
%% The current maintainer of this work is Ondrej Guth.
%% Contact ondrej.guth@fit.cvut.cz for bug reports.
%% Alternatively, submit bug reports into the tracker at
%% https://gitlab.fit.cvut.cz/theses-templates/FITthesis-LaTeX/issues
%%
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CLASS OPTIONS
% language: czech/english/slovak
% thesis type: bachelor/master/dissertation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentclass[czech,bachelor,unicode]{ctufit-thesis}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% FILL IN THIS INFORMATION
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\ctufittitle{Ověřená binární halda} % replace with the title of your thesis
\ctufitauthorfull{Luboš Zápotočný} % replace with your full name (first name(s) and then family name(s) / surname(s)) including academic degrees
\ctufitauthorsurnames{Zápotočný} % replace with your surname(s) / family name(s)
\ctufitauthorgivennames{Luboš} % replace with your first name(s) / given name(s)
\ctufitsupervisor{doc. RNDr. Dušan Knop, Ph.D.} % replace with name of your supervisor/advisor (include academic degrees)
\ctufitdepartment{Katedra teoretické informatiky} % replace with the department of your defence
\ctufityear{2022} % replace with the year of your defence
\ctufitdeclarationplace{Praze} % replace with the place where you sign the declaration
\ctufitdeclarationdate{\today} % replace with the date of signature of the declaration
\ctufitabstractCZE{Tato práce popisuje implementaci binární minimové haldy a formální důkazy korektnosti jednotlivých operací. Ověřená binární halda je následně použita v Dijkstrově algoritmu pro hledání nejkratší cesty v grafu.}
\ctufitabstractENG{This thesis describes an implementation of the binary minimum heap and formal proofs of the correctness of individual operations. The verified binary heap is then used in Dijkstra's algorithm for finding the shortest path in a graph.}
\ctufitkeywordsCZE{Binární halda, Frama-C, ACSL, Dijkstrův algoritmus, Docker}
\ctufitkeywordsENG{Binary heap, Frama-C, ACSL, Dijkstra's algorithm, Docker}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% END FILL IN
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CUSTOMIZATION of this template
% Skip this part or alter it if you know what you are doing.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\RequirePackage{iftex}[2020/03/06]
\iftutex % XeLaTeX and LuaLaTeX
\RequirePackage{ellipsis}[2020/05/22] %ellipsis workaround for XeLaTeX
\else
\RequirePackage[utf8]{inputenc}[2018/08/11] %this file encoding
\RequirePackage{lmodern}[2009/10/30] % vector flavor of Computer Modern font
\fi
% hyperlinks
\RequirePackage[pdfpagelayout=TwoPageRight,colorlinks=false,allcolors=decoration,pdfborder={0 0 0.1}]{hyperref}[2020-05-15]
% uncomment the following to hide all hyperlinks
% \RequirePackage[pdfpagelayout=TwoPageRight,hidelinks]{hyperref}[2020-05-15]
\RequirePackage{pdfpages}[2020/01/28]
\setcounter{secnumdepth}{4} % numbering sections; 4: subsubsection
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CUSTOMIZATION of this template END
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%
% DEMO CONTENTS SETTINGS
% You may choose to modify this part.
%%%%%%%%%%%%%%%%%%%%%%
\usepackage{dirtree}
\usepackage{lipsum,tikz}
\usepackage{csquotes}
\usepackage[style=iso-numeric,backend=biber]{biblatex}
\addbibresource{text/bib-database.bib}
% \usepackage{listings} % typesetting of sources
\usepackage{minted} % typesetting of sources
\usetikzlibrary{trees}
\usetikzlibrary{matrix}
\usepackage{algorithm}
\usepackage{algpseudocode}
\renewcommand{\listalgorithmname}{Seznam pseudokódů}
\newenvironment{czechalgorithm}[1][]
{\begin{algorithm}[#1]
\selectlanguage{czech}%
\floatname{algorithm}{Algoritmus}%
\renewcommand{\algorithmicif}{\textbf{if}}%
\renewcommand{\algorithmicthen}{\textbf{then}}%
\renewcommand{\algorithmicend}{\textbf{end}}%
\renewcommand{\algorithmicrequire}{\textbf{Požaduje}}%
\renewcommand{\algorithmicensure}{\textbf{Zajišťuje}}%
% Set other language requirements
}
{\end{algorithm}}
%theorems, definitions, etc.
\theoremstyle{plain}
\newtheorem{theorem}{Věta}
\newtheorem{lemma}[theorem]{Tvrzení}
\newtheorem{corollary}[theorem]{Důsledek}
\newtheorem{proposition}[theorem]{Návrh}
\newtheorem{definition}[theorem]{Definice}
\theoremstyle{definition}
\newtheorem{example}[theorem]{Příklad}
\theoremstyle{remark}
\newtheorem{note}[theorem]{Poznámka}
\newtheorem*{note*}{Poznámka}
\newtheorem{remark}[theorem]{Pozorování}
\newtheorem*{remark*}{Pozorování}
\numberwithin{theorem}{chapter}
%theorems, definitions, etc. END
%%%%%%%%%%%%%%%%%%%%%%
% DEMO CONTENTS SETTINGS END
%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%
% Custom math functions
% for propper formatting in math mode
%%%%%%%%%%%%%%%%%%%
\DeclareMathOperator{\Index}{Index}
\DeclareMathOperator{\Parent}{Parent}
\DeclareMathOperator{\LeftChild}{LeftChild}
\DeclareMathOperator{\RightChild}{RightChild}
\DeclareMathOperator{\Value}{Value}
\DeclareMathOperator{\Predecessor}{Predecessor}
\DeclareMathOperator{\HeapFindMin}{HeapFindMin}
\DeclareMathOperator{\HeapExtractMin}{HeapExtractMin}
\DeclareMathOperator{\Weight}{Weight}
\DeclareMathOperator{\HeapChange}{HeapChange}
%%%%%%%%%%%%%%%%%%%
% Custom word splitting
%%%%%%%%%%%%%%%%%%%
\usepackage[T1]{fontenc}
\hyphenation{ro-di-čov-ský}
\hyphenation{maximálně}
\hyphenation{satelitu}
\hyphenation{Alt-Ergo}
\begin{document}
%%%%%%%%%%%%%%%%%%%%%%
% Override (.cls) default ctufit minted settings
%%%%%%%%%%%%%%%%%%%%%%
\usemintedstyle{vs}
\setminted{bgcolor={}}
\setminted{fontsize=\small}
%%%%%%%%%%%%%%%%%%%%%%
% End of override
%%%%%%%%%%%%%%%%%%%%%%
\frontmatter\frontmatterinit % do not remove these two commands
\includepdf{assignment-include.pdf} % replace that file with your thesis assignment provided by study office
\thispagestyle{empty}\cleardoublepage\maketitle % do not remove these three commands
\imprintpage % do not remove this command
\tableofcontents % do not remove this command
%%%%%%%%%%%%%%%%%%%%%%
% list of other contents: figures, tables, code listings, algorithms, etc.
% add/remove commands accordingly
%%%%%%%%%%%%%%%%%%%%%%
\listoffigures % list of figures
\begingroup
\let\clearpage\relax
%\listoftables % list of tables
% \lstlistoflistings % list of source code listings generated by the listings package
\listoflistings % list of source code listings generated by the minted package
\listofalgorithms
\endgroup
%%%%%%%%%%%%%%%%%%%%%%
% list of other contents END
%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%
% ACKNOWLEDGMENT
% FILL IN / MODIFY
% This is a place to thank people for helping you. It is common to thank your supervisor.
%%%%%%%%%%%%%%%%%%%
\begin{acknowledgmentpage}
Chtěl bych poděkovat doc. RNDr. Dušan Knop, Ph.D. za odborné vedení bakalářské práce.
\end{acknowledgmentpage}
%%%%%%%%%%%%%%%%%%%
% ACKNOWLEDGMENT END
%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%
% DECLARATION
% FILL IN / MODIFY
%%%%%%%%%%%%%%%%%%%
% INSTRUCTIONS
% ENG: choose one of approved texts of the declaration. DO NOT CREATE YOUR OWN. Find the approved texts at https://courses.fit.cvut.cz/SFE/download/index.html#_documents (document Declaration for FT in English)
% CZE/SLO: Vyberte jedno z fakultou schvalenych prohlaseni. NEVKLADEJTE VLASTNI TEXT. Schvalena prohlaseni najdete zde: https://courses.fit.cvut.cz/SZZ/dokumenty/index.html#_dokumenty (prohlášení do ZP)
\begin{declarationpage}
Prohlašuji, že jsem předloženou práci vypracoval samostatně a že jsem uvedl veškeré
použité informační zdroje v~souladu s~Metodickým pokynem o~dodržování etických
principů při přípravě vysokoškolských závěrečných prací.
Beru na vědomí, že se na moji práci vztahují práva a povinnosti vyplývající ze zákona č.~121/2000 Sb., autorského zákona, ve znění pozdějších předpisů, zejména
skutečnost, že České vysoké učení technické v Praze má právo na uzavření licenční
smlouvy o užití této práce jako školního díla podle § 60 odst. 1 citovaného zákona.
\end{declarationpage}
%%%%%%%%%%%%%%%%%%%
% DECLARATION END
%%%%%%%%%%%%%%%%%%%
\printabstractpage % do not remove this command
%%%%%%%%%%%%%%%%%%%
% SUMMARY
% FILL IN / MODIFY
% OR REMOVE ENTIRELY (upon agreement with your supervisor)
% (appropriate to remove in most theses)
%%%%%%%%%%%%%%%%%%%
%\begin{summarypage}
%\section*{Summary section}
%
%\lipsum[1][1-8]
%
%\section*{Summary section}
%
%\lipsum[2][1-6]
%
%\section*{Summary section}
%
%\lipsum[3]
%
%\section*{Summary section}
%
%\lipsum[2]
%
%\section*{Summary section}
%
%\lipsum[1][1-8] Lorem lorem lorem.
%\end{summarypage}
%%%%%%%%%%%%%%%%%%%
% SUMMARY END
%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%
% ABBREVIATIONS
% FILL IN / MODIFY
% OR REMOVE ENTIRELY
% List the abbreviations in lexicography order.
%%%%%%%%%%%%%%%%%%%
\chapter{Seznam zkratek}
\begin{tabular}{rl}
ACSL & ANSI/ISO C Specification Language\\
Frama-C & Framework for Modular Analysis of C programs
\end{tabular}
%%%%%%%%%%%%%%%%%%%
% ABBREVIATIONS END
%%%%%%%%%%%%%%%%%%%
\mainmatter\mainmatterinit % do not remove these two commands
%%%%%%%%%%%%%%%%%%%
% THE THESIS
% MODIFY ANYTHING BELOW THIS LINE
%%%%%%%%%%%%%%%%%%%
\include{text/text} % include `text.tex' from `text/' subdirectory
\appendix\appendixinit % do not remove these two commands
\include{text/appendix} % include `appendix.tex' from `text/' subdirectory
\backmatter % do not remove this command
\printbibliography % print out the BibLaTeX-generated bibliography list
\include{text/medium} % include `medium.tex' from `text/' subdirectory
\end{document}