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
114
115
116
117
118
119
120
121
|
% boogie.sty
% Boogie mode for the LaTeX listings package.
% Rustan Leino, 30 May 2008.
% Example:
% \begin{boogie}
% type Field \alpha;
% var Heap: <<\alpha>>[ref, Field \alpha]\alpha where IsHeap(Heap);
% function IsHeap(<<\alpha>>[ref, Field \alpha]\alpha) returns (bool);
% procedure Inc(x: int) returns (y: int)
% modifies Heap;
% {
% havoc Heap;
% if (0 <= x && x < 100) {
% y := x + 1;
% }
% }
% \end{boogie}
\usepackage{listings}
\lstdefinelanguage{boogie}{
morekeywords={type,bool,int,real,%
bv0,bv1,bv2,bv3,bv4,bv5,bv6,bv7,bv8,bv9,%
bv10,bv11,bv12,bv13,bv14,bv15,bv16,bv17,bv18,bv19,%
bv20,bv21,bv22,bv23,bv24,bv25,bv26,bv27,bv28,bv29,%
bv30,bv31,bv32,bv33,bv34,bv35,bv36,bv37,bv38,bv39,%
bv40,bv41,bv42,bv43,bv44,bv45,bv46,bv47,bv48,bv49,%
bv50,bv51,bv52,bv53,bv54,bv55,bv56,bv57,bv58,bv59,%
bv60,bv61,bv62,bv63,bv64,% ...
const,unique,complete,partition,
axiom,
function,returns,
var,where,
procedure,implementation,
requires,modifies,ensures,free,
% expressions
false,true,null,old,then,div,mod,
% statements
assert,assume,havoc,call,if,else,while,invariant,break,return,goto,
},
literate=%
{:}{$\colon$}1
{::}{$\bullet$}2
{:=}{$:$$=$}2
{!}{$\lnot$}1
{==}{$=$}1
{!=}{$\neq$}1
{&&}{$\land$}1
{||}{$\lor$}1
{<=}{$\le$}1
{>=}{$\ge$}1
{==>}{$\Longrightarrow$}3
{<==>}{$\Longleftrightarrow$}4
{forall}{$\forall$}1
{exists}{$\exists$}1
{lambda}{$\lambda$}1
% the following isn't actually Boogie, but it gives the option to produce nicer latex
{<<}{$\langle$}1
{>>}{$\rangle$}1
{\\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]{/*}{*/},
morestring=[b]",
numbers=none,
firstnumber=0,
numberstyle=\tiny,
stepnumber=5,
basicstyle=\scriptsize\sffamily,
commentstyle=\itshape,
keywordstyle=\bfseries,
ndkeywordstyle=\bfseries,
}
\lstnewenvironment{boogie}[1][]{%
\lstset{language=boogie,
floatplacement={tbp},captionpos=b,
frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}
\lstnewenvironment{boogieNoLines}[1][]{%
\lstset{language=boogie,
floatplacement={tbp},captionpos=b,
xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}
\def\inlineboogie{%
\lstinline[language=boogie,basicstyle=\ttfamily,columns=fixed]}
\newcommand{\lstfile}[1]{
\lstinputlisting[language=boogie,%
frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,columns=fixed]{#1}
}
|
