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
|
\newnotationgroup{regions}{Sets of regions (in the example
section).}{\ROReg, \WOReg, \RWReg, \RReg, \WReg}
\newnotationmember{regions}\Region{{\bf Reg}}
\newnotation\mreg{\rho}{Region meta-variable (example section)}
\newnotationmember{regions}\AllReg{\Region}
\newnotationmember{regions}\ROReg{\Region_{\bf RO}}
\newnotationmember{regions}\WOReg{\Region_{\bf WO}}
\newnotationmember{regions}\RWReg{\Region_{\bf RW}}
\newnotationmember{regions}\RReg{\Region_{\bf R}}
\newnotationmember{regions}\WReg{\Region_{\bf W}}
\newcommand\reglookop[1][\mreg]{\lookupop^{#1}}
\newcommand\regupop[1][\mreg]{\updateop^{#1}}
\newcommand\ndop{\lor}
\newnotationmember{ops}\rollbackop{\mathrm{rollback}}
\newnotationmember{ops}\abortop{\mathrm{abort}}
\newnotationargs\locLiteral1{#1}{A literal for the location
$\loc$.}{\locLiteral \loc}
\newnotation\mopt{o}{Optimisation meta-variable (stands for Copy,
Discard, etc.)}
\newnotationargs\optset1{\zeta^{#1}}{The set of effects satisfying
the op-wise valid optimisation $\mopt$.}{\optset\mopt}
\newnotation\proves{\vdash}{}
\newnotationexample\nproves{\nvdash}{$\mL$ does not prove $\mterm = \mtermv$}{\mL \nproves \mterm = \mtermv}
\newnotation\bnot{\sim}{Bit-wise not function.}
|