Merge

4 files changed, 205 insertions, 11 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 085ef78a..8f138bcd 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1701,37 +1701,56 @@ Execution trace:
 

 Dafny program verifier finished with 1 verified, 4 errors

 

--------------------- Superposition.dfy --------------------

+-------------------- Computations.dfy --------------------

+

+Dafny program verifier finished with 46 verified, 0 errors

+

+-------------------- ComputationsNeg.dfy --------------------

+ComputationsNeg.dfy(4,3): Error: failure to decrease termination measure

+Execution trace:

+    (0,0): anon3_Else

+ComputationsNeg.dfy(8,1): Error BP5003: A postcondition might not hold on this return path.

+ComputationsNeg.dfy(7,17): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+ComputationsNeg.dfy(20,1): Error BP5003: A postcondition might not hold on this return path.

+ComputationsNeg.dfy(19,11): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 3 verified, 3 errors

 

+-------------------- Superposition.dfy --------------------

+
 Verifying CheckWellformed$$_0_M0.C.M ...

   [0 proof obligations]  verified

-

+
 Verifying Impl$$_0_M0.C.M ...

   [4 proof obligations]  verified

-

+
 Verifying CheckWellformed$$_0_M0.C.P ...

   [4 proof obligations]  verified

-

+
 Verifying CheckWellformed$$_0_M0.C.Q ...

   [3 proof obligations]  error

 Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon5_Else

-

+
 Verifying CheckWellformed$$_0_M0.C.R ...

   [3 proof obligations]  error

 Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon5_Else

-

+
 Verifying CheckWellformed$$_1_M1.C.M ...

   [0 proof obligations]  verified

-

+
 Verifying Impl$$_1_M1.C.M ...

   [1 proof obligation]  verified

-

+
 Verifying CheckWellformed$$_1_M1.C.P ...

   [1 proof obligation]  error

 Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.

@@ -1740,10 +1759,10 @@ Execution trace:
     (0,0): anon7_Else

     (0,0): anon9_Then

     (0,0): anon6

-

+
 Verifying CheckWellformed$$_1_M1.C.Q ...

   [0 proof obligations]  verified

-

+
 Verifying CheckWellformed$$_1_M1.C.R ...

   [0 proof obligations]  verified

 

diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy
new file mode 100644
index 00000000..641b8207
--- /dev/null
+++ b/Test/dafny0/Computations.dfy
@@ -0,0 +1,152 @@
+function fact6(n: nat): nat

+{

+  fact(n+6)

+}

+

+function fact(n: nat): nat

+{

+  if (n==0) then 1 else n*fact(n-1)

+}

+ghost method compute_fact6()

+  ensures fact(6)==720;

+{

+}

+ghost method compute_fact6_plus()

+  ensures fact6(0)==720;

+{

+}

+

+datatype intlist = IntNil | IntCons(head: int, tail: intlist);

+function intsize(l: intlist): nat

+{

+  if (l.IntNil?) then 0 else 1+intsize(l.tail)

+}

+function intapp(a: intlist, b: intlist): intlist

+{

+  if (a.IntNil?) then b else IntCons(a.head, intapp(a.tail, b))

+}

+ghost method compute_intappsize()

+  ensures intsize(intapp(IntCons(1, IntCons(2, IntNil)), IntCons(3, IntCons(4, IntNil))))==4;

+{

+}

+ghost method compute_intsize4()

+  ensures intsize(IntCons(1, IntCons(2, IntCons(3, IntCons(4, IntNil))))) == 4;

+{

+}

+function cintsize(l: intlist): nat

+{

+  match l

+  case IntNil => 0

+  case IntCons(hd, tl) => 1+cintsize(tl)

+}

+function cintapp(a: intlist, b: intlist): intlist

+{

+  match a

+  case IntNil => b

+  case IntCons(hd, tl) => IntCons(hd, cintapp(tl, b))

+}

+ghost method compute_cintappsize()

+  ensures cintsize(cintapp(IntCons(1, IntCons(2, IntNil)), IntCons(3, IntCons(4, IntNil))))==4;

+{

+}

+ghost method compute_cintsize4()

+  ensures cintsize(IntCons(1, IntCons(2, IntCons(3, IntCons(4, IntNil))))) == 4;

+{

+}

+datatype list<A> = Nil | Cons(head: A, tail: list);

+function size(l: list): nat

+{

+  if (l.Nil?) then 0 else 1+size(l.tail)

+}

+function app(a: list, b: list): list

+{

+  if (a.Nil?) then b else Cons(a.head, app(a.tail, b))

+}

+ghost method compute_size4()

