From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001
From: mikebarnett <unknown>
Date: Wed, 15 Jul 2009 21:03:41 +0000
Subject: Initial set of files.

---
 Util/latex/boogie.sty  | 120 +++++++++++++++++++++++++++++++++++++++++++++++++
 Util/latex/chalice.sty |  63 ++++++++++++++++++++++++++
 Util/latex/dafny.sty   | 101 +++++++++++++++++++++++++++++++++++++++++
 3 files changed, 284 insertions(+)
 create mode 100644 Util/latex/boogie.sty
 create mode 100644 Util/latex/chalice.sty
 create mode 100644 Util/latex/dafny.sty

(limited to 'Util/latex')

diff --git a/Util/latex/boogie.sty b/Util/latex/boogie.sty
new file mode 100644
index 00000000..bda9f10a
--- /dev/null
+++ b/Util/latex/boogie.sty
@@ -0,0 +1,120 @@
+% 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,finite,bool,int,ref,%
+      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,
+      % 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
+    % 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}
+}
diff --git a/Util/latex/chalice.sty b/Util/latex/chalice.sty
new file mode 100644
index 00000000..f9ba5234
--- /dev/null
+++ b/Util/latex/chalice.sty
@@ -0,0 +1,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}
+}
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
new file mode 100644
index 00000000..9f7a76b3
--- /dev/null
+++ b/Util/latex/dafny.sty
@@ -0,0 +1,101 @@
+% dafny.sty
+% Dafny mode for the LaTeX listings package.
+% Rustan Leino, 22 June 2008.
+
+\usepackage{listings}
+
+\lstdefinelanguage{dafny}{
+  morekeywords={class,bool,int,object,set,seq,%
+      function,returns,
+      var,
+      method,in,
+      requires,modifies,ensures,reads,free,
+      % expressions
+      false,true,null,old,fresh,this,
+      % statements
+      assert,assume,new,havoc,call,if,else,while,invariant,break,return,foreach,
+      },
+  literate=%
+    {:}{$\colon$}1
+    {::}{$\bullet$}2
+    {:=}{$:$$=$}2
+    {!}{$\lnot$}1
+    {!!}{$\nparallel$}1
+    {==}{$=$}1
+    {!=}{$\neq$}1
+    {&&}{$\land$}1
+    {||}{$\lor$}1
+    {<=}{$\le$}1
+    {=>}{$\ge$}1
+    {<=set}{$\subseteq$}1
+    {+set}{$\cup$}1
+    {==>}{$\Longrightarrow$}3 
+    {<==>}{$\Longleftrightarrow$}4 
+    {forall}{$\forall$}1
+    {exists}{$\exists$}1
+    {\\in}{$\in$}1
+    % the following isn't actually Dafny, 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{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}
+}
-- 
cgit v1.2.3