8000 Keyval find specs by plredmond · Pull Request #85 · kenmcmil/ivy · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Keyval find specs #85

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Keyval find specs #85

wants to merge 3 commits into from

Conversation

plredmond
Copy link
@plredmond plredmond commented Nov 26, 2024 •
edited
Loading

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
plredmond commented Nov 26, 2024
View reviewed changes
ivy/include/1.8/collections.ivy Outdated
i := i.next;
}
assert end <= i | repr(s).value(i).p_key = k;
Copy link
Author
@plredmond plredmond Nov 26, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@nano-o
Copy link
nano-o commented Nov 26, 2024
  • 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
Copy link
Author

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
Copy link
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@plredmond @nano-o
0