blob: f6e15d86e7b693c424bba1c7f01edd82474c5a2b (
plain) (
blame)
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
|
\RequirePackage{amssymb,amsmath,stmaryrd,alltt,color}
\def\A#1{\mathcal{A}\left\llbracket#1\right\rrbracket}
\def\B#1{\mathcal{B}\left\llbracket#1\right\rrbracket}
\def\N#1{\mathcal{N}\left\llbracket#1\right\rrbracket}
\def\s{s\;}
\def\x{\mathtt{x}}
\def\y{\mathtt{y}}
\def\tt{\mathbf{tt}}
\def\ff{\mathbf{ff}}
\def\AND{\mathtt{\;\&\&\;}}
\def\OR{\mathtt{\;||\;}}
\newcommand{\sdowhile}[2]{\mbox{\texttt{do~}}#1\mbox{\texttt{~while~}}#2}
\def\ruleif#1{\using{\enspace\text{if }#1}}
\def\axif#1{\enspace\text{if }#1}
% Engelbert Hubbers, Annotated Programs
\input{sl1defs}
\newcommand{\pass}[2]{\left[#1\mapsto\calA{#2}\right]}
\newcommand{\smaller}[1]{{\small\textcolor{red}{#1}}}
\renewcommand{\allttsup}[1]{\begin{math}^{\textcolor{red}{#1}}\end{math}}
%\renewcommand{\allttsub}[1]{\begin{math}_{\textcolor{red}{#1}}\end{math}}
\renewcommand{\psqan}[5]{\{#1\}^{\textcolor{red}{#4}}\espace #2 \espace \{#3\}^{\textcolor{red}{#5}}}
\newcommand{\transl}[2]{\langle #1, #2\rangle}
\newcommand{\sfor}[4]{\mbox{\texttt{for~}}\sass#1#2\mbox{\texttt{~to~}}#3\mbox{\texttt{~do~}}#4}
\newcommand{\sassert}[2]{\mbox{\texttt{assert~}}#1\mbox{\texttt{~before~}}#2}
\newcommand{\sabort}{\mbox{\texttt{abort}}}
\def\rcompsos#1{[\mbox{comp}_{\mbox{\footnotesize{sos}}}^{#1}]}
\def\rasssos{[\mbox{ass}_{\mbox{\footnotesize{sos}}}]}
\def\rskipsos{[\mbox{skip}_{\mbox{\footnotesize{sos}}}]}
\def\rifsos#1{[\mbox{if}_{\mbox{\footnotesize{sos}}}^{\mbox{\footnotesize{#1}}}]}
\def\rwhilesos{[\mbox{while}_{\mbox{\footnotesize{sos}}}]}
\def\rassert{[\mbox{assert}_{\mbox{\footnotesize{sos}}}]}
|
