Reads for Function Composition and Map

Jan 21, 2015 at 10:56 AM
This is the simplest reads that I have been able to achieve for a function which composes two functions. Because of the ordering beween the reads and requires I have to guard one of the reads clauses by first checking if the x is in the range of the first function.
function Compose(f:int->int, g:int->int) : int->int
    reads f.reads(x)
    reads if f.requires(x) then g.reads(f(x)) else {} 
    requires f.requires(x) 
    requires g.requires(f(x)) 
      -> g(f(x))
The simplest I managed for a reads clause for a function which maps a function over a sequence was to extracted the reads into a separate function. This extracted function is recursive, and is also called from its own reads clause! Extracting it into a function also allowed me to put its essential property into its postcondition.
function MapSeq(xs:seq<int>, f:int->int) : seq<int>
   reads MapSeqReads(xs, f);
   requires forall x :: x in xs ==> f.requires(x);
   ensures |xs| == |MapSeq(xs,f)|;
   ensures forall x :: x in xs ==> f(x) in MapSeq(xs,f);
  if xs == [] then []
  else [f(xs[0])] + MapSeq(xs[1..], f) 

function MapSeqReads(xs:seq<int>, f:int->int) : set<object>
   reads if |xs| > 0 then f.reads(xs[0]) + MapSeqReads(xs[1..], f) else {};
   decreases xs;
   ensures forall x :: x in xs ==> f.reads(x) <= MapSeqReads(xs,f); 
  if xs == [] then {}
  else f.reads(xs[0]) + MapSeqReads(xs[1..],f)
For me, getting the reads correct was by far the most difficult part of these excercises.
Feb 26, 2015 at 5:48 PM
Edited Feb 28, 2015 at 12:36 PM
As maps are not objects I'm having trouble with phrasing the reads clause properly when accessing several objects through maps. I thought your post might help but I don't understand your code yet. Here is my intention. I hope the injected pseudocode is clear enough.
predicate valid(grp: SomeClass)
  reads grp, grp.myMap[all x where x in myMap]; // pseudocode obviously
  grp != null && forall k :: k in grp.myMap ==> grp.myMap[k] != null // && some more reading
EDIT: reads seems to accept a set of objects, thus my following attempt. This leaves me a "might be null" error positioned at myMap (most likely the mapped objects) despite the fact that I'm reading with the sole intent being to assert it is not null. So I can't read because it might be null and I can't assert it is not null because I can't read it. Help?
reads grp, set x | x in grp.myMap :: grp.myMap[x];
Mar 8, 2015 at 6:54 PM
I am not sure I fully understand what you say, but can you write something like:
reads grp;
reads set x | x in grp.myMap && grp.myMap[x]!=null :: grp.myMap[x];
Or perhaps:
reads grp;
reads if grp.myMap != null then set x | x in grp.myMap && grp.myMap[x]!=null :: grp.myMap[x] else {};
Mar 9, 2015 at 10:33 AM
Edited Mar 9, 2015 at 10:40 AM
Thanks for the reply. The position of the error message was inaccurate as it was grp itself that 'might be null'. The problem was mitigated by giving up on testing for null inside the predicate and requiring it a priory. I'm doing a cascade validation of objects that requires all objects in the map to satisfy their valid predicate before the top object's own is. Now a 'might be null' error is positioned at the valid word on line 7 (...Map[x].valid.reads()...), which I can only assume, in the light of the previous case, it means the myMap[x] object, which I determined not null just prior. How is this possible? Does the reads ignore the requires? In addition, an 'insufficient reads clause to invoke function' error is following the next word ".reads()", prompting questions like, how can the reads clause itself complain about an insufficient reads clause?
flatten concatenates the mapped objects with their valid predicate's reads requirements.
The top object's valid is in two parts because the requires clause needed in valid2.
predicate valid()
  reads this, valid2.reads();
{ this.notnull() && this.valid2() }

predicate valid2()
  requires this.notnull();
  reads this, flatten(set x | x in this.myMap :: {this.myMap[x]} + this.myMap[x].valid.reads()); // complains here
{ forall x :: x in this.myMap ==> this.myMap[x].valid() }

predicate notnull()
  reads this;
{ forall x :: x in this.myMap ==> this.myMap[x] != null } // <-- proven not null here

function flatten(nested: set<set<object>>) : set<object>
{ set x | forall y :: y in nested && x in y :: x }
The null problem goes away by doing the following, but there being an error like that in the first place confuses me. The second error remains.
reads this, flatten(
  set x | x in this.myMap :: {this.myMap[x]}
  + if this.myMap[x] != null then this.myMap[x].valid.reads() else {}
Mar 9, 2015 at 12:28 PM

I think the reads is independent of the requires. You have to guard the set comprehension in the reads l to make sure the set is defined even for situations which do not satisfied the requires.

In some sense, the reads must be total.

Mar 9, 2015 at 11:25 PM
Edited Mar 16, 2015 at 3:46 PM
Indeed the different clauses seems to be oblivious to each other. I thought only objects required entries in the reads clause but the reads() function seems to need to be mentioned also, or rather, something that enables it to be called does. Now the trouble is that the 'insufficient reads clause to invoke function' error persists even when all the mapped objects are extracted out to a reads clause of their own prior to mentioning .valid.reads() and .valid or .valid.reads are not accepted as they are not objects. What else am I missing here?
reads this;
reads set x | x in this.myMap :: this.myMap[x]; // works just fine
//reads set x | x in this.myMap && this.myMap[x] != null :: this.myMap[x].valid; <── not objects
//reads set x | x in this.myMap && this.myMap[x] != null :: this.myMap[x].valid.reads; <──┘
reads flatten( set x | x in this.myMap && this.myMap[x] != null :: this.myMap[x].valid.reads() ); // cannot call reads()
In a local frame (inside the mapped objects), reads() calls just fine.
function useless() : set<object>
  reads this, this.valid.reads();
{ this.valid.reads() }
EDIT: The following code works, so the problem might lie in the flatten function.
reads if 0 in this.myMap && this.myMap[0] != null then this.myMap[0].valid.reads() else {};
EDIT 2: The following does not work and exhibits the same error, so flatten is not the culprit.
reads set x | forall y :: y in this.myMap && this.myMap[y] != null && x in this.myMap[y].valid.reads();