title: keep track of legal values
body: <p>Assume two external functions init() and revoke(). Init() returns "valid" values, revoke() makes them invalid. I like to verify that use() only uses values which are initialized but not revoked. I don't know how to describe this property as predicate (think random session IDs) or otherwise.</p>
  
  <pre><code>#include &lt;lib.h&gt;
  
  // "ensures valid_val(\result)"
  extern int init();
  extern revoke(int);
  
  /*
   @ assigns \nothing;
   @ require valid_val(val);
   */
  void use(int val) {
      ...
  }
  
  int main() {
      int v = init();
      use(v);
      revoke(v);
  }
  </code></pre>