title: What does code outside a Dafny class verify, but not when encapsulated?
body: <p>Some code that verifies outside of a Dafny class fails to verify when encapsulated. I'm wondering (1) why, and (2) how to get the best of both worlds: encapsulation/abstraction and verification. The code models a "relation" as a pair: a domain set and a set of pairs over the domain set. Two versions are presented below. The first verifies, the second does not.</p>
  
  <p>The code defines a validity condition that requires that the pairs in the pair set actually be over the domain. It defines a predicate, isFunction, that returns true if the "relation" so modeled is single-valued. This is the predicate that verifies in one case but not in the other. The code, in the Main routine, then verifies that ( dom = {1,2,3,4}, pairs = { (1,1), (2,2), (3,3), (4,4 ) } ) is single-valued (a function). However, when I encapsulate the domain and pairs sets in a class, and make predicates into member functions, the same code in Main no longer verifies. </p>
  
  <p>UNENCAPSULATED VERSION:</p>
  
  <pre><code>/*
  Represent a finite binary relation on a set, S, 
  as a pair: the set S and a set of pairs (to be
  drawn from S)
  */ 
  type relationS&lt;T&gt; = (set&lt;T&gt;,set&lt;(T,T)&gt;)
  
  
  /*
  A de-facto Valid() predicate that checks that that each 
  value in each pair in pairs is a member ofthe domain set.
  */
  function method relS&lt;T(!new)&gt;(dom: set&lt;T&gt;, pairs: set&lt;(T,T)&gt;): 
  relationS&lt;T&gt; 
      requires forall x, y :: (x, y) in pairs ==&gt; x in dom &amp;&amp; y in dom
  {
      (dom, pairs)
  }
  
  /*
  Projection function: Given a relation on S, return its co/domain set.
  */
  function method domS&lt;T&gt;(r: relationS&lt;T&gt;): set&lt;T&gt;
  {
      r.0
  }
  
  /*
  Projection function: Given a relation on S, return its set of pairs.
  */
  function method pairsS&lt;T&gt;(r: relationS&lt;T&gt;): set&lt;(T,T)&gt;
  {
      r.1
  }
  
  /*
  Return true iff the relation is single-valued (a function)
  */
  predicate isFunctionS&lt;T&gt;(r: relationS&lt;T&gt;)
  {
    forall x, y, z :: x in domS(r) &amp;&amp; y in domS(r) &amp;&amp; z in domS(r) &amp;&amp;
                      (x, y) in pairsS(r) &amp;&amp; 
                      (x, z) in pairsS(r) ==&gt; 
                      y == z  
  }
  
  method Main()
  {
      var d := {1, 2, 3, 4};
      var h := { (1,1), (2,2), (3,3), (4,4) };
      var r1 := relS(d,h);
      assert isFunctionS(r1);        // Verifies
  }
  </code></pre>
  
  <p>ENCAPSULATED VERSION (sorry for slightly different identifiers)</p>
  
  <pre><code>/*
  Abstraction of a finite binary relation on a 
  set, S. Underlying representation is a pair: 
  the domain set, S, and a set of pairs over S.
  */ 
  class binRelationS&lt;T(!new,==)&gt;
  {
      var d: set&lt;T&gt;;
      var p: set&lt;(T,T)&gt;;
      predicate Valid()
          reads this;
      {
          forall x, y :: (x, y) in p ==&gt; x in d &amp;&amp; y in d
      }
  
      /*
      Constructor requires that all values appearing in 
      any of the pairs in p be in d. That is, the pairs
      in p must represent a relation on domain, d.
      */
      constructor(dom: set&lt;T&gt;, pairs: set&lt;(T,T)&gt;)
          requires forall x, y :: 
              (x, y) in pairs ==&gt; x in dom &amp;&amp; y in dom;
          ensures Valid();
      {
          d := dom;
          p := pairs;
      }
  
      function method dom(): set&lt;T&gt;
          requires Valid();
          reads this;
          ensures Valid();
      {
          d
      }
  
      function method rel(): set&lt;(T,T)&gt;
          requires Valid();
          reads this
          ensures Valid();
      {
          p
      }
  
      /*
      Return true iff the relation is single-valued (a function)
      */
      predicate isFunction()
          requires Valid();
          reads this;
          ensures Valid();
      {
          forall x, y, z :: 
              x in d &amp;&amp; y in d &amp;&amp; z in d &amp;&amp;
              (x, y) in p &amp;&amp; (x, z) in p ==&gt; 
              y == z  
      }
  }
  
  method Main()
  {
      var d := {1, 2, 3, 4};
      var h := { (1,1), (2,2), (3,3), (4,4) };
      var r := new binRelationS(d,h);
      assert r.isFunction();          // assertion violation
  }
  </code></pre>