summaryrefslogtreecommitdiff
path: root/Util/latex/boogie.sty
diff options
context:
space:
mode:
Diffstat (limited to 'Util/latex/boogie.sty')
-rw-r--r--Util/latex/boogie.sty242
1 files changed, 121 insertions, 121 deletions
diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty
index e67c61f4..65fa7fb1 100644
--- a/Util/latex/boogie.sty
+++ b/Util/latex/boogie.sty
@@ -1,121 +1,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}
-}
+% 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}
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 06:13:15 +0000