Added to the test suite a Dafny encoding of Chapter 3 from the Nipkow and Klein book on semantics

2 files changed, 284 insertions, 0 deletions

diff --git a/Test/dafny4/NipkowKlein-chapter3.dfy b/Test/dafny4/NipkowKlein-chapter3.dfy
new file mode 100644
index 00000000..df56a3b3
--- /dev/null
+++ b/Test/dafny4/NipkowKlein-chapter3.dfy
@@ -0,0 +1,282 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file is a Dafny encoding of chapter 3 from "Concrete Semantics: With Isabelle/HOL" by

+// Tobias Nipkow and Gerwin Klein.

+

+// ----- lists -----

+

+datatype List<T> = Nil | Cons(head: T, tail: List<T>)

+

+function append(xs: List, ys: List): List

+{

+  match xs

+  case Nil => ys

+  case Cons(x, tail) => Cons(x, append(tail, ys))

+}

+

+// ----- arithmetic expressions -----

+

+type vname = string  // variable names

+datatype aexp = N(n: int) | V(x: vname) | Plus(0: aexp, 1: aexp)  // arithmetic expressions

+

+type val = int

+type state = vname -> val

+// In Dafny, functions can in general read the heap (which is not interesting to these examples--in fact, for

+// the examples in this file, the fact that functions can read the state is just a distraction, so you can

+// just ignore all the lines "reads s.reads" if you prefer) and may have preconditions (that is, the function

+// may have some domain that is not specific than what its type says).

+// The following predicate holds for a given s if s can be applied to any vname

+predicate Total(s: state)

+  reads s.reads  // this says that Total(s) can read anything that s can (on any input)

+{

+  // the following line is the conjunction, over all x, of the precondition of the call s(x)

+  forall x :: s.requires(x)

+}

+

+function aval(a: aexp, s: state): val

+  reads s.reads

+  requires Total(s)

+{

+  match a

+  case N(n) => n

+  case V(x) => s(x)

+  case Plus(a0, a1) => aval(a0,s ) + aval(a1, s)

+}

+

+lemma Example0()

+{

+  var y := aval(Plus(N(3), V("x")), x => 0);

+  // The following line confirms that y is 3.  If you don't know what y is, you can use the

+  // verification debugger to figure it out, like this:  Put any value in the assert (for example,

+  // "assert y == 0;".  If you're lucky and picked the right value, the verifier will prove the

+  // assertion for you.  If the verifier says it's unable to prove it, then click on the error

+  // (in the Dafny IDE), which brings up the verification debugger.  There, inspect the value

+  // of y.  This is probably the right value, but due to incompleteness in the verifier, it

+  // could happen that the value you see is some value that verifier wasn't able to properly

+  // exclude.  Therefore, it's best to now take the value you see in the verification debugger,

+  // say K, and put that into the assert ("assert y == K;"), to have the verifier confirm that

+  // K really is the answer.

+  assert y == 3;

+}

+

+// ----- constant folding -----

+

+function asimp_const(a: aexp): aexp

+{

+  match a

+  case N(n) => a

+  case V(x) => a

+  case Plus(a0, a1) =>

+    var as0, as1 := asimp_const(a0), asimp_const(a1);

+    if as0.N? && as1.N? then

+      N(as0.n + as1.n)

+    else

+      Plus(as0, as1)

+}

+

+lemma AsimpConst(a: aexp, s: state)

+  requires Total(s)

+  ensures aval(asimp_const(a), s) == aval(a, s)

