setup.tex 13.4 KB
Newer Older
1
2
3
4
5
6

\makeatletter%
\@ifundefined{basedir}{%
\newcommand\basedir{}%
}{}%
\makeatother%
7
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Ralf Jung's avatar
Ralf Jung committed
8
%% PACKAGES
9
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
10

11
12
13
14
15
16
17
\usepackage{mathtools}
%\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{stmaryrd}

18
\usepackage{\basedir mathpartir}
19

20
21
\usepackage{array}
\usepackage{tabu}
22
23
24

\usepackage{dashbox}

25
\usepackage{\basedir pftools}
26
27
28
29

\usepackage{xcolor}  % for print version

\usepackage{graphicx}
30
31
32
33
34
35
36
37
38
39
40
41
\usepackage{tikz}
\usepackage{scalerel}

\usepackage{rotating}
\usepackage{xparse}
\usepackage{xstring}
\usepackage{semantic}
\usepackage{csquotes}

\usepackage{hyperref}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Ralf Jung's avatar
Ralf Jung committed
42
%% SETUP
43
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
44
\SetSymbolFont{stmry}{bold}{U}{stmry}{m}{n} % this fixes warnings when \boldsymbol is used with stmaryrd included
45
46
47
48
49
50
51
52
53
54

\extrarowheight=\jot	% else, arrays are scrunched compared to, say, aligned
\newcolumntype{.}{@{}}
% Array {rMcMl} modifies array {rcl}, putting mathrel-style spacing
% around the centered column. (We used this, for example, in laying
% out some of Iris' axioms. Generally, aligned is simpler but aligned
% does not work in mathpar because \\ inherits mathpar's 2em vskip.)
% The capital M stands for THICKMuskip. The smaller medmuskip would be
% right for mathbin-style spacing.
\newcolumntype{M}{@{\mskip\thickmuskip}}
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75

\definecolor{StringRed}{rgb}{.637,0.082,0.082}
\definecolor{CommentGreen}{rgb}{0.0,0.55,0.3}
\definecolor{KeywordBlue}{rgb}{0.0,0.3,0.55}
\definecolor{LinkColor}{rgb}{0.55,0.0,0.3}
\definecolor{CiteColor}{rgb}{0.55,0.0,0.3}
\definecolor{HighlightColor}{rgb}{0.0,0.0,0.0}

\usetikzlibrary{shapes}
%\usetikzlibrary{snakes}
\usetikzlibrary{arrows}
\usetikzlibrary{calc}
\usetikzlibrary{arrows.meta}
\tikzstyle{state}=[circle, draw, minimum size=1.2cm, align=center]
\tikzstyle{trans}=[arrows={->[scale=1.4]}]

\tikzstyle{layer}=[rounded corners=2pt, thin, align=center, draw, minimum width=4.2cm,minimum height=0.8cm]

\definecolor{grey}{rgb}{0.5,0.5,0.5}
\definecolor{red}{rgb}{1,0,0}

76
77
78
79
80
81
82
83
84
\hypersetup{%
  linktocpage=true, pdfstartview=FitV,
  breaklinks=true, pageanchor=true, pdfpagemode=UseOutlines,
  plainpages=false, bookmarksnumbered, bookmarksopen=true, bookmarksopenlevel=3,
  hypertexnames=true, pdfhighlight=/O,
  colorlinks=true,linkcolor=LinkColor,citecolor=CiteColor,
  urlcolor=LinkColor
}

85
86
87
88
89
90
91
92
93
94
95
96

%\theoremstyle{definition}
%\newtheorem{prop}{Prop}
\newtheorem{defn}{Definition}
\newtheorem{cor}{Corollary}
\newtheorem{conj}{Conj}
\newtheorem{lem}{Lemma}
\newtheorem{thm}{Theorem}

\newtheorem{exercise}{Exercise}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Ralf Jung's avatar
Ralf Jung committed
97
%% GENERIC MACROS
98
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
99
100
101
102
103
104
105
106
107
\newcommand*{\Sref}[1]{\hyperref[#1]{\S\ref*{#1}}}
\newcommand*{\secref}[1]{\hyperref[#1]{Section~\ref*{#1}}}
\newcommand*{\lemref}[1]{\hyperref[#1]{Lemma~\ref*{#1}}}
\newcommand{\corref}[1]{\hyperref[#1]{Cor.~\ref*{#1}}}
\newcommand*{\defref}[1]{\hyperref[#1]{Definition~\ref*{#1}}}
\newcommand*{\egref}[1]{\hyperref[#1]{Example~\ref*{#1}}}
\newcommand*{\appendixref}[1]{\hyperref[#1]{Appendix~\ref*{#1}}}
\newcommand*{\figref}[1]{\hyperref[#1]{Figure~\ref*{#1}}}
\newcommand*{\tabref}[1]{\hyperref[#1]{Table~\ref*{#1}}}
108
109
110
111
112

\newcommand{\changes}{{\bf\color{red}{Changes}}}
\newcommand{\TODO}{\vskip 4pt {\color{red}\bf TODO}}


Ralf Jung's avatar
Ralf Jung committed
113
114
115
116
\newcommand{\ie}{\emph{i.e.,} }
\newcommand{\eg}{\emph{e.g.,} }
\newcommand{\etal}{\emph{et~al.}}
\newcommand{\wrt}{w.r.t.~}
117

Ralf Jung's avatar
Ralf Jung committed
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
\newcommand{\aaron}[1]{{\color{red}\textbf{AT: #1}}}
\newcommand{\derek}[1]{{\color{red}\textbf{DD: #1}}}
\newcommand{\lars}[1]{{\color{red}\textbf{LB: #1}}}
\newcommand{\kasper}[1]{{\color{red}\textbf{KS: #1}}}
\newcommand{\ralf}[1]{{\color{red}\textbf{RJ: #1}}}
\newcommand{\dave}[1]{{\color{red}\textbf{PDS: #1}}}
\newcommand{\hush}[1]{}
\newcommand{\relaxguys}{%
	\let\aaron\hush%
	\let\derek\hush%
	\let\lars\hush%
	\let\kasper\hush%
	\let\ralf\hush%
	\let\dave\hush%
}
133

Ralf Jung's avatar
Ralf Jung committed
134
135
136
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MATH SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
137
138
139
140
141
142
143
144

% superscript to the left
\def\presuper#1#2%
  {\mathop{}%
   \mathopen{\vphantom{#2}}^{#1}%
   \kern-\scriptspace%
   #2}

Ralf Jung's avatar
Ralf Jung committed
145
146
147
148
149
150
151
\DeclareMathOperator*{\Sep}{\scalerel*{\ast}{\sum}}
\newcommand{\bigast}{\Sep}

\newcommand*{\sep}[1][]{\mathrel{\#_{#1}}}	% bad name; it's a different "sep"

\newcommand{\ALT}{\ |\ }

Ralf Jung's avatar
Ralf Jung committed
152
\newcommand\dplus{\mathbin{+\kern-1.0ex+}}
153
154

\newcommand{\upclose}{\mathord{\uparrow}}
155

Ralf Jung's avatar
Ralf Jung committed
156
157
158
159
160
\newcommand{\spac}{\;} % a space

\def\All #1.{\forall #1.\spac}%
\def\Exists #1.{\exists #1.\spac}%
\def\Ret #1.{#1.\spac}%
161

Ralf Jung's avatar
Ralf Jung committed
162
163
\newcommand{\any}{{\rule[-.2ex]{1ex}{.4pt}}}%
\newcommand{\unitval}{()}%
164

Ralf Jung's avatar
Ralf Jung committed
165
\newcommand{\judgment}[2]{\paragraph{#1}\hspace{\stretch{1}}\fbox{$#2$}}
166

Ralf Jung's avatar
Ralf Jung committed
167
\newcommand{\pfn}{\rightharpoonup}
Ralf Jung's avatar
Ralf Jung committed
168
\newcommand\fpfn{}%\xrightharpoonup{\kern-0.25ex\textrm{fin}\kern-0.25ex}}
Ralf Jung's avatar
Ralf Jung committed
169
170
171
\newcommand{\ra}{\rightarrow}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\Lra}{\Leftrightarrow}
Ralf Jung's avatar
Ralf Jung committed
172
\newcommand\monra{}%\xrightarrow{\kern-0.25ex\textrm{mon}\kern-0.25ex}}
173

Ralf Jung's avatar
Ralf Jung committed
174
\newcommand{\eqdef}{\triangleq}
175

Ralf Jung's avatar
Ralf Jung committed
176
177
178
\newcommand{\restr}[2]{\lfloor #1 \rfloor_{#2}}
\newcommand{\pset}[1]{\wp(#1)} % Powerset
\newcommand{\psetdown}[1]{\wp^\downarrow(#1)}
179

Ralf Jung's avatar
Ralf Jung committed
180
181
182
\newcommand{\dom}{\mathrm{dom}}
\newcommand{\cod}{\mathrm{cod}}
\newcommand{\chain}{\mathrm{chain}}
183

Ralf Jung's avatar
Ralf Jung committed
184
185
\newcommand{\IF}{\mathrel{\text{if}}}
\newcommand{\WHEN}{\textrm{when }}
186

Ralf Jung's avatar
Ralf Jung committed
187
188
\newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}}
\newcommand*\set[1]{\left\{#1\right\}}
189

Ralf Jung's avatar
Ralf Jung committed
190
191
192
193
194
\newenvironment{inbox}[1][]{
  \begin{array}[#1]{@{}l@{}}
}{
  \end{array}
}
195

Ralf Jung's avatar
Ralf Jung committed
196
197
198
199
200
\newcommand{\tabubox}[2][]{%
  \begin{tabu}{@{#1}X[1,l,m]@{}}%
    #2 %
  \end{tabu}%
}
201

Ralf Jung's avatar
Ralf Jung committed
202
\newcommand{\Func}{F} % functor
Ralf Jung's avatar
Ralf Jung committed
203
204
205
206

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
207
\newcommand{\textdom}[1]{\textit{#1}}
Ralf Jung's avatar
Ralf Jung committed
208
209

\newcommand{\wIso}{\xi}
210

Ralf Jung's avatar
Ralf Jung committed
211
212
\newcommand{\rs}{r}
\newcommand{\rsB}{s}
213

Ralf Jung's avatar
Ralf Jung committed
214
\newcommand{\pres}{\pi}
215
\newcommand{\wld}{w}
Ralf Jung's avatar
Ralf Jung committed
216
\newcommand{\ghostRes}{g}
217

Ralf Jung's avatar
Ralf Jung committed
218
219
%% Various pieces of syntax
\newcommand{\fullSat}[4]{#1 \models_{#2} #3; #4}
220

Ralf Jung's avatar
Ralf Jung committed
221
\newcommand{\wtt}[2]{#1 : #2} % well-typed term
222

Ralf Jung's avatar
Ralf Jung committed
223
224
225
226
227
\newcommand{\nequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{=}}}}
\newcommand{\notnequiv}[1]{\ensuremath{\mathrel{\stackrel{#1}{\neq}}}}
\newcommand{\nequivset}[2]{\ensuremath{\mathrel{\stackrel{#1}{=}_{#2}}}}
\newcommand{\nequivB}[1]{\ensuremath{\mathrel{\stackrel{#1}{\equiv}}}}
\newcommand{\latert}{\mathord{\blacktriangleright}}
228

Ralf Jung's avatar
Ralf Jung committed
229
\newcommand{\Sem}[1]{\llbracket #1 \rrbracket}
230

Ralf Jung's avatar
Ralf Jung committed
231
232
\newcommand{\sembox}[1]{\hfill \normalfont \mbox{\fbox{\(#1\)}}}
\newcommand{\typedsection}[2]{\subsubsection*{\rm\em #1 \sembox{#2}}}
233
234


Ralf Jung's avatar
Ralf Jung committed
235
236
237
%% Some commonly used identifiers
\newcommand{\UPred}{\textdom{UPred}}
\newcommand{\SPred}{\textdom{SPred}}
238

Ralf Jung's avatar
Ralf Jung committed
239
240
\newcommand{\PropDom}{\textdom{Prop}}
\newcommand{\PredDom}{\textdom{Pred}}
241

Ralf Jung's avatar
Ralf Jung committed
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
\newcommand{\COFEs}{\mathcal{U}} % category of COFEs
\newcommand{\iFunc}{\Sigma}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CMRA (RESOURCE ALGEBRA) SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\textmon}[1]{\textsc{#1}}

\newcommand{\monoid}{M}
\newcommand{\mval}{V}

\newcommand{\melt}{a}
\newcommand{\meltB}{b}
\newcommand{\meltC}{c}
\newcommand{\melts}{A}
\newcommand{\meltsB}{B}

\newcommand{\mcar}[1]{|#1|}
\newcommand{\mcarp}[1]{\mcar{#1}^{+}}
\newcommand{\munit}{\mathord{\varepsilon}}
\newcommand{\mtimes}{\mathbin{\cdot}}
\newcommand{\mdiv}{\mathbin{\div}}

\newcommand{\mupd}{\rightsquigarrow}
\newcommand{\mincl}[1]{\ensuremath{\mathrel{\stackrel{#1}{\leq}}}}

\newcommand{\CMRAs}{\mathcal{R}} % category of CMRAs
Ralf Jung's avatar
Ralf Jung committed
271
272
273
274

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% LOGIC SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
275
276
\newcommand{\textlog}[1]{\textsf{#1}}
\newcommand{\textsort}[1]{\textlog{#1}}
Ralf Jung's avatar
Ralf Jung committed
277

278
\newcommand{\Sig}{\mathcal{S}}
279
280
\newcommand{\SigType}{\mathcal{T}}
\newcommand{\SigFn}{\mathcal{F}}
Ralf Jung's avatar
Ralf Jung committed
281
282
\newcommand{\SigAx}{\mathcal{A}}
\newcommand{\sigtype}{T}
283
\newcommand{\sigfn}{F}
Ralf Jung's avatar
Ralf Jung committed
284
\newcommand{\sigax}{A}
285

Ralf Jung's avatar
Ralf Jung committed
286
\newcommand{\type}{\tau}
287

Ralf Jung's avatar
Ralf Jung committed
288
289
290
\newcommand{\var}{x}
\newcommand{\varB}{y}
\newcommand{\varC}{z}
291

Ralf Jung's avatar
Ralf Jung committed
292
293
294
\newcommand{\term}{t}
\newcommand{\termB}{u}
\newcommand{\termVal}{V}
295

Ralf Jung's avatar
Ralf Jung committed
296
297
\newcommand{\vctx}{\Gamma}
\newcommand{\pfctx}{\Theta}
298

Ralf Jung's avatar
Ralf Jung committed
299
300
301
\newcommand{\prop}{P}
\newcommand{\propB}{Q}
\newcommand{\propC}{R}
302

Ralf Jung's avatar
Ralf Jung committed
303
304
305
\newcommand{\pred}{\varphi}
\newcommand{\predB}{\psi}
\newcommand{\predC}{\zeta}
306

Ralf Jung's avatar
Ralf Jung committed
307
308
309
\newcommand{\gname}{\gamma}
\newcommand{\iname}{\iota}
\newcommand{\inameB}{\iota'}
310

Ralf Jung's avatar
Ralf Jung committed
311
\newcommand{\mask}{\mathcal{E}}
312
\newcommand{\namesp}{\mathcal{N}}
313

Ralf Jung's avatar
Ralf Jung committed
314
%% various pieces of Syntax
315
316
\newcommand{\unitsort}{1}%	\unit is bold.

Ralf Jung's avatar
Ralf Jung committed
317
318
\def\MU #1.{\mu #1.\spac}%
\def\Lam #1.{\lambda #1.\spac}%
319

Ralf Jung's avatar
Ralf Jung committed
320
321
\newcommand{\proves}{\vdash}
\newcommand{\provesalways}{\vdash_{\!\!\boxempty}}
322

Ralf Jung's avatar
Ralf Jung committed
323
\newcommand{\wand}{\;{{\mbox{---}}\!\!{*}}\;}
324

Ralf Jung's avatar
Ralf Jung committed
325
326
% oh my... I have to wrap the "-" in a \mathrm, otherwise all hell breaks lose...
\newcommand{\fmapsto}[1][\mathrm{-}]{\xmapsto{#1}}
Ralf Jung's avatar
Ralf Jung committed
327
\newcommand{\gmapsto}{\hookrightarrow}%
Ralf Jung's avatar
Ralf Jung committed
328
\newcommand{\fgmapsto}[1][\mathrm{-}]{\xhookrightarrow{#1}}%
329

Ralf Jung's avatar
Ralf Jung committed
330
331
332
333
334
335
\newcommand{\dyn}[2]{\textlog{wp}({#1}, {#2})}
\newcommand{\adyn}[2]{{#1}\;\llparenthesis{#2}\rrparenthesis}
\newcommand{\dynpred}[2]{\textdom{wp}({#1}, {#2})}
\newcommand{\dynA}[3]{\textlog{wp}_{#3}({#1}, {#2})}
\newcommand{\pvs}[1]{\textlog{vs}({#1})}
\newcommand{\pvsA}[3]{\textlog{vs}_{#2}^{#3}({#1})}
336

Ralf Jung's avatar
Ralf Jung committed
337
338
\newcommand{\later}{\mathord{\triangleright}}
\newcommand{\always}{\Box{}}
339

Ralf Jung's avatar
Ralf Jung committed
340
%% Invariants and Ghost ownership
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
% PDS: Was 0pt inner, 2pt outer.
% \boxedassert [tikzoptions] contents [name]
\tikzstyle{boxedassert_border} = [sharp corners,line width=0.2pt]
\NewDocumentCommand \boxedassert {O{} m o}{%
	\tikz[baseline=(m.base)]{
		%	  \node[rectangle, draw,inner sep=0.8pt,anchor=base,#1] (m) {${#2}\mathstrut$};
		\node[rectangle,inner sep=0.8pt,outer sep=0.2pt,anchor=base] (m) {${#2}\mathstrut$};
		\draw[#1,boxedassert_border] ($(m.south west) + (0,0.65pt)$) rectangle ($(m.north east) + (0, 0.7pt)$);
	}\IfNoValueF{#3}{^{\,#3}}%
}
\newcommand*{\knowInv}[2]{\boxedassert{#2}[#1]}
\newcommand*{\ownGhost}[2]{\boxedassert[densely dashed]{#2}[#1]}
\newcommand*{\ownGGhost}[1]{\boxedassert[densely dashed]{#1}}

\newcommand{\ownPhys}[1]{\lfloor#1\rfloor}

Ralf Jung's avatar
Ralf Jung committed
357
%% View Shifts
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
\NewDocumentCommand \vsGen {O{} m O{}}%
  {\mathrel{%
    \ifthenelse{\equal{#3}{}}{%
      % Just one mask, or none
      {#2}_{#1}%
    }{%
      % Two masks
      \presuper{#1}{#2}^{#3}
    }%
  }}%
\NewDocumentCommand \vs {O{} O{}} {\vsGen[#1]{\Rrightarrow}[#2]}
\NewDocumentCommand \vsL {O{} O{}} {\vsGen[#1]{\Lleftarrow}[#2]}
\NewDocumentCommand \vsE {O{} O{}} %
  {\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}

Ralf Jung's avatar
Ralf Jung committed
373
%% Hoare Triples
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
\newcommand*{\hoaresizebox}[1]{%
  \hbox{$\mathsurround=0pt{#1}\mathstrut$}}
\newcommand*{\hoarescalebox}[2]{%
  \hbox{\scalerel*[1ex]{#1}{#2}}}
\newcommand{\triple}[5]{%
  \setbox0=\hoaresizebox{{#3}{#5}}%
  \setbox1=\hoarescalebox{#1}{\copy0}%
  \setbox2=\hoarescalebox{#2}{\copy0}%
  \copy1{#3}\copy2%
  \;{#4}\;%
  \copy1{#5}\copy2}
\NewDocumentCommand \hoare {m m m O{}}{
	\triple\{\}{#1}{#2}{#3}%
	_{#4}%
}

\newcommand{\bracket}[4][]{%
  \setbox0=\hbox{$\mathsurround=0pt{#1}{#4}\mathstrut$}%
  \scalerel*[1ex]{#2}{\copy0}%
  {#4}%
  \scalerel*[1ex]{#3}{\copy0}}
% \curlybracket[other] x
\newcommand{\curlybracket}[2][]{\bracket[{#1}]\{\}{#2}}
\newcommand{\anglebracket}[2][]{\bracket[{#1}]\langle\rangle{#2}}
% \hoareV[t] pre c post [mask]
\NewDocumentCommand \hoareV {O{c} m m m O{}}{
		{\begin{aligned}[#1]
		&\curlybracket{#2} \\
		&\quad{#3} \\
		&{\curlybracket{#4}}_{#5}
		\end{aligned}}%
}
% \hoareHV[t] pre c post [mask]
\NewDocumentCommand \hoareHV {O{c} m m m O{}}{
	{\begin{aligned}[#1]
	&\curlybracket{#2} \; {#3} \\
	&{\curlybracket{#4}}_{#5}
	\end{aligned}}%
}


Ralf Jung's avatar
Ralf Jung committed
415
416
417
418
%% Some commonly used identifiers
\newcommand{\timeless}[1]{\textlog{timeless}(#1)}
\newcommand{\physatomic}[1]{\textlog{$#1$ phys.\ atomic}}
\newcommand{\infinite}{\textlog{infinite}}
419

Ralf Jung's avatar
Ralf Jung committed
420
421
\newcommand{\Prop}{\textlog{Prop}}
\newcommand{\Pred}{\textlog{Pred}}
422

Ralf Jung's avatar
Ralf Jung committed
423
424
\newcommand{\TRUE}{\textlog{True}}
\newcommand{\FALSE}{\textlog{False}}
425
426

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
427
% LANGUAGE SYNTAX AND SEMANTICS
428
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Ralf Jung's avatar
Ralf Jung committed
429
430
431
432
433
\newcommand{\expr}{e}
\newcommand{\val}{v}
\newcommand{\valB}{w}
\newcommand{\state}{\sigma}
\newcommand{\step}{\ra}
434

Ralf Jung's avatar
Ralf Jung committed
435
436
437
438
439
\newcommand{\toval}{\mathit{val}}
\newcommand{\ofval}{\mathit{expr}}
\newcommand{\atomic}{\mathit{atomic}}
\newcommand{\Lang}{\Lambda}

Ralf Jung's avatar
Ralf Jung committed
440
\newcommand{\tpool}{T}
441

Ralf Jung's avatar
Ralf Jung committed
442
\newcommand{\cfg}[2]{{#1};{#2}}
443
444

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Ralf Jung's avatar
Ralf Jung committed
445
446
% DERIVED CONSTRUCTIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
447

Ralf Jung's avatar
Ralf Jung committed
448
%% Commonly used identifiers
Ralf Jung's avatar
Ralf Jung committed
449
450
\newcommand{\FHeap}{\textmon{FHeap}}
\newcommand{\AFHeap}{\textmon{AFHeap}}
451

Ralf Jung's avatar
Ralf Jung committed
452
\newcommand{\auth}[1]{\textmon{Auth}}
453
454
455
\newcommand{\authfull}{\mathord{\bullet}\,}
\newcommand{\authfrag}{\mathord{\circ}\,}

Ralf Jung's avatar
Ralf Jung committed
456
457
458
\newcommand{\fracm}{\ensuremath{\textmon{Frac}}}
\newcommand{\exm}{\ensuremath{\textmon{Ex}}}
\newcommand{\agm}{\ensuremath{\textmon{Ag}}}
459

Ralf Jung's avatar
Ralf Jung committed
460
\newcommand{\STSMon}[1]{\textmon{Sts}_{#1}}
461
462
463
464
465
466
467
468
469
\newcommand{\STSInv}{\textsf{STSInv}}
\newcommand{\STS}{\textsf{STS}}
\newcommand{\STSS}{\mathcal{S}} % states
\newcommand{\STST}{\mathcal{T}} % tokens
\newcommand{\STSL}{\mathcal{L}} % labels
\newcommand{\ststrans}{\ra^{*}}%	the relation relevant to the STS rules

\newcommand{\AuthInv}{\textsf{AuthInv}}
\newcommand{\Auth}{\textsf{Auth}}