Skip to content

Commit

Permalink
Address more comments
Browse files Browse the repository at this point in the history
  • Loading branch information
@dnezam
dnezam committed Nov 23, 2023
1 parent df8a072 commit fe27837
Showing 1 changed file with 42 additions and 89 deletions.
131 changes: 42 additions & 89 deletions sets/sets.gobra
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
See LICENSE or go to https://github.com/viperproject/gobra-libs/blob/main/LICENSE
for full license details.

This file is inspired by the following content:
This file is inspired by the standard libraries and axiomatisations of the following verifiers:
- dafny-lang/libraries: https://github.com/dafny-lang/libraries/blob/master/src/Collections/Sets/Sets.dfy
- verus-lang/verus: https://github.com/verus-lang/verus/blob/main/source/pervasive/set_lib.rs
- why3: https://why3.lri.fr/stdlib/set.html
Expand All @@ -17,20 +17,14 @@ package sets
// ##(-I ../)
import utils "utils"

// QUES Do we want to have comments for every function? In some cases it is trivial, in other
// cases it feels like the natural language version is less understandable than the formal specs.
// TODO Improve comments

// Empty set
// *********
// A set is empty if it has cardinality 0.
ghost
decreases
pure func IsEmpty(xs set[int]) bool {
return len(xs) == 0
}

// Returns an empty set.
// Returns the empty set.
ghost
ensures IsEmpty(result)
decreases
Expand All @@ -56,8 +50,6 @@ pure func NotInEmpty(xs set[int], e int) utils.Unit {
return utils.Unit{}
}

// Singleton set
// **************
// A set is a singleton if it has cardinality 1.
ghost
decreases
Expand All @@ -74,7 +66,7 @@ pure func SingletonSet(e int) (result set[int]) {
return set[int]{e}
}

// If a is in a singleton set x, then x is of the form {a}
// If a is in a singleton set x, then x is of the form {a}.
ghost
requires IsSingleton(xs)
requires e in xs
Expand All @@ -95,9 +87,7 @@ pure func SingletonEquality(xs set[int], a int, b int) utils.Unit {
return let _ := choose(xs) in utils.Unit{}
}

// Constructing new sets
// **********************
// Construct a set with all integers in the range [a, b).
// Constructs a set with all integers in the range [a, b).
ghost
requires a <= b
ensures forall i int :: { i in result } (a <= i && i < b) == i in result
Expand All @@ -107,7 +97,7 @@ pure func Range(a, b int) (result set[int]) {
return a == b ? EmptySet() : Add(Range(a + 1, b), a)
}

// Construct a set with all integers in the range [0, n).
// Constructs a set with all integers in the range [0, n).
ghost
requires n >= 0
ensures forall i int :: { i in result } (0 <= i && i < n) == i in result
Expand All @@ -129,9 +119,6 @@ pure func ToMultiset(s set[int]) (ms mset[int]) {
((mset[int] {}) union (mset[int] {x})) union ToMultiset(Remove(s, x))
}


// choose axiom
// ************
// Returns an element from a non-empty set.
ghost
requires !IsEmpty(xs)
Expand All @@ -140,8 +127,6 @@ ensures IsSingleton(xs) ==> xs == SingletonSet(e)
decreases
pure func choose(xs set[int]) (e int)

// General definitions and properties
// **********************************
// Returns whether xs and ys are disjoint sets.
ghost
decreases
Expand All @@ -157,8 +142,6 @@ pure func SetEquality(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}

// Subset
// ******
// Definition of subset without quantifiers.
ghost
requires e in xs
Expand Down Expand Up @@ -187,7 +170,7 @@ pure func SubsetIsTransitive(xs, ys, zs set[int]) utils.Unit {
return utils.Unit{}
}

// If x is a subset of y and both have the same cardinality, they are equal.
// If xs is a subset of ys and both have the same cardinality, they are equal.
ghost
requires xs subset ys
requires len(xs) == len(ys)
Expand All @@ -197,16 +180,14 @@ pure func SubsetEquality(xs, ys set[int]) utils.Unit {
return utils.Asserting(len(ys setminus xs) == len(ys) - len(xs))
}