+{

+  // by induction

+  forall a' | a' < a {

+    AsimpConst(a', s);  // this invokes the induction hypothesis for every a' that is structurally smaller than a

+  }

+/*  Here is an alternative proof.  In the first two cases, the proof is trivial.  The Plus case uses two invocations

+    of the induction hypothesis.

+  match a

+  case N(n) =>

+  case V(x) =>

+  case Plus(a0, a1) =>

+    AsimpConst(a0, s);

+    AsimpConst(a1, s);

+*/

+}

+

+// more constant folding

+

+function plus(a0: aexp, a1: aexp): aexp

+{

+  if a0.N? && a1.N? then

+    N(a0.n + a1.n)

+  else if a0.N? then

+    if a0.n == 0 then a1 else Plus(a0, a1)

+  else if a1.N? then

+    if a1.n == 0 then a0 else Plus(a0, a1)

+  else

+    Plus(a0, a1)

+}

+

+lemma AvalPlus(a0: aexp, a1: aexp, s: state)

+  requires Total(s)

+  ensures aval(plus(a0, a1), s) == aval(a0, s) + aval(a1, s)

+{

+  // this proof is done automatically

+}

+

+function asimp(a: aexp): aexp

+{

+  match a

+  case N(n) => a

+  case V(x) => a

+  case Plus(a0, a1) => plus(asimp(a0), asimp(a1))

+}

+

+lemma AsimpCorrect(a: aexp, s: state)

+  requires Total(s)

+  ensures aval(asimp(a), s) == aval(a, s)

+{

+  // call the induction hypothesis on every value a' that is structurally smaller than a

+  forall a' | a' < a { AsimpCorrect(a', s); }

+}

+

+// ----- boolean expressions -----

+

+datatype bexp = Bc(v: bool) | Not(op: bexp) | And(0: bexp, 1: bexp) | Less(a0: aexp, a1: aexp)

+

+function bval(b: bexp, s: state): bool

+  reads s.reads

+  requires Total(s)

+{

+  match b

+  case Bc(v) => v

+  case Not(b) => !bval(b, s)

+  case And(b0, b1) => bval(b0, s) && bval(b1, s)

+  case Less(a0, a1) => aval(a0, s) < aval(a1, s)

+}

+

+// constant folding for booleans

+

+function not(b: bexp): bexp

+{

+  match b

+  case Bc(b0) => Bc(!b0)

+  case Not(b0) => b0  // this case is not in the Nipkow and Klein book, but it seems a nice one to include

+  case And(_, _) => Not(b)

+  case Less(_, _) => Not(b)

+}

+

+function and(b0: bexp, b1: bexp): bexp

+{

+  if b0.Bc? then

+    if b0.v then b1 else b0

+  else if b1.Bc? then

+    if b1.v then b0 else b1

+  else

+    And(b0, b1)

+}

+

+function less(a0: aexp, a1: aexp): bexp

+{

+  if a0.N? && a1.N? then

+    Bc(a0.n < a1.n)

+  else

+    Less(a0, a1)

+}

+

+function bsimp(b: bexp): bexp

+{

+  match b

+  case Bc(v) => b

+  case Not(b0) => not(bsimp(b0))

+  case And(b0, b1) => and(bsimp(b0), bsimp(b1))

+  case Less(a0, a1) => less(asimp(a0), asimp(a1))

+}

+

+lemma BsimpCorrect(b: bexp, s: state)

+  requires Total(s)

+  ensures bval(bsimp(b), s) == bval(b, s)

+{

+/*  Here is one proof, which uses the induction hypothesis any anything smaller than b and also invokes

+    the lemma AsimpCorrect on anything smaller than b.

+  forall b' | b' < b { BsimpCorrect(b', s); } 

+  forall a' | a' < b { AsimpCorrect(a', s); }

+*/

+  // Here is another proof, which makes explicit the uses of the induction hypothesis and the other lemma.

+  match b

+  case Bc(v) =>

+  case Not(b0) =>

+    BsimpCorrect(b0, s);

+  case And(b0, b1) =>

+    BsimpCorrect(b0, s); BsimpCorrect(b1, s);

+  case Less(a0, a1) =>

+    AsimpCorrect(a0, s); AsimpCorrect(a1, s);

+}

+

+// ----- stack machine -----

+

+datatype instr = LOADI(val) | LOAD(vname) | ADD

+

+type stack = List<val>

+

+function exec1(i: instr, s: state, stk: stack): stack

+  reads s.reads

+  requires Total(s)

+{

+  match i

+  case LOADI(n) => Cons(n, stk)

+  case LOAD(x) => Cons(s(x), stk)

+  case ADD =>

+    if stk.Cons? && stk.tail.Cons? then

+      var Cons(a1, Cons(a0, tail)) := stk;

+      Cons(a0 + a1, tail)

+    else  // stack underflow

+      Nil  // an alternative would be to return Cons(n, Nil) for an arbitrary value n--that is what Nipkow and Klein do

+}

+

+function exec(ii: List<instr>, s: state, stk: stack): stack

+  reads s.reads

+  requires Total(s)

+{

+  match ii

+  case Nil => stk

+  case Cons(i, rest) => exec(rest, s, exec1(i, s, stk))

+}

+

+// ----- compilation -----

+

+function comp(a: aexp): List<instr>

+{

+  match a

+  case N(n) => Cons(LOADI(n), Nil)

+  case V(x) => Cons(LOAD(x), Nil)

+  case Plus(a0, a1) => append(append(comp(a0), comp(a1)), Cons(ADD, Nil))

+}

+

+lemma CorrectCompilation(a: aexp, s: state, stk: stack)

+  requires Total(s)

+  ensures exec(comp(a), s, stk) == Cons(aval(a, s), stk)

+{

+  match a

+  case N(n) =>

+  case V(x) =>

+  case Plus(a0, a1) =>

+    // This proof spells out the proof as a series of equality-preserving steps.  Each

+    // expression in the calculation is terminated by a semi-colon.  In some cases, a hint

+    // for the step is needed.  Such hints are given in curly braces.

+    calc {

+      exec(comp(a), s, stk);

+      // definition of comp on Plus

+      exec(append(append(comp(a0), comp(a1)), Cons(ADD, Nil)), s, stk);

+      { ExecAppend(append(comp(a0), comp(a1)), Cons(ADD, Nil), s, stk); }

+      exec(Cons(ADD, Nil), s, exec(append(comp(a0), comp(a1)), s, stk));

+      { ExecAppend(comp(a0), comp(a1), s, stk); }

+      exec(Cons(ADD, Nil), s, exec(comp(a1), s, exec(comp(a0), s, stk)));

+      { CorrectCompilation(a0, s, stk); }

+      exec(Cons(ADD, Nil), s, exec(comp(a1), s, Cons(aval(a0, s), stk)));

+      { CorrectCompilation(a1, s, Cons(aval(a0, s), stk)); }

+      exec(Cons(ADD, Nil), s, Cons(aval(a1, s), Cons(aval(a0, s), stk)));

+      // definition of comp on ADD

+      Cons(aval(a1, s) + aval(a0, s), stk);

+      // definition of aval on Plus

+      Cons(aval(a, s), stk);

+    }

+}

+

+lemma ExecAppend(ii0: List<instr>, ii1: List<instr>, s: state, stk: stack)

+  requires Total(s)

+  ensures exec(append(ii0, ii1), s, stk) == exec(ii1, s, exec(ii0, s, stk))

+{

+  // the proof (which is by induction) is done automatically

+}

diff --git a/Test/dafny4/NipkowKlein-chapter3.dfy.expect b/Test/dafny4/NipkowKlein-chapter3.dfy.expect
new file mode 100644
index 00000000..ab18d98e
--- /dev/null
+++ b/Test/dafny4/NipkowKlein-chapter3.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 28 verified, 0 errors