diff options
Diffstat (limited to 'Util/latex/boogie.sty')
-rw-r--r-- | Util/latex/boogie.sty | 242 |
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} +} |