From c14d705d57c1dfcee481367bd6744feb6774dfae Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 6 Jan 2016 18:56:02 -0800
Subject: Added flying robots example to test suite

---
 Test/VerifyThis2015/Problem2.dfy    |   2 +-
 Test/dafny4/FlyingRobots.dfy        | 285 ++++++++++++++++++++++++++++++++++++
 Test/dafny4/FlyingRobots.dfy.expect |   5 +
 3 files changed, 291 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny4/FlyingRobots.dfy
 create mode 100644 Test/dafny4/FlyingRobots.dfy.expect

(limited to 'Test')

diff --git a/Test/VerifyThis2015/Problem2.dfy b/Test/VerifyThis2015/Problem2.dfy
index 86b4a019..2bb63e7b 100644
--- a/Test/VerifyThis2015/Problem2.dfy
+++ b/Test/VerifyThis2015/Problem2.dfy
@@ -114,7 +114,7 @@ method ParallelGcd(A: int, B: int) returns (gcd: int)
   var pc0, pc1 := 0, 0;  // program counter for the two processes
   var a0, b0, a1, b1;  // local variables for the two processes
   // To model fairness of scheduling, these "budget" variable give a bound on the number of times the
-  // scheduler will repeatedly schedule on process to execute its "compare a and b" test.  When a
+  // scheduler will repeatedly schedule one process to execute its "compare a and b" test.  When a
   // process executes its comparison, its budget is decreased and the budget for the other process
   // is set to some arbitrary positive amount.
   var budget0, budget1 :| budget0 > 0 && budget1 > 0;
