From f877aa3ee16efb5209edc8794934c37ae067954c Mon Sep 17 00:00:00 2001 From: Nadia Polikarpova Date: Sun, 16 Sep 2012 14:25:58 +0200 Subject: Added the new keyword (calc) to Util --- Util/Emacs/dafny-mode.el | 2 +- Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 3 ++- Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 1 + Util/latex/dafny.sty | 2 +- Util/vim/syntax/dafny.vim | 2 +- 5 files changed, 6 insertions(+), 4 deletions(-) (limited to 'Util') diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index e658bfe9..1e197644 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -38,7 +38,7 @@ )) . font-lock-builtin-face) `(,(dafny-regexp-opt '( "assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "while" "print" "where" - "old" "forall" "exists" "new" "parallel" "in" "this" "fresh" + "old" "forall" "exists" "new" "parallel" "calc" "in" "this" "fresh" "match" "case" "false" "true" "null")) . font-lock-keyword-face) `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "nat" "int" "object" "set" "seq")) . font-lock-type-face) ) diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 81dd0dd1..8c3eee59 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -28,7 +28,7 @@ namespace Demo "in", "forall", "exists", "seq", "set", "map", "multiset", "array", "array2", "array3", "match", "case", - "fresh", "old", "choose", "where" + "fresh", "old", "choose", "where", "calc" ); StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote); @@ -289,6 +289,7 @@ namespace Demo | "label" | "return" | "parallel" + | "calc" | "print" | "returns" | "requires" diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index 5853f180..19f98ff7 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -231,6 +231,7 @@ namespace DafnyLanguage case "assume": case "bool": case "break": + case "calc": case "case": case "choose": case "class": diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 81b04694..d60488d1 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -13,7 +13,7 @@ % expressions match,case,false,true,null,old,fresh,choose,this, % statements - assert,assume,print,new,if,then,else,while,invariant,break,label,return,parallel,where + assert,assume,print,new,if,then,else,while,invariant,break,label,return,parallel,where,calc }, literate=% {:}{$\colon$}1 diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index c61e5ebc..cc1c9d79 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -9,7 +9,7 @@ syntax keyword dafnyFunction function predicate copredicate method constructor syntax keyword dafnyTypeDef class datatype codatatype type module import opened as default syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat while parallel -syntax keyword dafnyStatement assume assert return new print break label where +syntax keyword dafnyStatement assume assert return new print break label where calc syntax keyword dafnyKeyword var ghost returns null static this refines syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map syntax keyword dafnyLogic requires ensures modifies reads decreases invariant -- cgit v1.2.3 From 458fa29bb7c59c3b7345ac21b20820f42d550ccc Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 21 Sep 2012 14:46:50 -0700 Subject: DafnyExtension: adding some missing keywords (for imports) --- Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'Util') diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index 19f98ff7..ec1514ae 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -227,6 +227,7 @@ namespace DafnyLanguage #region keywords case "allocated": case "array": + case "as": case "assert": case "assume": case "bool": @@ -250,7 +251,7 @@ namespace DafnyLanguage case "function": case "ghost": case "if": - case "imports": + case "import": case "in": case "int": case "invariant": @@ -265,6 +266,7 @@ namespace DafnyLanguage case "null": case "object": case "old": + case "opened": case "parallel": case "predicate": case "print": -- cgit v1.2.3 From 6d7e1ebc89767bfcc0cad74e7fc1be6c5efd0f4a Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 27 Sep 2012 14:01:18 -0700 Subject: DafnyExtension: make it usable also in Visual Studio 2012 --- Util/VS2010/DafnyExtension/DafnyExtension.sln | 4 ++-- .../DafnyExtension/DafnyExtension/DafnyExtension.csproj | 14 +++++++++++++- .../DafnyExtension/source.extension.vsixmanifest | 3 +++ 3 files changed, 18 insertions(+), 3 deletions(-) (limited to 'Util') diff --git a/Util/VS2010/DafnyExtension/DafnyExtension.sln b/Util/VS2010/DafnyExtension/DafnyExtension.sln index e7391254..fd450cc8 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension.sln +++ b/Util/VS2010/DafnyExtension/DafnyExtension.sln @@ -1,6 +1,6 @@  -Microsoft Visual Studio Solution File, Format Version 11.00 -# Visual Studio 2010 +Microsoft Visual Studio Solution File, Format Version 12.00 +# Visual Studio 2012 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyExtension", "DafnyExtension\DafnyExtension.csproj", "{6E9A5E14-0763-471C-A129-80A879D9E7BA}" EndProject Global diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj index 66370dec..2580c396 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj @@ -1,5 +1,6 @@  + Debug AnyCPU @@ -14,6 +15,12 @@ v4.0 512 false + 11.0 + + + + + 4.0 true @@ -158,8 +165,13 @@ + + 10.0 + $(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion) + - + + cd diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest index d822fbfc..ef5c1cf5 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest +++ b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest @@ -10,6 +10,9 @@ Pro + + Pro + -- cgit v1.2.3 From 2d2475362e0eaaa072464c87dd4a8ae98c0c3d2a Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 28 Sep 2012 15:19:53 -0700 Subject: Dafny: removed div/mod axioms, since Boogie now interprets div/mod Dafny: included FloydCycleDetect again (which had been temporarily commented out) DafnyExtension: adjusted to Boogie's change in abstract-interpretation support --- Binaries/DafnyPrelude.bpl | 15 --------------- Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy | 9 --------- Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs | 3 --- 3 files changed, 27 deletions(-) (limited to 'Util') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 53e8e86a..5530f8a7 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -610,18 +610,3 @@ type TickType; var $Tick: TickType; // --------------------------------------------------------------- -// -- Arithmetic ------------------------------------------------- -// --------------------------------------------------------------- - -// the connection between mod and div -axiom (forall x:int, y:int :: {x mod y} {x div y} x mod y == x - x div y * y); - -// remainder is always Euclidean Modulus. -axiom (forall x:int, y:int :: {x mod y} 0 < y ==> 0 <= x mod y && x mod y < y); -axiom (forall x:int, y:int :: {x mod y} y < 0 ==> 0 <= x mod y && x mod y < -y); - -// the following axiom has some unfortunate matching, but it does state a property about mod that -// is sometimes useful -axiom (forall a: int, b: int, d: int :: { a mod d, b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b); - -// --------------------------------------------------------------- diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy index 3f68ee5d..774008b8 100644 --- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy +++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy @@ -205,7 +205,6 @@ class Node { invariant forall k,l :: 0 <= k < l < steps ==> Nexxxt(k, S) != Nexxxt(l, S); decreases S - Visited; { -assume 2<2; // TEMPORARY HACK p, steps, Visited := p.next, steps + 1, Visited + {p}; } if (p == null) { @@ -219,7 +218,6 @@ assume 2<2; // TEMPORARY HACK invariant forall k :: 0 <= k < A ==> Nexxxt(k, S) != p; decreases steps - A; { -assume 2<2; // TEMPORARY HACK A := A + 1; } B := steps - A; @@ -228,13 +226,6 @@ assume 2<2; // TEMPORARY HACK } } -/** TEMPORARY - ghost method AnalyzeList_Aux(S: set, steps: int, p: Node) returns (A: int) - ensures 0 <= A < steps; - ensures forall k :: 0 <= k < A ==> Nexxxt(k, S) != p; - ensures Nexxxt(A, S) == p; -**/ - ghost method CrucialLemma(a: int, b: int, S: set) requires IsClosed(S); requires 0 <= a && 1 <= b; diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs index 9f22b887..c691d9da 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs @@ -231,9 +231,6 @@ namespace DafnyLanguage if (Bpl.CommandLineOptions.Clo.UseAbstractInterpretation) { if (Bpl.CommandLineOptions.Clo.Ai.J_Intervals || Bpl.CommandLineOptions.Clo.Ai.J_Trivial) { Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program); - } else if (Bpl.CommandLineOptions.Clo.Ai.AnySet) { - // run one of the old domains - Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program); } else { // use /infer:j as the default Bpl.CommandLineOptions.Clo.Ai.J_Intervals = true; -- cgit v1.2.3 From 17a14997cbcdad8bb0a435cf48dfb783ea21f3ac Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 3 Oct 2012 12:32:19 -0700 Subject: bunch of refactorings - moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs --- DafnyDriver/DafnyDriver.cs | 8 +------- Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs | 6 +----- 2 files changed, 2 insertions(+), 12 deletions(-) (limited to 'Util') diff --git a/DafnyDriver/DafnyDriver.cs b/DafnyDriver/DafnyDriver.cs index 39733c8e..80f78d16 100644 --- a/DafnyDriver/DafnyDriver.cs +++ b/DafnyDriver/DafnyDriver.cs @@ -571,13 +571,7 @@ namespace Microsoft.Dafny ConditionGeneration vcgen = null; try { - if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) - { - vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); - } else - { - vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); - } + vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend); } catch (ProverException e) { diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs index c691d9da..39829bb0 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs @@ -255,11 +255,7 @@ namespace DafnyLanguage ConditionGeneration vcgen = null; try { - if (Bpl.CommandLineOptions.Clo.vcVariety == Bpl.CommandLineOptions.VCVariety.Doomed) { - vcgen = new DCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend); - } else { - vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend); - } + vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend); } catch (Bpl.ProverException) { return PipelineOutcome.FatalError; } -- cgit v1.2.3