summaryrefslogtreecommitdiff
path: root/Util
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2010-05-21 18:38:47 +0000
committerGravatar rustanleino <unknown>2010-05-21 18:38:47 +0000
commit2fc9a47b200589fae14f698e7546553a0b31aec2 (patch)
treeae0fd61bcd66c4f92833c33f82de518a718bfb7c /Util
parent9657b7042a5a55fe96bc9b7560c473876d7efa60 (diff)
Dafny:
* Added arrays * Beefed up set axiomatization to know more things about set displays * Added a simple heuristic that can infer some simple decreases clauses for loops * Added Dafny solutions to a couple of VACID benchmarks
Diffstat (limited to 'Util')
-rw-r--r--Util/Emacs/dafny-mode.el2
-rw-r--r--Util/latex/dafny.sty2
2 files changed, 2 insertions, 2 deletions
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 7b5de59a..20f4477b 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -39,7 +39,7 @@
"assert" "assume" "break" "call" "then" "else" "havoc" "if" "label" "return" "while" "print"
"old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "use"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
- `(,(dafny-regexp-opt '("bool" "int" "object" "set" "seq")) . font-lock-type-face)
+ `(,(dafny-regexp-opt '("array" "bool" "int" "object" "set" "seq")) . font-lock-type-face)
)
"Minimal highlighting for Dafny mode")
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 1f891a71..dd44665a 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -5,7 +5,7 @@
\usepackage{listings}
\lstdefinelanguage{dafny}{
- morekeywords={class,datatype,bool,int,object,set,seq,%
+ morekeywords={class,datatype,bool,int,object,set,seq,array,%
function,unlimited,
ghost,var,static,
method,returns,module,imports,in,