From 9368c8aa9d95ae4e1cfbed54c2996c6ef41d61b3 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 11 Oct 2012 19:24:41 -0700 Subject: New feature: * Added "comethod" declarations and support for writing manual co-inductive proofs (but currently blindly assume comethod postconditions to, in positive positions, only have copredicates and codatatype equalities--other cases still need to be dealt with) Code restructuring: * New set of Boogie procedure stubs generated for each other * Start of improvements around TrSplitExpr --- Util/latex/dafny.sty | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Util/latex') diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 879b90cb..8ac9defe 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -9,7 +9,8 @@ bool,nat,int,object,set,multiset,seq,array,array2,array3,map, function,predicate,copredicate, ghost,var,static,refines, - method,constructor,returns,yields,module,import,default,opened,as,in, + method,constructor,comethod, + returns,yields,module,import,default,opened,as,in, requires,modifies,ensures,reads,decreases,free, % expressions match,case,false,true,null,old,fresh,choose,this, -- cgit v1.2.3