files from hedyindafny repo added to hedy repo in a folder (hedyorg#2942

)

semantics/Dafny/README.md

@@ -0,0 +1,11 @@
+# hedyindafny
+
+hedy1.cs is the C# file hedy1.dfy compiles to, etc.
+
+hedy1.dfy, hedy2.dfy, hedy3.dfy, hedy4.dfy and hedy5.dfy contain the semantics of Hedy level 1, 2, 3, 4 and 5 respectively, I think it is now complete and without errors. 
+
+hedy4.dfy contains the semantics of Hedy level 4. It is exactly the same as the code for level 3, except for the method substStr, this method works a little bit different here, because of syntactic changes in Hedy. The semantics does not change from level 3 to 4.
+
+oldapproachhedy.dfy contains an old approach for implementing the semantics. This might be useful if someone continues this work of implementing the semantics of Dafny in Hedy. This approach can be helpful for the next step of verifying the implementation, so that the Dafny code can be used as a reference implementation. The approach taken here is similar to: https://www.cs.cmu.edu/~mfredrik/15414/lectures/11-notes.pdf
+
+hedy1-properties.dfy and hedy1-tree.dfy contain attempts to verify the implementation of the semantics of Hedy level 1, so that the Dafny code can be used as reference implementation.

semantics/Dafny/hedy1-properties.dfy

@@ -0,0 +1,175 @@
+include "hedy1.dfy"
+
+datatype ActionType
+  = PrintT(string)
+  | GetT(string)
+  | TurnT(int)
+  | ForwardT(int)
+  | DrawT
+  | ExecutionError(string)
+  | SampleError
+
+type Sample = seq<string>
+
+class Action {
+  var act : ActionType;
+
+  constructor PrintA(output : string)
+    ensures act == PrintT(output)
+  {
+    act := PrintT(output);
+  }
+
+  constructor GetA(input : string) {
+    act := GetT(input);
+  }
+
+  // etc. (one constructor per action
+
+  constructor SampleErrorA() {
+    act := SampleError;
+  }
+
+}
+
+class SampleEnv1 extends Env1 {
+  var samples: Sample;
+  var execution : seq<Action>;
+
+  constructor(inputs : seq<string>){
+    samples := inputs;
+  }
+
+  method Print(output : string)
+    modifies this
+    ensures |execution| > 0
+    ensures execution[0].act == PrintT(output)
+  {
+    var a := new Action.PrintA(output);
+    execution := [a] + execution;
+    assert execution[0].act == PrintT(output);
+  }
+
+  method Ask(question : string) returns (input : string) modifies this {
+    var a := new Action.PrintA(question);
+    var b;
+    if(|samples| > 0){
+      input := samples[0];
+      samples := samples[1..];
+      b := new Action.GetA(input);
+    }
+    else {
+      b := new Action.SampleErrorA();
+    }
+    execution := [b, a] + execution;
+  }
+
+  method Error(exception: string) modifies this {
+  }
+
+  method Turn(angle: int) modifies this {
+  }
+
+  method Forward(step: int) modifies this {
+  }
+
+  method Draw() modifies this {
+  }
+}
+
+method Interpret(e1 : SampleEnv1, e2 : Env1)
+  modifies e2
+  requires e1 != e2 // needed to make sure that we do not interpret e1 in itself
+{
+  var i := |e1.execution|;
+  var j;
+  while 0 < i
+    decreases i
+    invariant 0 <= i
+    invariant i <= |e1.execution|
+  {
+    // for i := |e1.execution| downto 0 {
+    j := i - 1;
+    i := i - 1;
+    match e1.execution[j].act {
+      case PrintT(x) => e2.Print(x);
+      case _ => return;
+    }
+  }
+}
+
+// Checks whether the last action executed in e was a print with output s
+predicate WasPrint(s : string, e : SampleEnv1)
+  reads e, e.execution
+  requires |e.execution| > 0
+{
+  e.execution[0].act == PrintT(s)
+}
+
+method bigstep_level1_samples(c: Com1, e: SampleEnv1)
+  modifies e
+  ensures forall x :: c == Print(x) ==> |e.execution| > 0 && WasPrint(x, e)
+{
+    match(c){
+        case Print(x) =>
+          e.Print(x);
+          assert WasPrint(x, e);
+        case Ask(x) =>
+	          var answer := e.Ask(x);
+            e.store := Just(answer);
+        case Echo(x) =>
+            match(e.store) {
+                case Nothing => e.Error("echo without ask");
+                case Just(s) => e.Print(x+s);
+            }
+        case Turn(x) =>
+            if (e.turtle_exists == false) {
+                e.Draw();
+                e.turtle_exists := true;
+            }
+            e.Turn(bigstep_D_level1(x)); 
+        case Forward(x) =>
+            if (e.turtle_exists == false) {
+                e.Draw();
+                e.turtle_exists := true;
+            }
+            e.Forward(bigstep_P_level1(x));
+        case Seq(c1, c2) => {
+            bigstep_level1(c1, e);
+            bigstep_level1(c2, e);
+        }
+    }
+}
+
+twostate predicate SampleDequed(e : SampleEnv1)
+  reads e
+  requires old(|e.samples|) > 0
+{
+  old(e.samples[1..]) == e.samples
+}
+
+
+// https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-old-expression
+
+method PrintCorrect(o : string, e : SampleEnv1)
+  modifies e
+  ensures |e.execution| > 0
+  ensures e.execution[0].act == PrintT(o)
+
+{
+  var c := Print(o);
+  e.Print(o);
+  // bigstep_level1(c, e);
+}
+
+/*
+method AskCorrect(q : string, e : SampleEnv1)
+  modifies e
+  requires |e.samples| > 0
+{
+  var c := Ask(q);
+  bigstep_level1(c, e);
+  label Executed:
+    assert SampleDequed@Executed(e);
+}
+ */

