Initial set of files.

6 files changed, 631 insertions, 0 deletions

diff --git a/Util/Emacs/boogie-mode.el b/Util/Emacs/boogie-mode.el
new file mode 100644
index 00000000..1d8ffb05
--- /dev/null
+++ b/Util/Emacs/boogie-mode.el
@@ -0,0 +1,120 @@
+;; boogie-mode.el - GNU Emacs mode for Boogie 2

+;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why

+

+(defvar boogie-mode-hook nil)

+

+(defvar boogie-mode-map nil

+  "Keymap for Boogie major mode")

+

+(if boogie-mode-map nil

+  (setq boogie-mode-map (make-keymap))

+  (define-key boogie-mode-map "\C-c\C-c" 'boogie-run-boogie)

+  (define-key boogie-mode-map [(control return)] 'font-lock-fontify-buffer))

+

+(setq auto-mode-alist

+      (append

+       '(("\\.bpl" . boogie-mode))

+       auto-mode-alist))

+

+;; font-lock

+

+(defun boogie-regexp-opt (l)

+  (concat "\\<" (concat (regexp-opt l t) "\\>")))

+

+(defconst boogie-font-lock-keywords-1

+  (list

+   ; comments have the form /* ... */

+   '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face)

+   ; or // ...

+   '("//\\([^

+]\\)*" . font-lock-comment-face)

+

+   `(,(boogie-regexp-opt '(

+        "type" "const" "function" "axiom" "var" "procedure" "implementation"

+        "returns" "where" "requires" "ensures" "modifies" "free" "unique"

+        "invariant" "extends" "complete"

+        )) . font-lock-builtin-face)

+   `(,(boogie-regexp-opt '(

+        "assert" "assume" "break" "call" "else" "havoc" "if" "goto" "return" "while"

+        "old" "forall" "exists" "cast"

+        "false" "true")) . font-lock-keyword-face)

+   `(,(boogie-regexp-opt '("bool" "int"

+                             "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" ; and so on

+                             )) . font-lock-type-face)

+   )

+  "Minimal highlighting for Boogie mode")

+

+(defvar boogie-font-lock-keywords boogie-font-lock-keywords-1

+  "Default highlighting for Boogie mode")

+

+;; syntax

+

+(defvar boogie-mode-syntax-table nil

+  "Syntax table for boogie-mode")

+

+(defun boogie-create-syntax-table ()

+  (if boogie-mode-syntax-table

+      ()

+    (setq boogie-mode-syntax-table (make-syntax-table))

+    (set-syntax-table boogie-mode-syntax-table)

+    (modify-syntax-entry ?' "w" boogie-mode-syntax-table)

+    (modify-syntax-entry ?_ "w" boogie-mode-syntax-table)))

+

+;; menu

+

+(require 'easymenu)

+

+(defun boogie-menu ()

+  (easy-menu-define

+   boogie-mode-menu (list boogie-mode-map)

+   "Boogie Mode Menu." 

+   '("Boogie"

+     ["Run Boogie" boogie-run-boogie t]

+     "---"

+     ["Recolor buffer" font-lock-fontify-buffer t]

+     "---"

+     ))

+  (easy-menu-add boogie-mode-menu))

+

+;; commands

+

+(defun boogie-command-line (file)

+  (concat "boogie -nologo -abbrevOutput " file))

+

+(defun boogie-run-boogie ()

+  "run Boogie to check the Boogie program"

+  (interactive)

+  (let ((f (buffer-name)))

+    (compile (boogie-command-line f))))

+

+;; setting the mode

+

+(defun boogie-mode ()

+  "Major mode for editing Boogie programs.

+

+\\{boogie-mode-map}"

+  (interactive)

+  (kill-all-local-variables)

+  (boogie-create-syntax-table)

+  ; hilight

+  (make-local-variable 'font-lock-defaults)

+  (setq font-lock-defaults '(boogie-font-lock-keywords))

+  ; indentation

+  ; (make-local-variable 'indent-line-function)

+  ; (setq indent-line-function 'boogie-indent-line)

+  ; menu

+  ; providing the mode

+  (setq major-mode 'boogie-mode)

+  (setq mode-name "Boogie")

+  (use-local-map boogie-mode-map)

+  (font-lock-mode 1)

+  (boogie-menu)

+  (run-hooks 'boogie-mode-hook))

+

+(provide 'boogie-mode)

diff --git a/Util/Emacs/chalice-mode.el b/Util/Emacs/chalice-mode.el
new file mode 100644
index 00000000..91c69120
--- /dev/null
+++ b/Util/Emacs/chalice-mode.el
@@ -0,0 +1,115 @@
+;; chalice-mode.el - GNU Emacs mode for Chalice

+;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why

+

+(defvar chalice-mode-hook nil)

+

+(defvar chalice-mode-map nil

+  "Keymap for Chalice major mode")

+

+(if chalice-mode-map nil

+  (setq chalice-mode-map (make-keymap))

+  (define-key chalice-mode-map "\C-c\C-c" 'chalice-run-boogie)

+  (define-key chalice-mode-map [(control return)] 'font-lock-fontify-buffer))

+

+(setq auto-mode-alist

+      (append

+       '(("\\.chalice" . chalice-mode))

+       auto-mode-alist))

+

+;; font-lock

+

+(defun chalice-regexp-opt (l)

+  (concat "\\<" (concat (regexp-opt l t) "\\>")))

+

+(defconst chalice-font-lock-keywords-1

+  (list

+   ; comments have the form /* ... */

+   '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face)

+   ; or // ...

+   '("//\\([^

+]\\)*" . font-lock-comment-face)

+

+   `(,(chalice-regexp-opt '(

+        "class" "ghost" "var" "const" "external" "function" "method"

+        "predicate" "returns" "requires" "ensures" "lockchange"

+        "invariant"

+        )) . font-lock-builtin-face)

+   `(,(chalice-regexp-opt '(

+        "above" "acc" "acquire" "and" "assert" "assigned" "assume"

+        "below" "between" "call"

+        "downgrade" "else" "eval" "exists" "fold" "forall" "fork" "free" "havoc" "holds"

+        "if" "in" "install" "ite" "join" "lock" "lockbottom" "maxlock" "module" "new" "nil"

+        "old" "rd" "release" "result" "share" "this" "unfold" "unfolding" "unshare" "while"

+        "false" "true" "null")) . font-lock-keyword-face)

+   `(,(chalice-regexp-opt '("bool" "int" "seq" "token")) . font-lock-type-face)

+   )

+  "Minimal highlighting for Chalice mode")

+

+(defvar chalice-font-lock-keywords chalice-font-lock-keywords-1

+  "Default highlighting for Chalice mode")

+

+;; syntax

+

+(defvar chalice-mode-syntax-table nil

+  "Syntax table for chalice-mode")

+

+(defun chalice-create-syntax-table ()

+  (if chalice-mode-syntax-table

+      ()

+    (setq chalice-mode-syntax-table (make-syntax-table))

+    (set-syntax-table chalice-mode-syntax-table)

+    (modify-syntax-entry ?' "w" chalice-mode-syntax-table)

+    (modify-syntax-entry ?_ "w" chalice-mode-syntax-table)))

+

+;; menu

+

+(require 'easymenu)

+

+(defun chalice-menu ()

+  (easy-menu-define

+   chalice-mode-menu (list chalice-mode-map)

+   "Chalice Mode Menu." 

+   '("Chalice"

+     ["Run Boogie" chalice-run-boogie t]

+     "---"

+     ["Recolor buffer" font-lock-fontify-buffer t]

+     "---"

+     ))

+  (easy-menu-add chalice-mode-menu))

+

+;; commands

+

+(defun chalice-command-line (file)

+  (concat "boogie " file))

+

+(defun chalice-run-boogie ()

+  "run Boogie to check the Chalice program"

+  (interactive)

+  (let ((f (buffer-name)))

+    (compile (chalice-command-line f))))

+

+;; setting the mode

+

+(defun chalice-mode ()

+  "Major mode for editing Chalice programs.

+

+\\{chalice-mode-map}"

+  (interactive)

+  (kill-all-local-variables)

+  (chalice-create-syntax-table)

+  ; hilight

+  (make-local-variable 'font-lock-defaults)

+  (setq font-lock-defaults '(chalice-font-lock-keywords))

+  ; indentation

+  ; (make-local-variable 'indent-line-function)

+  ; (setq indent-line-function 'chalice-indent-line)

+  ; menu

+  ; providing the mode

+  (setq major-mode 'chalice-mode)

+  (setq mode-name "Chalice")

+  (use-local-map chalice-mode-map)

+  (font-lock-mode 1)

+  (chalice-menu)

+  (run-hooks 'chalice-mode-hook))

+

+(provide 'chalice-mode)

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
new file mode 100644
index 00000000..508ffbaf
--- /dev/null
+++ b/Util/Emacs/dafny-mode.el
@@ -0,0 +1,112 @@
+;; dafny-mode.el - GNU Emacs mode for Dafny

+;; Adapted by Rustan Leino from Jean-Christophe FILLIATRE's GNU Emancs mode for Why

+

+(defvar dafny-mode-hook nil)

+

+(defvar dafny-mode-map nil

+  "Keymap for Dafny major mode")

+

+(if dafny-mode-map nil

+  (setq dafny-mode-map (make-keymap))

+  (define-key dafny-mode-map "\C-c\C-c" 'dafny-run-boogie)

+  (define-key dafny-mode-map [(control return)] 'font-lock-fontify-buffer))

+

+(setq auto-mode-alist

+      (append

+       '(("\\.dfy" . dafny-mode))

+       auto-mode-alist))

+

+;; font-lock

+

+(defun dafny-regexp-opt (l)

+  (concat "\\<" (concat (regexp-opt l t) "\\>")))

+

+(defconst dafny-font-lock-keywords-1

+  (list

+   ; comments have the form /* ... */

+   '("/\\*\\([^*]\\|\\*[^/]\\)*\\*/" . font-lock-comment-face)

+   ; or // ...

+   '("//\\([^

+]\\)*" . font-lock-comment-face)

+

+   `(,(dafny-regexp-opt '(

+        "class" "function" "frame" "var" "method"

+        "returns" "requires" "ensures" "modifies" "reads" "free"

+        "invariant" "decreases"

+        )) . font-lock-builtin-face)

+   `(,(dafny-regexp-opt '(

+        "assert" "assume" "break" "call" "else" "havoc" "if" "label" "return" "while"

+        "old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "use"

+        "false" "true" "null")) . font-lock-keyword-face)

+   `(,(dafny-regexp-opt '("bool" "int" "object" "set" "seq")) . font-lock-type-face)

+   )

+  "Minimal highlighting for Dafny mode")

+

+(defvar dafny-font-lock-keywords dafny-font-lock-keywords-1

+  "Default highlighting for Dafny mode")

+

+;; syntax

+

+(defvar dafny-mode-syntax-table nil

+  "Syntax table for dafny-mode")

+

+(defun dafny-create-syntax-table ()

+  (if dafny-mode-syntax-table

+      ()

+    (setq dafny-mode-syntax-table (make-syntax-table))

+    (set-syntax-table dafny-mode-syntax-table)

+    (modify-syntax-entry ?' "w" dafny-mode-syntax-table)

+    (modify-syntax-entry ?_ "w" dafny-mode-syntax-table)))

+

+;; menu

+

+(require 'easymenu)

+

+(defun dafny-menu ()

+  (easy-menu-define

+   dafny-mode-menu (list dafny-mode-map)

+   "Dafny Mode Menu." 

+   '("Dafny"

+     ["Run Boogie" dafny-run-boogie t]

+     "---"

+     ["Recolor buffer" font-lock-fontify-buffer t]

+     "---"

+     ))

+  (easy-menu-add dafny-mode-menu))

+

+;; commands

+

+(defun dafny-command-line (file)

+  (concat "boogie " file))

+

+(defun dafny-run-boogie ()

+  "run Boogie to check the Dafny program"

+  (interactive)

+  (let ((f (buffer-name)))

+    (compile (dafny-command-line f))))

+

+;; setting the mode

+

+(defun dafny-mode ()

+  "Major mode for editing Dafny programs.

+

+\\{dafny-mode-map}"

+  (interactive)

+  (kill-all-local-variables)

+  (dafny-create-syntax-table)

+  ; hilight

+  (make-local-variable 'font-lock-defaults)

+  (setq font-lock-defaults '(dafny-font-lock-keywords))

+  ; indentation

+  ; (make-local-variable 'indent-line-function)

+  ; (setq indent-line-function 'dafny-indent-line)

+  ; menu

+  ; providing the mode

+  (setq major-mode 'dafny-mode)

+  (setq mode-name "Dafny")

+  (use-local-map dafny-mode-map)

+  (font-lock-mode 1)

+  (dafny-menu)

+  (run-hooks 'dafny-mode-hook))

+

+(provide 'dafny-mode)

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}

+}