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
|
\usepackage{listings}
%\lstloadlanguages{C}
\lstdefinestyle{chalice}{%
numbers=none,
firstnumber=0,
numberstyle=\tiny,
stepnumber=5,
% basicstyle=\scriptsize\sffamily,%
% commentstyle=\itshape,%
% keywordstyle=\bfseries,%
% ndkeywordstyle=\bfseries,%
% language=[Sharp]C,
morekeywords={%
above,acc,acquire,and,assert,assigned,assume,%
below,between,bool,%
call,class,const,%
downgrade,%
else,ensures,eval,exists,%
false,fold,forall,fork,free,function,%
ghost,%
holds,%
if,in,int,invariant,ite,%
join,%
lock,lockbottom,lockchange,%
maxlock,method,module,%
new,nil,null,%
old,%
predicate,%
rd,reorder,release,requires,result,returns,%
seq,share,%
this,token,true,%
unfold,unfolding,unshare,%
var,%
while},
literate=%
{=}{{=~}}1%
{+=}{{+}{=}~}3%
{-=}{{-}{=}~}3%
{*=}{{*}{=}~}3%
{++}{{+}{+}}2%
{--}{{-}{-}}2%
{==}{==}2%
{<=}{<=}2%
{=>}{=>}2%
{==>}{==>}3 %
{<==>}{<==>}4 %
%% % {!}{$\lnot$}1% don't do this if ! is also used to indicate non-null types
{!=}{!=}2%
}%
\lstnewenvironment{chalice}[1][]{%
\lstset{style=chalice,
floatplacement={tbp},showstringspaces=false,captionpos=b,
frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}%
\lstnewenvironment{chaliceNoLines}[1][]{%
\lstset{style=chalice,
floatplacement={tbp},showstringspaces=false,captionpos=b,
xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}%
\def\S{%
\lstinline[style=chalice,basicstyle=\ttfamily,columns=fixed]}
\newcommand{\lstfile}[1]{
\lstinputlisting[style=chalice,%
frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,columns=fixed]{#1}
}
|
