branch merge

8 files changed, 72 insertions, 15 deletions

diff --git a/.hgtags b/.hgtags
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/.hgtags
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 708c4c06..33b6d39d 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5173,9 +5173,11 @@ namespace Microsoft.Dafny {
           foreach (var n in inductionVariables) {

             var newCases = new List<Bpl.Expr>();

             foreach (var kase in InductionCases(n.Type, nn[i], etran)) {

-              if (kase != Bpl.Expr.True) {  // if there's no case, don't add anything to the token

-                foreach (var cs in caseProduct) {

+              foreach (var cs in caseProduct) {

+                if (kase != Bpl.Expr.True) {  // if there's no case, don't add anything to the token

                   newCases.Add(Bpl.Expr.Binary(new NestedToken(cs.tok, kase.tok), Bpl.BinaryOperator.Opcode.And, cs, kase));

+                } else {

+                  newCases.Add(cs);

                 }

               }

             }

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 68027609..1c7286e7 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -15,7 +15,6 @@ namespace Microsoft.Boogie.ModelViewer
 {

   public partial class Main : Form

   {

-    string SearchText;

     SkeletonItem unfoldingRoot;

     SkeletonItem[] allItems;

     int currentState, previousState = -1;

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 2fd70cc2..0cd0c5b5 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -43,6 +43,10 @@ Dafny program verifier finished with 9 verified, 0 errors
 

 Dafny program verifier finished with 8 verified, 0 errors

 

+-------------------- pow2.dfy --------------------

+

+Dafny program verifier finished with 8 verified, 0 errors

+

 -------------------- SchorrWaite.dfy --------------------

 

 Dafny program verifier finished with 10 verified, 0 errors

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index f31d79f8..c3daad9e 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -119,12 +119,12 @@ class IntegerInduction {
   // possibility of applying induction.  Instead, the "==>" and "<==" cases are given separately.

   // Proving the "<==" case is simple; it's the "==>" case that requires induction.

   // The example uses an attribute that requests induction on just "j".  However, the proof also

-  // goes through by applying induction just on "i" or applying induction on both bound variables.

+  // goes through by applying induction on both bound variables.

   function method IsSorted(s: seq<int>): bool

     ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]);

     ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s);

   {

-    (forall i :: 0 <= i && i+1 < |s| ==> s[i] <= s[i+1])

+    (forall i :: 1 <= i && i < |s| ==> s[i-1] <= s[i])

   }

 }

 

diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy
new file mode 100644
index 00000000..52cddaac
--- /dev/null
+++ b/Test/dafny1/pow2.dfy
@@ -0,0 +1,54 @@
+// This is a Dafny adaptation of a Coq program by David Pichardie.

+

+function IsEven(n: int): bool

+  requires 0 <= n;

+  ensures IsEven(n) ==> n == (n/2)+(n/2);

+{

+  (n/2)*2 == n

+}

+

+function Square(n: int): int { n * n }

+

+function pow2(n: int): int

+  requires 0 <= n;

+  ensures 0 <= pow2(n);

+{

+  if n == 0 then

+    1

+  else if IsEven(n) then

+    Square(pow2(n / 2))

+  else

+    2*pow2(n-1)

+

+}

+

+function pow2_slow(n: int): int

+  requires 0 <= n;

+{

+  if n == 0 then

+    1

+  else

+    2*pow2_slow(n-1)

+}

+

+ghost method Lemma(n: int)

+  requires 0 <= n && IsEven(n);

+  ensures pow2_slow(n) == Square(pow2_slow(n/2));

+{

+  if (n != 0) {

+    call Lemma(n-2);

+  }

+}

+

+ghost method Theorem(n: int)

+  requires 0 <= n;

+  ensures pow2(n) == pow2_slow(n);

+{

+  if (n == 0) {

+  } else if (IsEven(n)) {

+    call Lemma(n);

+    call Theorem(n/2);

+  } else {

+    call Theorem(n-1);

+  }

+}

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 8d34dfc0..b6fc7f62 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -16,7 +16,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy
             UnboundedStack.dfy

             SeparationLogicList.dfy

             ListCopy.dfy ListReverse.dfy ListContents.dfy

-            MatrixFun.dfy

+            MatrixFun.dfy pow2.dfy

             SchorrWaite.dfy

             Cubes.dfy SumOfCubes.dfy

             TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy

diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log
index b255508d..d1b3cd6d 100644
--- a/_admin/Boogie/aste/summary.log
+++ b/_admin/Boogie/aste/summary.log
@@ -1,11 +1,10 @@
-# Aste started: 2011-04-02 07:00:17

+# Aste started: 2011-04-05 14:33:00

 # Host id: Boogiebox

-# [2011-04-02 07:02:48] SpecSharp revision: e47e2d10ac81

-# [2011-04-02 07:02:48] SscBoogie revision: e47e2d10ac81

-# [2011-04-02 07:04:02] Boogie revision: 65019

-[2011-04-02 07:06:38] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

+# [2011-04-05 14:35:37] SpecSharp revision: 40cb7c139809

+# [2011-04-05 14:35:37] SscBoogie revision: 40cb7c139809

+# [2011-04-05 14:36:59] Boogie revision: 445ca894f870

+[2011-04-05 14:38:55] C:\Program Files (x86)\Microsoft Visual Studio 10.0\Common7\IDE\devenv.com Boogie.sln /Rebuild Checked

 

-    D:\Temp\aste\Boogie\Source\ModelViewer\Main.cs(18,12): warning CS0169: The field 'Microsoft.Boogie.ModelViewer.Main.SearchText' is never used


     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(823,16): warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     D:\Temp\aste\Boogie\Source\Core\AbsyType.cs(2802,16): warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     D:\Temp\aste\Boogie\Source\Core\OOLongUtil.cs(109,7): warning CS0162: Unreachable code detected


@@ -19,7 +18,6 @@
     D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1597,11): warning CS0162: Unreachable code detected


     D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(1753,11): warning CS0162: Unreachable code detected


     D:\Temp\aste\Boogie\Source\VCGeneration\StratifiedVC.cs(662,17): warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.


-    warning CS0169: The field 'Microsoft.Boogie.ModelViewer.Main.SearchText' is never used


     warning CS0659: 'Microsoft.Boogie.BasicType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     warning CS0659: 'Microsoft.Boogie.CtorType' overrides Object.Equals(object o) but does not override Object.GetHashCode()


     warning CS0162: Unreachable code detected


@@ -33,5 +31,5 @@
     warning CS0162: Unreachable code detected


     warning CS0162: Unreachable code detected


     warning CC1032: Method 'VC.StratifiedVCGen+NormalChecker.CheckVC' overrides 'VC.StratifiedVCGen+StratifiedCheckerInterface.CheckVC', thus cannot add Requires.


-[2011-04-02 07:48:50] 0 out of 30 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

-# [2011-04-02 07:49:52] Released nightly of Boogie

+[2011-04-05 15:20:55] 0 out of 30 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed

+# [2011-04-05 15:21:59] Released nightly of Boogie