Dafny: Improved default decreases clauses for methods and functions

Dafny:  Don't display "alloc" field in BVD
Chalice:  Fixed error-message parsing error in VS mode

5 files changed, 0 insertions, 17 deletions

diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
index 70b38a5d..540225a1 100644
--- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
+++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
@@ -166,7 +166,6 @@ class LinkedList<T> {
   }

 

   static function method ReverseSeq(s: seq<T>): seq<T>

-    decreases s;

   {

     if s == [] then [] else

     ReverseSeq(s[1..]) + [s[0]]

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 9e4da459..197d6916 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -10,7 +10,6 @@ datatype Expr {
 }

 

 static function Subst(e: Expr, v: int, val: int): Expr

-  decreases e;

 {

   match e

   case Const(c) => e

@@ -19,7 +18,6 @@ static function Subst(e: Expr, v: int, val: int): Expr
 }

 

 static function SubstList(l: List, v: int, val: int): List

-  decreases l;

 {

   match l

   case Nil => l

@@ -28,7 +26,6 @@ static function SubstList(l: List, v: int, val: int): List
 

 static ghost method Theorem(e: Expr, v: int, val: int)

   ensures Subst(Subst(e, v, val), v, val) == Subst(e, v, val);

-  decreases e;

 {

   match e {

     case Const(c) =>

@@ -40,7 +37,6 @@ static ghost method Theorem(e: Expr, v: int, val: int)
 

 static ghost method Lemma(l: List, v: int, val: int)

   ensures SubstList(SubstList(l, v, val), v, val) == SubstList(l, v, val);

-  decreases l;

 {

   match l {

     case Nil =>

@@ -110,7 +106,6 @@ static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>,
   ensures |SubstSeq(parent, q, v, val)| == |q|;

   ensures (forall k :: 0 <= k && k < |q| ==>

             SubstSeq(parent, q, v, val)[k] == Substitute(q[k], v, val));

-  decreases q;

 {

   if (q == []) {

   } else {

diff --git a/Test/dafny1/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy
index b4fab490..2fecaee5 100644
--- a/Test/dafny1/SumOfCubes.dfy
+++ b/Test/dafny1/SumOfCubes.dfy
@@ -43,7 +43,6 @@ class SumOfCubes {
 

   static function GSum(k: int): int

     requires 0 <= k;

-    decreases k;

   {

     if k == 0 then 0 else GSum(k-1) + k-1

   }

@@ -86,7 +85,6 @@ class SumOfCubes {
 

   static function SumEmDown(n: int, m: int): int

     requires 0 <= n && n <= m;

-    decreases m;

   {

     if m == n then 0 else SumEmDown(n, m-1) + (m-1)*(m-1)*(m-1)

   }

diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
index 6b63bfec..fb530258 100644
--- a/Test/dafny1/TerminationDemos.dfy
+++ b/Test/dafny1/TerminationDemos.dfy
@@ -3,7 +3,6 @@ class Example {
   {

     var i := 0;

     while (i < n)

-      decreases n - i;

     {

       i := i + 1;

     }

@@ -14,7 +13,6 @@ class Example {
 

 class Fibonacci {

   function Fib(n: int): int

-    decreases n;

   {

     if n < 2 then n else Fib(n-2) + Fib(n-1)

   }

@@ -24,7 +22,6 @@ class Fibonacci {
 

 class Ackermann {

   function F(m: int, n: int): int

-    decreases m, n;

   {

     if m <= 0 then

       n + 1

diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy
index 58124171..7fc62feb 100644
--- a/Test/dafny1/TreeDatatype.dfy
+++ b/Test/dafny1/TreeDatatype.dfy
@@ -10,14 +10,12 @@ datatype Tree {
 }

 

 static function Inc(t: Tree): Tree

-  decreases t;

 {

   match t

   case Node(n, children) => #Tree.Node(n+1, ForestInc(children))

 }

 

 static function ForestInc(forest: List<Tree>): List<Tree>

-  decreases forest;

 {

   match forest

   case Nil => forest

@@ -31,14 +29,12 @@ datatype GTree<T> {
 }

 

 static function GInc(t: GTree<int>): GTree<int>

-  decreases t;

 {

   match t

   case Node(n, children) => #GTree.Node(n+1, GForestInc(children))

 }

 

 static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>

-  decreases forest;

 {

   match forest

   case Nil => forest

@@ -57,14 +53,12 @@ datatype OneTree {
 }

 

 static function XInc(t: OneTree): OneTree

-  decreases t;

 {

   match t

   case Node(n, children) => #OneTree.Node(n+1, XForestInc(children))

 }

 

 static function XForestInc(forest: TreeList): TreeList

-  decreases forest;

 {

   match forest

   case Nil => forest