+  ensures size(Cons(1, Cons(2, Cons(3, Cons(4, Nil))))) == 4;

+{

+}

+ghost method compute_size4_cons()

+  ensures size(Cons(IntNil, Cons(IntNil, Cons(IntNil, Cons(IntNil, Nil))))) == 4;

+{

+}

+ghost method compute_appsize()

+  ensures size(app(Cons(1, Cons(2, Nil)), Cons(3, Cons(4, Nil))))==4;

+{

+}

+

+datatype exp = Plus(e1: exp, e2: exp) | Num(n: int) | Var(x: int);

+function interp(env: map<int,int>, e: exp): int

+  decreases e;

+{

+  if (e.Plus?) then interp(env, e.e1)+interp(env, e.e2)

+  else if (e.Num?) then e.n

+  else if (e.Var? && e.x in env) then env[e.x]

+  else 0

+}

+ghost method compute_interp1()

+  ensures interp(map[], Plus(Plus(Num(1), Num(2)), Plus(Num(3), Num(4))))==10;

+{

+}

+ghost method compute_interp2(env: map<int,int>)

+  requires 0 in env && env[0]==10;

+  ensures interp(env, Plus(Plus(Var(0), Num(1)), Num(0)))==11;

+{

+}

+ghost method compute_interp3(env: map<int,int>)

+  requires 0 in env && env[0]==10 && 1 !in env;

+  ensures interp(env, Plus(Var(0), Plus(Var(1), Var(0))))==20;

+{

+}

+function cinterp(env: map<int,int>, e: exp): int

+  decreases e;

+{

+  match e

+  case Plus(e1, e2) => cinterp(env, e1)+cinterp(env, e2)

+  case Num(n) => n

+  case Var(x) => if x in env then env[x] else 0

+}

+ghost method compute_cinterp1()

+  ensures cinterp(map[], Plus(Plus(Num(1), Num(2)), Plus(Num(3), Num(4))))==10;

+{

+}

+ghost method compute_cinterp2(env: map<int,int>)

+  requires 0 in env && env[0]==10;

+  ensures cinterp(env, Plus(Plus(Var(0), Num(1)), Num(0)))==11;

+{

+}

+ghost method compute_cinterp3(env: map<int,int>)

+  requires 0 in env && env[0]==10 && 1 !in env;

+  ensures cinterp(env, Plus(Var(0), Plus(Var(1), Var(0))))==20;

+{

+}

+

+function opt(e: exp): exp

+{

+  match e

+  case Num(n) => e

+  case Var(x) => e

+  case Plus(e1, e2) =>

+    var o1 := opt(e1);

+    if (o1.Num? && o1.n==0) then e2 else Plus(o1, e2)

+}

+ghost method opt_test()

+  ensures opt(Plus(Plus(Plus(Num(0), Num(0)), Num(0)), Num(1)))==Num(1);

+{

+}

+function copt(e: exp): exp

+{

+  match e

+  case Num(n) => e

+  case Var(x) => e

+  case Plus(e1, e2) => match e1

+    case Num(n) => if n==0 then e2 else e

+    case Var(x) => e

+    case Plus(e11, e12) =>

+      var o1 := copt(e1);

+      if (o1.Num? && o1.n==0) then e2 else Plus(o1, e2)

+}

+ghost method copt_test()

+  ensures copt(Plus(Plus(Plus(Num(0), Num(0)), Num(0)), Num(1)))==Num(1);

+{

+}

diff --git a/Test/dafny0/ComputationsNeg.dfy b/Test/dafny0/ComputationsNeg.dfy
new file mode 100644
index 00000000..72e249d8
--- /dev/null
+++ b/Test/dafny0/ComputationsNeg.dfy
@@ -0,0 +1,22 @@
+function bad(n: nat): nat

+  decreases n;

+{

+  bad(n+1)

+}

+ghost method go_bad()

+  ensures bad(0)==0;

+{

+}

+

+datatype Nat = Zero | Succ(tail: Nat)

+predicate ThProperty(step: nat, t: Nat, r: nat)

+{

+  match t

+  case Zero => true

+  case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro)

+}

+ghost method test_ThProperty()

+  ensures ThProperty(10, Succ(Zero), 0);

+{

+//  assert ThProperty(9, Zero, 0);

+}
\ No newline at end of file
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index c238b1f4..18f34345 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -26,7 +26,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy
             Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy

             RefinementModificationChecking.dfy TailCalls.dfy

             Calculations.dfy IteratorResolution.dfy Iterators.dfy

-            RankPos.dfy RankNeg.dfy) do (

+            RankPos.dfy RankNeg.dfy

+            Computations.dfy ComputationsNeg.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f