Skip to content
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

Add mapValue #23

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Add mapValue #23

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions src/Collections/Maps/Maps.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,17 @@ module Maps {
m'
}

/* Map a function to the values of a map */
function method {:opaque} mapValue<K, V, V'>(f: V -> V', m: map<K, V>): (m':map<K, V'>)
Copy link
Member

Choose a reason for hiding this comment

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

Just a few suggestions:

Suggested change
function method {:opaque} mapValue<K, V, V'>(f: V -> V', m: map<K, V>): (m':map<K, V'>)
function method {:opaque} MapValues<K, V, V'>(f: V ~> V', m: map<K, V>): (m': map<K, V'>)
  • Pascal casing since that's what the style guide says:https://github.com/dafny-lang/libraries/blob/master/STYLE.md#naming-convention :)
  • You're already accounting for partial functions in your requires, but since you're declaring f to have type V -> V', that means f is a total function and its precondition is always just "true". V --> V' is the arrow type that allows for other non-trivial preconditions, and then V ~> V' is the even more general arrow type that allows for reads clauses as well. You'll have to add a reads clause to the function itself of course, something like reads set o | exists k in m.Keys :: o in f.reads(k).

requires forall k:: k in m.Keys ==> f.requires(m[k])
ensures m.Keys == m'.Keys
ensures |m| == |m'|
{
var result := map k | k in m :: f(m[k]);
assert |result.Keys| == |result|;
result
}

/* Keep all key-value pairs corresponding to the set of keys provided. */
function method {:opaque} Restrict<X, Y>(m: map<X, Y>, xs: set<X>): (m': map<X, Y>)
ensures m' == RemoveKeys(m, m.Keys - xs)
Expand Down
2 changes: 1 addition & 1 deletion src/Collections/Maps/Maps.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@

Dafny program verifier finished with 14 verified, 0 errors
Dafny program verifier finished with 15 verified, 0 errors