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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
% dafny.sty
% Dafny mode for the LaTeX listings package.
% Rustan Leino, 22 June 2008.
\usepackage{listings}
\lstdefinelanguage{dafny}{
morekeywords={class,datatype,codatatype,newtype,type,iterator,trait,extends,
bool,char,nat,int,real,object,set,iset,multiset,seq,string,map,imap,array,array2,array3,
function,predicate,copredicate,inductive,
ghost,var,static,protected,refines,
method,lemma,constructor,colemma,
returns,yields,abstract,module,import,default,opened,as,in,
requires,modifies,ensures,reads,decreases,free,include,
% expressions
match,case,false,true,null,old,fresh,this,
% statements
assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,
where,calc,modify
},
literate=%
{:}{$\colon$}1
{::}{$\bullet$}2
{:=}{$:$$=$}2
{:|}{${:}\!\!|$}2
{!}{$\lnot$}1
{!!}{$\not\cap$}1
{==}{$=$}1
{!=}{$\neq$}1
{&&}{$\land$}1
{||}{$\lor$}1
{<=}{$\le$}1
{>=}{$\ge$}1
% the following isn't actually Dafny, but it gives the option to produce nicer latex
{<=set}{$\subseteq$}1
{+set}{$\cup$}1
{*set}{$\cap$}1
{==>}{$\Longrightarrow$}3
{<==}{$\Longleftarrow$}3
{=>}{$\Rightarrow$}2
{<==>}{$\Longleftrightarrow$}4
{forall}{$\forall$}1
{exists}{$\exists$}1
{!in}{$\not\in$}1
{\\in}{$\in$}1
% the following isn't actually Dafny, but it gives the option to produce nicer latex
{<<}{$\langle$}1
{>>}{$\rangle$}1
{(==)}{${}^{(=)}$}2
{...}{$\ldots$}2
{\\alpha}{$\alpha$}1
{\\beta}{$\beta$}1
{\\gamma}{$\gamma$}1
{\\delta}{$\delta$}1
{\\epsilon}{$\epsilon$}1
{\\zeta}{$\zeta$}1
{\\eta}{$\eta$}1
{\\theta}{$\theta$}1
{\\iota}{$\iota$}1
{\\kappa}{$\kappa$}1
{\\lambda}{$\lambda$}1
{\\mu}{$\mu$}1
{\\nu}{$\nu$}1
{\\xi}{$\xi$}1
{\\pi}{$\pi$}1
{\\rho}{$\rho$}1
{\\sigma}{$\sigma$}1
{\\tau}{$\tau$}1
{\\upsilon}{$\upsilon$}1
{\\phi}{$\phi$}1
{\\chi}{$\chi$}1
{\\psi}{$\psi$}1
{\\omega}{$\omega$}1
{\\Gamma}{$\Gamma$}1
{\\Delta}{$\Delta$}1
{\\Theta}{$\Theta$}1
{\\Lambda}{$\Lambda$}1
{\\Xi}{$\Xi$}1
{\\Pi}{$\Pi$}1
{\\Sigma}{$\Sigma$}1
{\\Upsilon}{$\Upsilon$}1
{\\Phi}{$\Phi$}1
{\\Psi}{$\Psi$}1
{\\Omega}{$\Omega$}1
,
sensitive=true, % case sensitive
morecomment=[l]{//},
morecomment=[s]{/*}{*/},
morecomment=[s]{\{:}{\}},
morestring=[b]",
numbers=none,
firstnumber=0,
numberstyle=\tiny,
stepnumber=5,
basicstyle=\scriptsize\sffamily,
commentstyle=\itshape,
keywordstyle=\bfseries,
ndkeywordstyle=\bfseries,
}
\lstnewenvironment{dafny}[1][]{%
\lstset{language=dafny,
floatplacement={tbp},captionpos=b,
frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}
\lstnewenvironment{dafnyNoLines}[1][]{%
\lstset{language=dafny,
floatplacement={tbp},captionpos=b,
xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}
\def\inlinedafny{%
\lstinline[language=dafny,basicstyle=\ttfamily,columns=fixed]}
\newcommand{\lstfile}[1]{
\lstinputlisting[language=dafny,%
frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,columns=fixed]{#1}
}
|
