Added to the test suite a Dafny version of Basics.v from the "Software Foundations" book (Pierce et al.)

1 files changed, 504 insertions, 0 deletions

diff --git a/Test/dafny4/SoftwareFoundations-Basics.dfy b/Test/dafny4/SoftwareFoundations-Basics.dfy
new file mode 100644
index 00000000..25adce4c
--- /dev/null
+++ b/Test/dafny4/SoftwareFoundations-Basics.dfy
@@ -0,0 +1,504 @@
+// Basics.v done in Dafny

+

+// Enumerated Types

+

+// Days of the Week

+

+datatype day =

+    monday

+  | tuesday

+  | wednesday

+  | thursday

+  | friday

+  | saturday

+  | sunday

+

+// See method test_next_weekday() below for an explanation of why this function

+// is declared a non-ghost (by "function method").

+function method next_weekday (d:day) : day

+{

+  match d

+  case monday    => tuesday

+  case tuesday   => wednesday

+  case wednesday => thursday

+  case thursday  => friday

+  case friday    => monday

+  case saturday  => monday

+  case sunday    => monday

+}

+

+method test_next_weekday()

+{

+  assert next_weekday(friday) == monday;

+  assert next_weekday(next_weekday(saturday)) == tuesday;

+  // Note, if you're not sure what some expression will compute, you

+  // can assert that it equals some arbitrary value of the correct type.

+  // For example:

+  var d := next_weekday(next_weekday(tuesday));

+  assert d == friday;   // error (use the Verification Debugger to view the correct value)

+  // You will then get an error message (unless you were lucky and

+  // happened to pick the right value).  If you're running the Dafny IDE

+  // in Visual Studio, you can then click on the red circle that signals

+  // the error.  This will bring up the Verification Debugger, where you

+  // can inspect the value of d.  Then try changing the assertion in

+  // the program to assert d to equal it.  In some cases, depending on

+  // how many Dafny knows about the value you're trying to get it to

+  // compute, you may need to build a disjunction of values for d in the

+  // assertion.

+  // Or, just write a program that prints the value, compile the program,

+  // and run it -- Dafny is a programming language after all.  (Note, by

+  // default, functions in Dafny of "ghost", which means they don't turn

+  // into compiled code.  If you want to compile code for next_weekday, so

+  // that you can use it in a print statement, change "function" to

+  // "function method" in the declaration of next_weekday.)  To try this

+  // out on rise4fun.com/dafny:  (0) comment out (or fix!) the assert above

+  // so that the program will verify, (1) fill in a body of the uninterpreted

+  // function f on line 412 below (any body will do; for example, uncomment

+  // line 416), and (2) change the name of this method to Main().

+  print next_weekday(wednesday);

+}

+

+

+

+// Booleans

+

+// Booleans are built into Dafny as primitives.  Nevertheless, here is

+// another definition, using an enumeration.

+

+datatype Bool = True | False

+

+function negb (b:Bool) : Bool

+{

+  match b

+  case True => False

+  case False => True

+}

+

+function andb (b1:Bool, b2:Bool) : Bool

+{

+  match b1

+  case True => b2 

+  case False => False

+}

+

+function orb (b1:Bool, b2:Bool) : Bool

+{

+  match b1

+  case True => True

+  case False => b2

+}

+

+method test_orb()

+{

+  assert orb(True, False) == True;

+  assert orb(False, False) == False;

+  assert orb(False, True) == True;

+  assert orb(True, True) == True;

+}

+

+// Exercise: 1 star (nandb)

+

+function nandb (b1:Bool, b2:Bool) : Bool

+{

+  negb(andb(b1, b2))

+}

+

+method test_nandb()

+{

+  assert nandb(True, False) == True;

+  assert nandb(False, False) == True;

+  assert nandb(False, True) == True;

+  assert nandb(True, True) == False;

+}

+

+// Exercise: 1 star (andb3)

+

+function andb3 (b1:Bool, b2:Bool, b3:Bool) : Bool

+{

+  andb(andb(b1, b2), b3)

+}

+

+method test_andb3()

+{

+  assert andb3(True, True, True) == True;

+  assert andb3(False, True, True) == False;

+  assert andb3(True, False, True) == False;

+  assert andb3(True, True, False) == False;

+}

+

+// Function Types

+

+// Numbers

+

+datatype Nat =

+    O

+  | S(Nat)

+

+// Note, in order to refer to the function pred as Playground1.pred outside the current

+// module, the function must be declared "static".  This will change in a near-future

+// release of Dafny.

+static function pred (n : Nat) : Nat

