Keyval find specs

[plredmond]

Added specs for find to state that the return value i either refers to the correct index for the given key k, or refers to a value outside of the assigned indexes.

Test file test.ivy:

#lang ivy1.8

include collections

instance k : unbounded_sequence
instance v : unbounded_sequence
instance kv : keyval(index, k, v)

export kv.find

Test command:

$ ivy_check isolate=kv.iso test.ivy

Review request: @nano-o

• I've written the postcondition for find using implications to separate the two cases. I'm not sure if that's the right approach.

• Should I include assertions in the postcondition that the keyval structure is not changed? is assert s = old s enough, or do I need all of

    assert s.end = old s.end;                  
    assert s.key_at(I, K) = old s.key_at(I, K);
    assert s.value_at(I) = old s.value_at(I);  
  

[plredmond]

This line isn't required. We might choose to delete it.

[nano-o]

• I've written the postcondition for find using implications to separate the two cases. I'm not sure if that's the right approach.

This might be better:

assert s.key_at(I, k) -> s.key_at(i,k)
assert (i = end(s)) = (forall I . ~s.key_at(I,k));

The first is equivalent to yours but a little shorter, while the second one is more precise than yours.

• Should I include assertions in the postcondition that the keyval structure is not changed?

No, Ivy understands that only i changes in the loop.

[plredmond]

For the first one I had simplified it to exists I. s.key_at(I, k) -> i = I in my local copy, but I like yours better.

For the second I struggled to simplify it. Thanks for your suggestion!

[plredmond]

Pushed the rewrite of the invariant & implementation of find that we paired on.