diff --git a/Test/dafny4/FlyingRobots.dfy b/Test/dafny4/FlyingRobots.dfy
new file mode 100644
index 00000000..c80d310d
--- /dev/null
+++ b/Test/dafny4/FlyingRobots.dfy
@@ -0,0 +1,285 @@
+// RUN: %dafny /compile:3 /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// The flying robots examples from an F* tutorial.  It demonstrates how to specify
+// mutable data structures in the heap.
+
+class Cell {
+  var val:int
+  constructor (v:int)
+    modifies this
+    ensures val == v
+  {
+    val := v;
+  }
+}
+
+class Point {
+  ghost var Value: (int, int, int)
+
+  ghost var Repr: set<object>
+  predicate Valid()
+    reads this, Repr
+  {
+    this in Repr && null !in Repr &&
+    {x,y,z} <= Repr &&
+    x != y && y != z && z != x &&
+    Value == (x.val, y.val, z.val)
+  }
+  
+  var x:Cell, y:Cell, z:Cell
+
+  constructor (a:int, b:int, c:int)
+    modifies this
+    ensures Valid() && fresh(Repr - {this})
+    ensures Value == (a, b, c)
+  {
+    x := new Cell(a);
+    y := new Cell(b);
+    z := new Cell(c);
+    Repr := {this};
+    Repr := Repr + {x, y, z};
+    Value := (a, b, c);
+  }
+
+  method Mutate(a:int, b:int, c:int)
+    requires Valid()
+    modifies Repr
+    ensures Valid() && fresh(Repr - old(Repr))
+    ensures Value == (a, b, c)
+  {
+    x.val, y.val, z.val := a, b, c;
+    Value := (a, b, c);
+  }
+}
+
+class Arm {
+  ghost var Value: (int, int)
+
+  ghost var Repr: set<object>
+  predicate Valid()
+    reads this, Repr
+  {
+    this in Repr && null !in Repr &&
+    {polar, azim} <= Repr &&
+    polar != azim &&
+    Value == (polar.val, azim.val)
+  }
+
+  var polar:Cell
+  var azim:Cell
+
+  constructor (polar_in:int, azim_in:int)
+    modifies this
+    ensures Valid() && fresh(Repr - {this})
+    ensures Value == (polar_in, azim_in)
+  {
+    polar := new Cell(polar_in);
+    azim := new Cell(azim_in);
+    Repr := {this};
+    Repr := Repr + {polar, azim};
+    Value := (polar_in, azim_in);
+  }
+
+  method Mutate(polar_in:int, azim_in:int)
+    requires Valid()
+    modifies Repr
+    ensures Valid() && fresh(Repr - old(Repr))
+    ensures Value == (polar_in, azim_in)
+  {
+    polar.val, azim.val := polar_in, azim_in;
+    Value := (polar_in, azim_in);
+  }
+}
+
+class Bot {
+  ghost var Repr: set<object>
+  predicate {:opaque} Valid()
+    reads this, Repr
+    ensures Valid() ==> this in Repr && null !in Repr
+  {
+    this in Repr && null !in Repr &&
+    pos in Repr && {left, right} <= Repr &&
+    left != right &&
+    pos.Repr <= Repr && left.Repr <= Repr && right.Repr <= Repr &&
+    pos.Repr !! left.Repr !! right.Repr &&
+    pos.Valid() && left.Valid() && right.Valid()
+  }
+
+  var pos:Point
+  var left:Arm
+  var right:Arm
+
+  constructor ()
+    modifies this
+    ensures Valid() && fresh(Repr - {this})
+  {
+    pos := new Point(0, 0, 0);
+    left := new Arm(0, 0);
+    right := new Arm(0, 0);
+    Repr := {this};
+    Repr := Repr + pos.Repr + left.Repr + right.Repr;
+    reveal_Valid();
+  }
+
+  predicate flying()
+    requires (reveal_Valid(); Valid())
+    reads Repr
+  {
+    pos.z.val > 0
+  }
+  
+  predicate arms_up()
+    requires (reveal_Valid(); Valid())
+    reads Repr
+  {
+    left.polar.val == right.polar.val == 0
+  }
+
+  predicate robot_inv()
+    requires (reveal_Valid(); Valid())
+    reads Repr
+  {
+    flying() ==> arms_up()
+  }
+
+  method Fly()
+    requires Valid()
+    modifies Repr
+    ensures Valid() && fresh(Repr - old(Repr))
+    ensures robot_inv() && flying()
+  {
+    reveal_Valid();
+    left.polar.val, right.polar.val := 0, 0;
+    pos.z.val := 100;
+    right.azim.val := 17;
+    pos.Value := (pos.Value.0, pos.Value.1, 100);
+    left.Value, right.Value := (0, left.Value.1), (0, 17);
+    reveal_Valid();
+  }
+}
+
+// This method tests that Fly operates independently on disjoint robots
+method FlyRobots(b0:Bot, b1:Bot)
+  requires b0 != null && b0.Valid()
+  requires b1 != null && b1.Valid()
+  requires b0 != b1 ==> b0.Repr !! b1.Repr
+  modifies b0.Repr, b1.Repr
+  ensures b0.Valid() && fresh(b0.Repr - old(b0.Repr))
+  ensures b1.Valid() && fresh(b1.Repr - old(b1.Repr))
+  ensures b0 != b1 ==> b0.Repr !! b1.Repr
+  ensures  b0.robot_inv() && b1.robot_inv()
+  ensures  b0.flying() && b1.flying()
+{
+  b0.Fly();
+  b1.Fly();
+}
+
+// ----- robot armies ----------
+
+// The union of .Repr for the robots in "bots"
+function ArmyRepr(bots:seq<Bot>) : set<object>
+  reads set b | b in bots 
+{
+  set b,o | b in bots && b != null && o in b.Repr :: o
+}
+
+// An army is a sequence of disjoint, valid robots
+predicate ValidArmy(bots:seq<Bot>)
+  reads set b | b in bots 
+  reads ArmyRepr(bots)     
+{
+      (forall i :: 0 <= i < |bots| ==> bots[i] != null && bots[i].Valid())
+  &&  (forall i,j :: 0 <= i < j < |bots| ==> bots[i].Repr !! bots[j].Repr)
+}
+
+method FlyRobotArmy(bots:seq<Bot>)
+  requires ValidArmy(bots)
+  modifies ArmyRepr(bots)
+  ensures ValidArmy(bots) && fresh(ArmyRepr(bots) - old(ArmyRepr(bots)))
+  ensures forall b :: b in bots ==> b.Valid() && b.robot_inv() && b.flying()
+{
+  if * {
+    // fly recursively
+    FlyRobotArmy_Recursively(bots);
+  } else {
+    // fly iteratively
+    var n := 0;
+    while n < |bots|
+      invariant 0 <= n <= |bots|
+      invariant ValidArmy(bots)
+      invariant forall j :: 0 <= j < n ==> bots[j].Valid() && bots[j].robot_inv() && bots[j].flying()
+      invariant forall i :: 0 <= i < |bots| ==> fresh(bots[i].Repr - old(bots[i].Repr))
+    {
+      FlyOne(bots, n);
+      n := n + 1;
+    }
+  }
+}
+
+method FlyRobotArmy_Recursively(bots:seq<Bot>)
+  requires ValidArmy(bots)
+  modifies ArmyRepr(bots)
+  ensures ValidArmy(bots)
+  ensures forall i :: 0 <= i < |bots| ==> fresh(bots[i].Repr - old(bots[i].Repr))
+  ensures forall b :: b in bots ==> b.robot_inv() && b.flying()
+{
+  if bots != [] {
+    FlyOne(bots, 0);
+    FlyRobotArmy_Recursively(bots[1..]);
+  }
+}
+
+// This method is intended to be called in each loop iteration of FlyRobotArmy
+method FlyOne(bots:seq<Bot>, n:int)
+  requires 0 <= n < |bots|
+  requires forall j :: 0 <= j < |bots| ==> bots[j] != null && bots[j].Valid()
+  requires forall i,j :: 0 <= i < j < |bots| ==> bots[i].Repr !! bots[j].Repr
+  requires forall j :: 0 <= j < n ==>  bots[j].robot_inv() && bots[j].flying()
+  modifies bots[n].Repr
+  ensures forall j :: 0 <= j < |bots| ==> bots[j].Valid()
+  ensures fresh(bots[n].Repr - old(bots[n].Repr))
+  ensures bots[n].robot_inv() && bots[n].flying()
+  ensures forall j :: 0 <= j < |bots| && j != n ==> bots[j].Repr == old(bots[j].Repr)
+  ensures forall j :: 0 <= j < n ==> bots[j].robot_inv() && bots[j].flying()
+{
+  bots[n].Fly();
+}
+
+// This method makes sure FlyRobotArmy is callable and callable again
+method FormArmy(b0:Bot, b1:Bot, b2:Bot)
+  requires null !in {b0, b1, b2}
+  requires b0.Valid() && b1.Valid() && b2.Valid()
+  requires b0.Repr !! b1.Repr !! b2.Repr
+  modifies b0.Repr, b1.Repr, b2.Repr
+  ensures b0.Valid() && b1.Valid() && b2.Valid()
+  ensures b0.Repr !! b1.Repr !! b2.Repr
+  ensures fresh(b0.Repr + b1.Repr + b2.Repr - old(b0.Repr + b1.Repr + b2.Repr))
+{
+  var army := [b0, b1, b2];
+  ArmyRepr3(army);
+  FlyRobotArmy(army);
+  FlyRobotArmy(army);  // do it again
+  ArmyRepr3(army);
+}
+
+lemma ArmyRepr3(army:seq<Bot>)
+  requires null !in army && |army| == 3
+  ensures ArmyRepr(army) == army[0].Repr + army[1].Repr + army[2].Repr
+{
+}
+
+// ----- Make sure everything is callable ----------
+
+method Main()
+{
+  var b0 := new Bot();
+  var b1 := new Bot();
+  FlyRobots(b0, b1);
+  FlyRobots(b0, b1);
+  FlyRobots(b1, b0);
+
+  var b2 := new Bot();
+  FormArmy(b0, b1, b2);
+  FormArmy(b2, b0, b1);
+}
diff --git a/Test/dafny4/FlyingRobots.dfy.expect b/Test/dafny4/FlyingRobots.dfy.expect
new file mode 100644
index 00000000..99cdc3cb
--- /dev/null
+++ b/Test/dafny4/FlyingRobots.dfy.expect
@@ -0,0 +1,5 @@
+
+Dafny program verifier finished with 37 verified, 0 errors
+Program compiled successfully
+Running...
+
-- 
cgit v1.2.3