Initial set of files.

3 files changed, 284 insertions, 0 deletions

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}

+}