semantics/Dafny/hedy1-tree.dfy

@@ -0,0 +1,178 @@
+include "hedy1.dfy"
+
+// https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml250.pdf
+//  https://github.com/dafny-lang/dafny/blob/master/Test/dafny4/NipkowKlein-chapter7.dfy
+
+  // Record type with one field for the store and one to indicate whether the turtle
+// has already been drawn.
+datatype State = State(store : Maybe<string>, drawn : bool)
+
+// Type that represents interactions with the environment as tree
+datatype Prog<A>
+  = Return (pure : A)
+  | PrintP(output : string, Prog<A>)
+  | AskP(question : string, input : string -> Prog<A>)
+  | TurnP(angle : int, Prog<A>)
+  | ForwardP(step : int, Prog<A>)
+  | DrawP(Prog<A>)
+  | Error(exception : string)
+
+
+// We give the big-step semantics as two mutually recursively defined inductive
+// relations. big_step_seq is used to sequentially compose the semantics of two
+// commands.
+
+least predicate big_step_seq(c : Com1, p : Prog<State>, q : Prog<State>) {
+  match p {
+    case Return(s) => big_step(c, s, q)
+    case PrintP(o, p') => exists q' :: q == PrintP(o, q') && big_step_seq(c, p', q')
+    case AskP(o, f) => exists g :: q == AskP(o, g) &&  forall i :: big_step_seq(c, f(i), g(i))
+    case TurnP(a, p') => false
+    case ForwardP(x, p') => false
+    case DrawP(p') => exists q' :: q == DrawP(q') && big_step_seq(c, p', q')
+    case Error(e) => q == Error(e)
+  }
+}
+
+
+least predicate big_step(c : Com1, s : State, p : Prog<State>) {
+  match c {
+    case Print(o) => p == PrintP(o, Return(s))
+    case Ask(o) =>
+      p == AskP(o, i => Return(s.(store := Just(i))))
+    case Echo(o) =>
+      match s.store {
+        case Nothing => p == Error("echo without ask")
+        case Just(x) => p == PrintP(o + x, Return(s))
+      }
+    case Turn(x) =>
+      p == TurnP(bigstep_D_level1(x), Return(s))
+    case Forward(x) => p == ForwardP(bigstep_P_level1(x), Return(s))
+    case Seq(c1, c2) =>
+      exists p1 :: big_step(c1, s, p1) && big_step_seq(c2, p1, p)
+  }
+}
+
+lemma PrintCorrect(o : string, s : State)
+  ensures forall p :: big_step(Print(o), s, p) ==> p == PrintP(o, Return(s));
+{ }
+
+predicate readStore(p : Prog<State>, v : string) {
+  match p {
+    case Return(s) =>
+      match s.store {
+        case Nothing => false
+        case Just (x) => x == v
+      }
+     case _ => false
+  }
+}
+
+lemma AskCorrect(o : string, s : State, p : Prog<State>)
+  requires big_step(Ask(o), s, p)
+  ensures exists f :: p == AskP(o, f) && forall i :: readStore(f(i), i)
+{ }
+
+lemma big_step_seq_return(c : Com1, s : State)
+  ensures forall p :: big_step_seq(c, Return(s), p) ==> big_step(c, s, p)
+{ }
+
+lemma PrintSeq(c : Com1, o : string, s : State, p : Prog<State>)
+  requires big_step(Seq(Print(o), c), s, p)
+  ensures exists q :: p == PrintP(o, q) && big_step(c, s, q)
+{
+  big_step_seq_return(c, s);
+}
+
+lemma SimpleSeq(o : string, s : State, p : Prog<State>)
+  requires big_step(Seq(Print(o), Ask(o)), s, p)
+{
+  PrintSeq(Ask(o), o, s, p);
+  assert exists q :: p == PrintP(o, q) && big_step(Ask(o), s, q);
+}
+
+// lemma big_step_deterministic_aux(k: ORDINAL, k': ORDINAL, c: Com1, s: State, p: Prog<State>, p': Prog<State>)
+//   requires big_step#[k](c, s, p) && big_step#[k'](c, s, p')
+//   ensures p == p'
+// {}
+
+
+least predicate wfTree<T> (p : Prog<T>){
+  match p {
+    case Return(b) => true
+    case PrintP(_, p') => wfTree(p')
+    case AskP(_, g) => forall x :: wfTree(g(x))
+    case TurnP(_, p') => wfTree(p')
+    case ForwardP(_, p') => wfTree(p')
+    case DrawP(p') => wfTree(p')
+    case Error(_) => true
+  }
+}
+
+// // Not executable because it tests for limit ordinals
+// method run_aux(ghost k :ORDINAL, p : Prog<State>, e : Env1)
+//   requires wfTree#[k](p)
+//   decreases k
+// {
+//   if(k.IsLimit) {
+//     ghost var m :| m < k && wfTree#[m](p);
+//     run_aux(m, p, e);
+//   }
+//   else {
+//     match p {
+//       case Return(s) => return;
+//       case PrintP(o, q) =>
+//         e.Print(o);
+//         run_aux(k-1, q, e);
+//       case AskP(o, f) =>
+//         var i := e.Ask(o);
+//         run_aux(k-1, f(i), e);
+//       case TurnP(a, p') =>
+//         e.Turn(a);
+//         run_aux(k-1, p', e);
+//       case ForwardP(x, p') =>
+//         e.Forward(x);
+//         run_aux(k-1, p', e);
+//       case DrawP(p') =>
+//         e.Draw();
+//         run_aux(k-1, p', e);
+//       case Error(x) =>
+//         e.Error(x);
+//     }
+//   }
+// }
+
+// method runP(p : Prog<State>, e : Env1)
+//   requires wfTree(p)
+// {
+//   ghost var k :| wfTree#[k](p);
+//   run_aux(k, p, e);
+// }
+
+
+// Unsafe declaration but Dafny does not understand that this method
+// is terminating because of the higher-order argument of Get.
+method {: verify false} run(p : Prog<State>, e : Env1)
+  modifies e
+{
+  match p {
+    case Return(s) => return;
+    case PrintP(o, q) =>
+      e.Print(o);
+      run(q, e);
+    case AskP(o, f) =>
+      var i := e.Ask(o);
+      run(f(i), e);
+    case TurnP(a, p') =>
+      e.Turn(a);
+      run(p', e);
+    case ForwardP(x, p') =>
+      e.Forward(x);
+      run(p', e);
+    case DrawP(p') =>
+      e.Draw();
+      run(p', e);
+    case Error(x) =>
+      e.Error(x);
+  }
+}