-
Notifications
You must be signed in to change notification settings - Fork 0
/
semantics-macros.tex
78 lines (77 loc) · 3.55 KB
/
semantics-macros.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
% !TEX root = main.tex
% expr, store, result
\newcommand{\bigstep}[3]{\langle #1, #2 \rangle \downarrow #3}
\newcommand{\bigstepderiv}[4]{\overset{#1}{\langle #2, #3 \rangle \downarrow #4}}
\newcommand{\bigstepw}[4]{\langle #1, #2, #3 \rangle \downarrow^w #4}
\newcommand{\bigsteppl}[4]{\langle #1, #2, #3 \rangle \downarrow^{\Phi1} #4}
\newcommand{\bigsteppr}[4]{\langle #1, #2, #3 \rangle \downarrow^{\Phi2} #4}
\newcommand{\typestep}[3]{#1 \vdash {#2}: #3}
\newcommand{\typestmt}[2]{#1 \vdash {#2}}
% name, requirement, result
\newcommand{\bsrule}[3]{\textsc{#1}\ddfrac{#2}{#3}}
\newcommand{\trule}[3]{\textsc{#1}\ddfrac{#2}{#3}}
\newcommand{\literalint}[1][n]{\bar{#1}}
\newcommand{\store}[1][\sigma]{#1}
%\newcommand{\clean}[1][n]{#1^\textbf{c}}
%\newcommand{\tracked}[1][n]{#1^\textbf{t}}
%\newcommand{\flagged}[1][n]{#1^f}
\NewDocumentCommand{\clean}{O{n}+o}{{#1}_{[\textbf{c}\IfValueT{#2}{_#2}]}}
\NewDocumentCommand{\tracked}{O{n}+o}{{#1}_{[\textbf{t}\IfValueT{#2}{_#2}]}}
\NewDocumentCommand{\flagged}{O{n}+o}{{#1}_{[{f}\IfValueT{#2}{_#2}]}}
\NewDocumentCommand{\flaggedn}{O{n}}{\tilde{#1}}
\newcommand{\source}[1]{\textbf{source }{#1}}
\newcommand{\defaultsource}{\source{a}}
\newcommand{\sink}[1]{\textbf{sink }{#1}}
\newcommand{\defaultsink}{\sink{a}}
\newcommand{\excstore}[1][\sigma]{\hat{#1}}
\newcommand{\initialstore}[1][\sigma]{\text{initial}({#1})}
\newcommand{\Loc}{\textbf{Loc}}
\newcommand{\partialf}{\rightharpoonup} %{\dashrightarrow}
\newcommand{\StoreDomain}{\tilde{\textbf{Z}}}
\newcommand{\exception}{\textbf{abrt}}
\newcommand{\skipcmd}{\textbf{skip}}
\newcommand{\seq}[2]{{#1}; {#2}}
\newcommand{\defaultseq}{\seq{c_0}{c_1}}
\newcommand{\defaultssaseq}{\seq{s_0}{s_1}}
\newcommand{\ifcmd}[3]{\textbf{if }{#1} \textbf{ then }{#2}\textbf{ else }{#3}}
\newcommand{\defaultif}{\ifcmd{b}{c_0}{c_1}}
\newcommand{\btrue}{\textbf{true}}
\newcommand{\bfalse}{\textbf{false}}
\newcommand{\whilecmd}[2]{\textbf{while }{#1} \textbf{ do } {#2}}
\newcommand{\defaultwhile}{\whilecmd{b}{c_0}}
\newcommand{\storecmd}[2]{{#1} \coloneqq {#2}}
\newcommand{\defaultstore}{\storecmd{X}{a}}
\newcommand{\phistore}[3]{{#1} \coloneqq \varphi({#2}, {#3})}
\newcommand{\philist}{\Phi}
\newcommand{\defaultphi}{\phistore{X_1}{Y_1}{Z_1}, \ldots}
\newcommand{\defaultphilist}{[\defaultphi]}
\newcommand{\defaultphilistn}{[\defaultphi, \phistore{X_n}{Y_n}{Z_n}]}
\newcommand{\ssaif}[4]{\textbf{if }{#1} \textbf{ then }{#2}\textbf{ else }{#3};{#4}}
\newcommand{\defaultssaif}{\ssaif{b}{s_0}{s_1}{\philist}}
\newcommand{\ssawhile}[3]{\textbf{while }#3;{#1} \textbf{ do } {#2}}
\newcommand{\defaultssawhile}{\ssawhile{b}{s_0}{\philist}}
\newcommand{\dunion}{\mathbin{\mathaccent\cdot\cup}}
\newcommand{\union}{\cup}
\newcommand{\storeassign}[2]{{#1} \dunion [{#2}]}
\newcommand{\leftphi}[1]{X_1 \mapsto {#1}(Y_1), \ldots}
\newcommand{\rightphi}[1]{X_1 \mapsto {#1}(Z_1), \ldots}
\newcommand{\dom}[1]{\text{dom }{#1}}
\newcommand{\lattice}{\textbf{Ltc}}
\newcommand{\lclean}{\tint_\textbf{c}}
\newcommand{\lunknown}{\tint_\textbf{u}}
\newcommand{\ltracked}{\tint_\textbf{t}}
\newcommand{\join}{\mathbin\sqcup}
% refine Join to be the unary lattice join
%\let\Join\undefined
%\newcommand{\Join}{\mathop\bigsqcup}
\newcommand{\restrict}[1]{\raisebox{-.5ex}{$|$}_{#1}}
\newcommand{\filter}{\Theta}
\newcommand{\matches}[2]{{#1}:{#2}}
\newcommand{\Tau}{\mathrm{T}}
\newcommand{\tint}{\textbf{int}}
\newcommand{\type}{\tau}
%\newcommand*{\longeq}{\ratio\Longleftrightarrow}
\newcommand{\longeq}{\;\Longleftrightarrow\;}
\newcommand{\labtracked}{\textbf{tracked}}
\newcommand{\labclean}{\textbf{clean}}
\newcommand{\labunknown}{\textbf{unknown}}