// Returns whether x is a proper subset of y.
// Returns whether xs is a proper subset of ys.
ghost
decreases
pure func IsProperSubset(xs, ys set[int]) bool {
return xs subset ys && xs != ys
}

// Union
// *****
// If an e is in the union of xs and ys, then it must be in xs or ys.
// If e is in the union of xs and ys, then it must be in xs or ys.
ghost
ensures (e in (xs union ys)) == ((e in xs) || (e in ys))
decreases
Expand All @@ -222,39 +203,36 @@ pure func UnionIsCommutative(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}

// Union is idempotent.
ghost
ensures (xs union ys) union ys == xs union ys
decreases
pure func UnionIsRightIdempotent(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}

ghost
ensures xs union (xs union ys) == xs union ys
decreases
pure func UnionIsLeftIdempotent(xs, ys set[int]) utils.Unit {
pure func UnionIsIdempotent(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}

// Add (union with singleton)
// **************************
// Add an element x to the set xs.
// Add x to xs.
ghost
// Need this post-condition to verify CardinalAdd
// Need this post-condition first to ensure the properties about the length.
ensures (e in xs) ==> res == xs
ensures (e in xs) ==> (len(res) == len(xs))
ensures !(e in xs) ==> (len(res) == len(xs) + 1)
ensures e in res
decreases
pure func Add(xs set[int], e int) (res set[int]) {
return xs union SingletonSet(e)
}

// If a is in xs union {b}, then a is equal to b, or a was already in xs.
ghost
ensures (a in Add(xs, b)) == ((a == b) || a in xs)
decreases
pure func InAdd(xs set[int], a, b int) utils.Unit {
return utils.Unit{}
}

// If a is in xs, then a will remain in xs no matter what we add to it.
ghost
requires a in xs
ensures a in Add(xs, b)
Expand All @@ -263,43 +241,34 @@ pure func InvarianceInAdd(xs set[int], a, b int) utils.Unit {
return utils.Unit{}
}

// Remove (setminus with singleton)
// ********************************
// Remove the element x from the set xs.
// QUES Should we add something like ensures !(x in xs) ==> xs == Remove(xs, x)
// like we did for Add?
// Remove e from xs. Does not require e to be in xs.
ghost
ensures !(e in xs) ==> result == xs
ensures (e in xs) ==> (len(result) == len(xs) - 1)
ensures !(e in xs) ==> (len(result) == len(xs))
decreases
pure func Remove(xs set[int], e int) set[int] {
pure func Remove(xs set[int], e int) (result set[int]) {
return xs setminus SingletonSet(e)
}

// Intersection
// ************
// Intersection is commutative.
ghost
ensures (xs intersection ys) == (ys intersection xs)
decreases
pure func IntersectionIsCommutative(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}

// Intersection is idempotent.
ghost
ensures (xs intersection ys) intersection ys == (xs intersection ys)
decreases
pure func IntersectionIsRightIdempotent(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}

ghost
ensures xs intersection (xs intersection ys) == (xs intersection ys)
decreases
pure func IntersectionIsLeftIdempotent(xs, ys set[int]) utils.Unit {
pure func IntersectionIsIdempotent(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}


// Setminus
// ********
// If e is in the difference xs - ys, then e must be in xs but not in ys.
ghost
ensures (e in (xs setminus ys)) == ((e in xs) && !(e in ys))
decreases
Expand All @@ -316,15 +285,16 @@ pure func NotInDifference(xs, ys set[int], e int) utils.Unit {
return utils.Unit{}
}

// Relating multiple operations
// ****************************
// If e is in the intersection of xs and ys, then e must be both in xs and ys.
ghost
ensures e in (xs intersection ys) == ((e in xs) && (e in ys))
decreases
pure func InIntersectionInBoth(xs, ys set[int], e int) utils.Unit {
return utils.Unit{}
}

// If xs and ys are disjoint, adding and then removing one from the other
// yields the original set.
ghost
requires AreDisjoint(xs, ys)
ensures (xs union ys) setminus xs == ys
Expand All @@ -343,7 +313,7 @@ pure func AddRemove(xs set[int], e int) utils.Unit {
return utils.Unit{}
}

// If we remove x from the set xs, it doesn't matter whether we have added x
// If we remove e from the set xs, it doesn't matter whether we have added e
// to it before.
ghost
ensures Remove(Add(xs, e), e) == Remove(xs, e)
Expand All @@ -352,52 +322,40 @@ pure func RemoveAdd(xs set[int], e int) utils.Unit {
return utils.Unit{}
}

// xs - {e} is a subset of xs.
ghost
ensures Remove(xs, e) subset xs
decreases
pure func SubsetRemove(xs set[int], e int) utils.Unit {
return utils.Unit{}
}

// QUES Should we merge SubsetUnion1 and SubsetUnion2?
// xs and ys are subsets of the union of xs and ys.
ghost
ensures xs subset (xs union ys)
decreases
pure func SubsetUnion1(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}

ghost
ensures ys subset (xs union ys)
decreases
pure func SubsetUnion2(xs, ys set[int]) utils.Unit {
pure func SubsetUnion(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}

// The intersection of xs and ys are subsets of xs, and ys.
ghost
ensures (xs intersection ys) subset xs
decreases
pure func SubsetIntersection1(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}

ghost
ensures (xs intersection ys) subset ys
decreases
pure func SubsetIntersection2(xs, ys set[int]) utils.Unit {
pure func SubsetIntersection(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}

// The difference xs - ys is a subset of xs.
ghost
ensures (xs setminus ys) subset xs
decreases
pure func SubsetDifference(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}


// Cardinality
// ***********
// The cardinality of a set is non-negative.
ghost
ensures len(xs) >= 0
Expand Down Expand Up @@ -481,6 +439,8 @@ pure func DifferenceLenEq(xs, ys set[int]) utils.Unit {
return utils.Unit{}
}

// If e is in xs, adding it to xs doesn't change the cardinality.
// If e is not in xs, adding it to xs increases the cardinality by 1.
ghost
ensures (e in xs) ==> (len(Add(xs, e)) == len(xs))
ensures !(e in xs) ==> (len(Add(xs, e)) == len(xs) + 1)
Expand All @@ -489,6 +449,8 @@ func AddLen(xs set[int], e int) utils.Unit {
return utils.Unit{}
}

// If e is in xs, removing it from xs reduces the cardinality by 1.
// If e is not in xs, removing it from xs doesn't change the cardinality.
ghost
ensures (e in xs) ==> (len(Remove(xs, e)) == len(xs) - 1)
ensures !(e in xs) ==> (len(Remove(xs, e)) == len(xs))
Expand All @@ -497,6 +459,8 @@ func RemoveLen(xs set[int], e int) utils.Unit {
return utils.Unit{}
}

// If xs and ys are disjoint, the cardinality of their union is equal to the
// sum of the cardinality of xs, and the cardinality of ys.
ghost
requires AreDisjoint(xs, ys)
ensures len(xs union ys) == len(xs) + len(ys)
Expand All @@ -514,16 +478,5 @@ pure func DisjointUnionLen(xs, ys set[int]) utils.Unit {
// requires a <= b
// ensures |x| <= b - a

// *****************

// QUES S3: min_elt{,_def}, max_elt{,_def} mention forall x . x in xs in
// their post-condition; do we want these functions?


// S3 The sections in "Finite Monomorphic sets" suggest to move cardinality properties as a
// postcondition to functions that "generate" it
// Empty() would return an empty list, but also ensure that its cardinality is 0
// Add(xs, x) would return a set where x has been added to xs, but also ensure that
// the cardinality stays the same if x was already in xs, or increases if it wasnt
// A similar consideration is made for Singleton(x) and Remove(xs, x)
// QUES Do we want to merge functions like this?
// their post-condition; do we want these functions?

0 comments on commit fe27837

Please sign in to comment.