+{

+  match n

+  case O => O

+  case S(n') => n'

+}

+

+function minustwo (n : Nat) : Nat

+{

+  match n

+  case O => O

+  case S(nn) =>

+    // Note, Dafny currently does not support nested patterns in match expressions, but

+    // this will change soon.

+    match nn

+    case O => O

+    case S(n') => n'

+}

+

+function evenb (n:Nat) : Bool

+{

+  match n

+  case O       => True

+  case S(nn) =>

+    match nn

+    case O     => False

+    case S(n') => evenb(n')

+}

+

+function oddb (n:Nat) : Bool

+{

+  negb(evenb(n))

+}

+

+method test_oddb()

+{

+  assert oddb(S(O)) == True;

+  assert oddb(S(S(S(S(O))))) == False;

+}

+

+function plus (n : Nat, m : Nat) : Nat

+{

+  match n

+  case O => m

+  case S(n') => S(plus(n', m))

+}

+

+method test_plus()

+{

+  assert plus(S(S(S(O))), S(S(O))) == S(S(S(S(S(O)))));

+}

+

+function mult (n: Nat, m: Nat) : Nat

+{

+  match n

+  case O => O

+  case S(n') => plus(m, mult(n', m))

+}

+

+method test_mult()

+{

+  var n3 := S(S(S(O)));

+  var n9 := S(S(S(S(S(S(S(S(S(O)))))))));

+  assert mult(n3, n3) == n9;

+}

+

+function minus (n: Nat, m: Nat) : Nat

