From a7f52e2b468f1eea6a502127508c09f030bdfe03 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Tue, 5 Oct 2021 14:26:55 -0700
Subject: [PATCH 1/2] Add Validatable trait

---
 src/Frames.dfy        | 42 ++++++++++++++++++++++++++++++++++++++++++
 src/Frames.dfy.expect |  2 ++
 2 files changed, 44 insertions(+)
 create mode 100644 src/Frames.dfy
 create mode 100644 src/Frames.dfy.expect

diff --git a/src/Frames.dfy b/src/Frames.dfy
new file mode 100644
index 00000000..bafed7ca
--- /dev/null
+++ b/src/Frames.dfy
@@ -0,0 +1,42 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT 
+*******************************************************************************/
+
+module Frames {
+
+  // A trait for objects with a Valid() predicate. Necessary in order to
+  // generalize some proofs, but also useful for reducing the boilerplate
+  // that most such objects need to include.
+  trait {:termination false} Validatable {
+    // Ghost state tracking the common set of objects most
+    // methods need to read.
+    ghost var Repr: set<object>
+
+    predicate Valid()
+      reads this, Repr
+      ensures Valid() ==> this in Repr
+
+    // Convenience predicate for when your object's validity depends on one
+    // or more other objects.
+    predicate ValidComponent(component: Validatable)
+      reads this, Repr 
+    {
+      && component in Repr
+      && component.Repr <= Repr
+      && this !in component.Repr
+      && component.Valid()
+    }
+
+    // Convenience predicate, since you often want to assert that 
+    // new objects in Repr are fresh as well in most postconditions.
+    twostate predicate ValidAndDisjoint()
+      reads this, Repr
+    {
+      Valid() && fresh(Repr - old(Repr))
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/Frames.dfy.expect b/src/Frames.dfy.expect
new file mode 100644
index 00000000..00a51f82
--- /dev/null
+++ b/src/Frames.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 3 verified, 0 errors

From adcbeff1ea0b9003334f0e0b4d44a8531a92ed31 Mon Sep 17 00:00:00 2001
From: Robin Salkeld <salkeldr@amazon.com>
Date: Tue, 5 Oct 2021 15:12:35 -0700
Subject: [PATCH 2/2] Add example

---
 examples/Frames.dfy        | 99 ++++++++++++++++++++++++++++++++++++++
 examples/Frames.dfy.expect |  2 +
 src/Frames.dfy             |  2 +-
 3 files changed, 102 insertions(+), 1 deletion(-)
 create mode 100644 examples/Frames.dfy
 create mode 100644 examples/Frames.dfy.expect

diff --git a/examples/Frames.dfy b/examples/Frames.dfy
new file mode 100644
index 00000000..528d971e
--- /dev/null
+++ b/examples/Frames.dfy
@@ -0,0 +1,99 @@
+
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+include "../src/Frames.dfy"
+
+module ValidatableExample {
+
+  import opened Frames
+
+  // Example loosely based on Chapters 8 and 9 of "Using Dafny, an Automatic Program Verifier":
+  // http://leino.science/papers/krml221.pdf
+
+  class Cell extends Validatable {
+    // public variables
+    var Data: int;    
+
+    function Valid(): bool
+      reads this, Repr
+    {
+      Repr == {this}
+    }
+
+    constructor()
+      ensures Valid() && fresh(Repr - {this})
+      ensures Data == 0
+    {
+      Data := 0;
+      Repr := {this};
+    }
+
+    method Inc() 
+      requires Valid()
+      modifies Repr
+      ensures ValidAndDisjoint()
+      ensures Data == old(Data) + 1
+    {
+      Data := Data + 1;
+    }
+  }
+
+  class Counter extends Validatable {
+    // public variables
+    ghost var Value: int;
+    // private variables
+    var incs: Cell;
+    var decs: Cell;
+
+    function Valid(): bool
+      reads this, Repr
+    {
+      && this in Repr
+      && ValidComponent(incs)
+      && ValidComponent(decs)
+      && incs.Repr !! decs.Repr
+      && Value == incs.Data - decs.Data
+    }
+
+    constructor()
+      ensures Valid() && fresh(Repr - {this} - incs.Repr - decs.Repr)
+      ensures Value == 0
+    {
+      incs := new Cell();
+      decs := new Cell();
+      Value := 0;
+      new;
+      Repr := {this} + incs.Repr + decs.Repr;
+    }
+
+    method GetValue() returns (x: int)
+      requires Valid()
+      ensures x == Value
+    {
+      x := incs.Data - decs.Data;
+    }
+
+    method Inc()
+      requires Valid()
+      modifies Repr
+      ensures ValidAndDisjoint()
+      ensures Value == old(Value) + 1
+    {
+      incs.Inc();
+      Value := Value + 1;
+      Repr := {this} + incs.Repr + decs.Repr;
+    }
+
+    method Dec()
+      requires Valid()
+      modifies Repr
+      ensures ValidAndDisjoint()
+      ensures Value == old(Value) - 1
+    {
+      decs.Inc();
+      Value := Value - 1;
+      Repr := {this} + incs.Repr + decs.Repr;
+    }
+  }
+}
diff --git a/examples/Frames.dfy.expect b/examples/Frames.dfy.expect
new file mode 100644
index 00000000..66ffe366
--- /dev/null
+++ b/examples/Frames.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 14 verified, 0 errors
diff --git a/src/Frames.dfy b/src/Frames.dfy
index bafed7ca..88c9e7bf 100644
--- a/src/Frames.dfy
+++ b/src/Frames.dfy
@@ -39,4 +39,4 @@ module Frames {
       Valid() && fresh(Repr - old(Repr))
     }
   }
-}
\ No newline at end of file
+}