From 2fc9a47b200589fae14f698e7546553a0b31aec2 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Fri, 21 May 2010 18:38:47 +0000 Subject: 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 --- Util/latex/dafny.sty | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Util/latex') 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, -- cgit v1.2.3