+{

+  match n

+  case O => O

+  case S(n') =>

+    match m

+    case O => n

+    case S(m') => minus(n', m')

+}

+

+function exp (base: Nat, power: Nat) : Nat

+{

+  match power

+  case O => S(O)

+  case S(p) => mult(base, exp(base, p))

+}

+

+// Exercise: 1 star (factorial)

+

+function factorial(n: Nat): Nat

+{

+  match n

+  case O => S(O)

+  case S(n') => mult(n, factorial(n'))

+}

+

+method test_factorial1()

+{

+  var n2 := S(S(O));

+  var n3 := S(n2);

+  var n5 := S(S(n3));

+  var n6 := S(n5);

+  assert factorial(n3) == n6;

+

+  var n10 := S(S(S(S(n6))));

+  var n12 := S(S(n10));

+

+  // proving that 5! == 10*12 takes some effort, because the computation fuel runs out

+  calc {

+    factorial(n5);

+    { mult_lemma(n2, n6); }

+    mult(n5, plus(plus(n6, n6), plus(plus(n6, n6), O)));

+    { mult_lemma(n5, plus(n6, n6)); }

+    mult(n10, n12);

+  }

+}

+

+// This lemma expresses:  m*(2*n) == (2*m)*n

+lemma mult_lemma(m: Nat, n: Nat)

+  ensures mult(m, plus(n, n)) == mult(plus(m, m), n);

+{

+  match m {

+    case O =>

+    case S(m') =>

+      calc {

+        mult(m, plus(n, n));

+        plus(plus(n, n), mult(m', plus(n, n)));

+        // induction hypothesis

+        plus(plus(n, n), mult(plus(m', m'), n));

+        { assert forall a,b,c :: plus(plus(a, b), c) == plus(a, plus(b, c)); }

+        plus(n, plus(n, mult(plus(m', m'), n)));

+        mult(S(S(plus(m', m'))), n);

+        mult(S(plus(S(m'), m')), n);

+        { assert forall a,b :: S(plus(a, b)) == plus(a, S(b)); }

+        mult(plus(S(m'), S(m')), n);

+      }

+  }

+}

+

+function beq_nat (n: Nat, m: Nat) : Bool

+{

+  match n

+  case O => (

+         match m

+         case O => True

+         case S(m') => False

+         )

+  case S(n') =>

+         match m

+         case O => False

+         case S(m') => beq_nat(n', m')

+}

+

+function ble_nat (n: Nat, m: Nat) : Bool

+{

+  match n

+  case O => True

+  case S(n') =>

+      match m

+      case O => False

+      case S(m') => ble_nat(n', m')

+}

+

+method test_ble_nat1()

+{

+  var n2 := S(S(O));

+  var n4 := S(S(n2));

+  assert ble_nat(n2, n2) == True;

+  assert ble_nat(n2, n4) == True;

+  assert ble_nat(n4, n2) == False;

+}

+

+// Exercise: 2 stars (blt_nat)

+

+function blt_nat (n: Nat, m: Nat) : Bool

+{

+  andb(ble_nat(n, m), negb(beq_nat(n, m)))

+}

+

+method test_blt_nat1()

+{

+  var n2 := S(S(O));

+  var n4 := S(S(n2));

+  assert blt_nat(n2, n2) == False;

+  assert blt_nat(n2, n4) == True;

+  assert blt_nat(n4, n2) == False;

+}

+

+// Proof by Simplification

+

+lemma plus_O_n (n: Nat)

+  ensures plus(O, n) == n;

+{

+}

+

+lemma plus_1_l (n: Nat)

+  ensures plus(S(O), n) == S(n);

+{

+}

+

+lemma mult_0_l (n: Nat)

+  ensures mult(O, n) == O;

+{

+}

+

+// Proof by Rewriting

+

+lemma plus_id_example (n: Nat, m: Nat)

+  ensures n == m ==> plus(n, n) == plus(m, m);

+{

+}

+

+// Exercise: 1 star (plus_id_exercise)

+

+lemma plus_id_exercise (n: Nat, m: Nat, o: Nat)

+  ensures n == m ==> m == o ==> plus(n, m) == plus(m, o);

+{

+}

+

+lemma mult_0_plus (n: Nat, m: Nat)

+  ensures mult(plus(O, n), m) == mult(n, m);

+{

+}

+

+// Exercise: 2 stars (mult_S_1)

+

+lemma mult_S_1 (n: Nat, m: Nat)

+  ensures m == S(n) ==> mult(m, plus(S(O), n)) == mult(m, m);

+{

+}

+

+

+// Proof by Case Analysis

+

+lemma plus_1_neq_0_firsttry (n: Nat)

+  ensures beq_nat(plus(n, S(O)), O) == False;

+{

+}

+

+lemma plus_1_neq_0 (n: Nat)

+  ensures beq_nat(plus(n, S(O)), O) == False;

+{

+}

+

+lemma negb_involutive (b: Bool)

+  ensures negb(negb(b)) == b;

+{

+}

+

+// Exercise: 1 star (zero_nbeq_plus_1)

+

+lemma zero_nbeq_plus_1 (n: Nat)

+  ensures beq_nat(O, plus(n, S(O))) == False;

+{

+}

+

+// More Exercises

+

+// Exercise: 2 stars (boolean functions)

+

+// Since Dafny currently does not allow functions as parameters, we instead declare

+// a global function f for use in the following lemmas.  Since f is given no body,

+// it will be treated as an uninterpreted function.

+function f(x: Bool): Bool

+// Note:  If you want to compile and run the program, as suggested above in method

+// test_next_weekday, then you must supply some body for f.  Here is one way to do

+// that:

+//      { x }

+

+lemma identity_fn_applied_twice(b: Bool)

+  requires forall x :: f(x) == x;

+  ensures f(f(b)) == b;

+{

+}

+  

+    

+lemma negation_fn_applied_twice(b: Bool)

+  requires forall x :: f(x) == negb(x);

+  ensures f(f(b)) == b;

+{

+}

+

+// Exercise: 2 stars (andb_eq_orb)

+

+lemma andb_true (b : Bool)

+  ensures andb(True, b) == b;

+{

+}

+

+lemma orb_false (b : Bool)

+  ensures orb(False, b) == b;

+{

+}

+

+lemma andb_eq_orb (b: Bool, c: Bool)

+  ensures andb(b, c) == orb(b, c) ==> b == c;

+{

+}

+

+// Exercise: 3 stars (binary)

+

+datatype bin = Zero | Twice(bin) | TwicePlusOne(bin)

+

+function increment(b: bin): bin

+{

+  match b

+  case Zero => TwicePlusOne(Zero)

+  case Twice(b') => TwicePlusOne(b')

+  case TwicePlusOne(b') => Twice(increment(b'))

+}

+

+function BinToUnary(b: bin): Nat

+{

+  match b

+  case Zero => O

+  case Twice(b') =>

+    var t := BinToUnary(b');

+    plus(t, t)

+  case TwicePlusOne(b') =>

+    var t := BinToUnary(b');

+    plus(t, plus(t, S(O)))

+}

+

+method test_bin()

+{

+  var n6 := S(S(S(S(S(S(O))))));

+  var n13 := S(S(S(S(S(S(S(n6)))))));

+  assert BinToUnary(Twice(TwicePlusOne(TwicePlusOne(Zero)))) == n6;

+  assert BinToUnary(TwicePlusOne(Twice(TwicePlusOne(TwicePlusOne(Zero))))) == n13;

+}

+

+method test_increment()

+{

+  var b13 := TwicePlusOne(Twice(TwicePlusOne(TwicePlusOne(Zero))));

+  var n13 := S(S(S(S(S(S(S(S(S(S(S(S(S(O)))))))))))));

+  var n14 := S(n13);

+

+  assert increment(Twice(TwicePlusOne(TwicePlusOne(Zero)))) == TwicePlusOne(TwicePlusOne(TwicePlusOne(Zero)));

+  assert increment(b13) == Twice(TwicePlusOne(TwicePlusOne(TwicePlusOne(Zero))));

+

+  assert BinToUnary(increment(b13)) == plus(BinToUnary(b13), S(O));

+}

+

+// Optional Material

+

+// [Fixpoint]s and Structural Recursion

+

+function plus' (n : Nat, m : Nat) : Nat

+{

+  match n

+  case O => m

+  case S(n') => S(plus'(n', m))

+}

+

+// Exercise: 2 stars, optional (decreasing)

+

+function decreasingOnTwo (n: Nat, m: Nat, p: Nat) : Nat

+{

+  match p

+  case O => (

+      match n

+      case O     => O

+      case S(n') => decreasingOnTwo(n', m, S(O))

+      )

+  case S(_) =>

+      match m

+      case O     => S(O)

+      case S(m') => decreasingOnTwo(n, m', O)

+}