"Validatable" trait for classes using the Valid()/Repr idiom

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;
+    }
+  }
+}

examples/Frames.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 14 verified, 0 errors

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))
+    }
+  }
+}

src/Frames.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 3 verified, 0 errors