Dafny:

 * Allow (and currently ignore) "ghost" modifier.
 * Fixed bug in boxing.
 * Check for div-by-zero error for modulo operator.
 * Improved emacs and latex modes.

1 files changed, 7 insertions, 3 deletions

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index f334e770..f88c3b54 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -7,9 +7,9 @@
 \lstdefinelanguage{dafny}{

   morekeywords={class,datatype,bool,int,object,set,seq,%

       function,returns,

-      var,

+      ghost,var,

       method,in,

-      requires,modifies,ensures,reads,free,

+      requires,modifies,ensures,reads,decreases,free,

       % expressions

       match,case,false,true,null,old,fresh,this,

       % statements

@@ -20,15 +20,18 @@
     {::}{$\bullet$}2

     {:=}{$:$$=$}2

     {!}{$\lnot$}1

-    {!!}{$\nparallel$}1

+    {!!}{$\not\cap$}1

     {==}{$=$}1

     {!=}{$\neq$}1

     {&&}{$\land$}1

     {||}{$\lor$}1

     {<=}{$\le$}1

     {=>}{$\ge$}1

+    % the following isn't actually Dafny, but it gives the option to produce nicer latex

+    {|=>}{$\Rightarrow$}2

     {<=set}{$\subseteq$}1

     {+set}{$\cup$}1

+    {*set}{$\cap$}1

     {==>}{$\Longrightarrow$}3 

     {<==>}{$\Longleftrightarrow$}4 

     {forall}{$\forall$}1

@@ -38,6 +41,7 @@
     % the following isn't actually Dafny, but it gives the option to produce nicer latex

     {<<}{$\langle$}1

     {>>}{$\rangle$}1

+    {...}{$\ldots$}1

     {\\alpha}{$\alpha$}1

     {\\beta}{$\beta$}1

     {\\gamma}{$\gamma$}1