Struct vstd::seq::Seq

source · 
pub struct Seq<A> { /* private fields */ }
Expand description

Seq<A> is a sequence type for specifications. To use a “sequence” in compiled code, use an exec type like vec::Vec that has Seq<A> as its specification type.

An object seq: Seq<A> has a length, given by seq.len(), and a value at each i for 0 <= i < seq.len(), given by seq[i].

Sequences can be constructed in a few different ways:

  • Seq::empty construct an empty sequence (len() == 0)
  • Seq::new construct a sequence of a given length, initialized according to a given function mapping indices i to values A.
  • The seq! macro, to construct small sequences of a fixed size (analagous to the std::vec! macro).
  • By manipulating an existing sequence with Seq::push, Seq::update, or Seq::add.

To prove that two sequences are equal, it is usually easiest to use the extensional equality operator =~=.

Implementations§

source§

impl<A> Seq<A>

source

pub uninterp fn empty() -> Seq<A>

An empty sequence (i.e., a sequence of length 0).

source

pub uninterp fn new(len: nat, f: impl Fn(int) -> A) -> Seq<A>

Construct a sequence s of length len where entry s[i] is given by f(i).

source

pub uninterp fn len(self) -> nat

The length of a sequence.

source

pub uninterp fn index(self, i: int) -> A

recommends
0 <= i < self.len(),

Gets the value at the given index i.

If i is not in the range [0, self.len()), then the resulting value is meaningless and arbitrary.

source

pub open spec fn spec_index(self, i: int) -> A

recommends
0 <= i < self.len(),
{ self.index(i) }

[] operator, synonymous with index

source

pub uninterp fn push(self, a: A) -> Seq<A>

Appends the value a to the end of the sequence. This always increases the length of the sequence by 1. This often requires annotating the type of the element literal in the sequence, e.g., 10int.

§Example
proof fn push_test() {
    assert(seq![10int, 11, 12].push(13) =~= seq![10, 11, 12, 13]);
}
source

pub uninterp fn update(self, i: int, a: A) -> Seq<A>

recommends
0 <= i < self.len(),

Updates the sequence at the given index, replacing the element with the given value, and leaves all other entries unchanged.

§Example
proof fn update_test() {
    let s = seq![10, 11, 12, 13, 14];
    let t = s.update(2, -5);
    assert(t =~= seq![10, 11, -5, 13, 14]);
}
source

pub uninterp fn subrange(self, start_inclusive: int, end_exclusive: int) -> Seq<A>

recommends
0 <= start_inclusive <= end_exclusive <= self.len(),

Returns a sequence for the given subrange.

§Example
proof fn subrange_test() {
    let s = seq![10int, 11, 12, 13, 14];
    //                      ^-------^
    //           0      1   2   3   4   5
    let sub = s.subrange(2, 4);
    assert(sub =~= seq![12, 13]);
}
source

pub open spec fn take(self, n: int) -> Seq<A>

{ self.subrange(0, n) }

Returns a sequence containing only the first n elements of the original sequence

source

pub open spec fn skip(self, n: int) -> Seq<A>

{ self.subrange(n, self.len() as int) }

Returns a sequence without the first n elements of the original sequence

source

pub uninterp fn add(self, rhs: Seq<A>) -> Seq<A>

Concatenates the sequences.

§Example
proof fn add_test() {
    assert(seq![10int, 11].add(seq![12, 13, 14])
            =~= seq![10, 11, 12, 13, 14]);
}
source

pub open spec fn spec_add(self, rhs: Seq<A>) -> Seq<A>

{ self.add(rhs) }

+ operator, synonymous with add

source

pub open spec fn last(self) -> A

recommends
0 < self.len(),
{ self[self.len() as int - 1] }

Returns the last element of the sequence.

source

pub open spec fn first(self) -> A

recommends
0 < self.len(),
{ self[0] }

Returns the first element of the sequence.

source§

impl<A> Seq<A>

source

pub open spec fn map<B>(self, f: FnSpec<(int, A), B>) -> Seq<B>

{ Seq::new(self.len(), |i: int| f(i, self[i])) }

Applies the function f to each element of the sequence, and returns the resulting sequence. The int parameter of f is the index of the element being mapped.

source

pub open spec fn map_values<B>(self, f: FnSpec<(A,), B>) -> Seq<B>

{ Seq::new(self.len(), |i: int| f(self[i])) }

Applies the function f to each element of the sequence, and returns the resulting sequence.

source

pub open spec fn is_prefix_of(self, other: Self) -> bool

{ self.len() <= other.len() && (self =~= other.subrange(0, self.len() as int)) }

Is true if the calling sequence is a prefix of the given sequence ‘other’.

§Example
proof fn prefix_test() {
    let pre: Seq<int> = seq![1, 2, 3];
    let whole: Seq<int> = seq![1, 2, 3, 4, 5];
    assert(pre.is_prefix_of(whole));
}
source

pub open spec fn is_suffix_of(self, other: Self) -> bool

{
    self.len() <= other.len()
        && (self
            =~= other.subrange((other.len() - self.len()) as int, other.len() as int))
}

Is true if the calling sequence is a suffix of the given sequence ‘other’.

§Example
proof fn suffix_test() {
    let end: Seq<int> = seq![3, 4, 5];
    let whole: Seq<int> = seq![1, 2, 3, 4, 5];
    assert(end.is_suffix_of(whole));
}
source

pub closed spec fn sort_by(self, leq: FnSpec<(A, A), bool>) -> Seq<A>

recommends
total_ordering(leq),

Sorts the sequence according to the given leq function

§Example
{{#include ../../../rust_verify/example/multiset.rs:sorted_by_leq}}
source

pub proof fn lemma_sort_by_ensures(self, leq: FnSpec<(A, A), bool>)

requires
total_ordering(leq),
ensures
self.to_multiset() =~= self.sort_by(leq).to_multiset(),
sorted_by(self.sort_by(leq), leq),
forall |x: A| !self.contains(x) ==> !(#[trigger] self.sort_by(leq).contains(x)),
source

pub open spec fn filter(self, pred: FnSpec<(A,), bool>) -> Self

{
    if self.len() == 0 {
        self
    } else {
        let subseq = self.drop_last().filter(pred);
        if pred(self.last()) { subseq.push(self.last()) } else { subseq }
    }
}

Returns the sequence containing only the elements of the original sequence such that pred(element) is true.

§Example
proof fn filter_test() {
   let seq: Seq<int> = seq![1, 2, 3, 4, 5];
   let even: Seq<int> = seq.filter(|x| x % 2 == 0);
   reveal_with_fuel(Seq::<int>::filter, 6); //Needed for Verus to unfold the recursive definition of filter
   assert(even =~= seq![2, 4]);
}
source

pub broadcast proof fn lemma_filter_len(self, pred: FnSpec<(A,), bool>)

ensures
#[trigger] self.filter(pred).len() <= self.len(),
source

pub broadcast proof fn lemma_filter_pred(self, pred: FnSpec<(A,), bool>, i: int)

requires
0 <= i < self.filter(pred).len(),
ensures
pred(#[trigger] self.filter(pred)[i]),
source

pub broadcast proof fn lemma_filter_contains(self, pred: FnSpec<(A,), bool>, i: int)

requires
0 <= i < self.len() && pred(self[i]),
ensures
#[trigger] self.filter(pred).contains(self[i]),
source

pub proof fn filter_lemma(self, pred: FnSpec<(A,), bool>)

👎Deprecated: Use broadcast use group_filter_ensures instead
ensures
forall |i: int| {
    0 <= i < self.filter(pred).len() ==> pred(#[trigger] self.filter(pred)[i])
},
forall |i: int| {
    0 <= i < self.len() && pred(self[i]) ==> #[trigger]
        self.filter(pred).contains(self[i])
},
#[trigger] self.filter(pred).len() <= self.len(),
source

pub broadcast proof fn filter_distributes_over_add(a: Self, b: Self, pred: FnSpec<(A,), bool>)

ensures
#[trigger] (a + b).filter(pred) == a.filter(pred) + b.filter(pred),
source

pub broadcast proof fn add_empty_left(a: Self, b: Self)

requires
a.len() == 0,
ensures
#[trigger] (a + b) == b,
source

pub broadcast proof fn add_empty_right(a: Self, b: Self)

requires
b.len() == 0,
ensures
#[trigger] (a + b) == a,
source

pub broadcast proof fn push_distributes_over_add(a: Self, b: Self, elt: A)

ensures
#[trigger] (a + b).push(elt) == a + b.push(elt),
source

pub open spec fn max_via(self, leq: FnSpec<(A, A), bool>) -> A

recommends
self.len() > 0,
{
    if self.len() > 1 {
        if leq(self[0], self.subrange(1, self.len() as int).max_via(leq)) {
            self.subrange(1, self.len() as int).max_via(leq)
        } else {
            self[0]
        }
    } else {
        self[0]
    }
}

Returns the maximum value in a non-empty sequence, given sorting function leq

source

pub open spec fn min_via(self, leq: FnSpec<(A, A), bool>) -> A

recommends
self.len() > 0,
{
    if self.len() > 1 {
        let subseq = self.subrange(1, self.len() as int);
        let elt = subseq.min_via(leq);
        if leq(elt, self[0]) { elt } else { self[0] }
    } else {
        self[0]
    }
}

Returns the minimum value in a non-empty sequence, given sorting function leq

source

pub open spec fn contains(self, needle: A) -> bool

{ exists |i: int| 0 <= i < self.len() && self[i] == needle }
source

pub open spec fn index_of(self, needle: A) -> int

{ choose |i: int| 0 <= i < self.len() && self[i] == needle }

Returns an index where needle appears in the sequence. Returns an arbitrary value if the sequence does not contain the needle.

source

pub closed spec fn index_of_first(self, needle: A) -> result : Option<int>

For an element that occurs at least once in a sequence, if its first occurence is at index i, Some(i) is returned. Otherwise, None is returned

source

pub proof fn index_of_first_ensures(self, needle: A)

ensures
match self.index_of_first(needle) {
    Some(index) => (
        &&& self.contains(needle)
        &&& 0 <= index < self.len()
        &&& self[index] == needle
        &&& forall |j: int| 0 <= j < index < self.len() ==> self[j] != needle

    ),
    None => !self.contains(needle),
},
source

pub closed spec fn index_of_last(self, needle: A) -> Option<int>

For an element that occurs at least once in a sequence, if its last occurence is at index i, Some(i) is returned. Otherwise, None is returned

source

pub proof fn index_of_last_ensures(self, needle: A)

ensures
match self.index_of_last(needle) {
    Some(index) => (
        &&& self.contains(needle)
        &&& 0 <= index < self.len()
        &&& self[index] == needle
        &&& forall |j: int| 0 <= index < j < self.len() ==> self[j] != needle

    ),
    None => !self.contains(needle),
},
source

pub open spec fn drop_last(self) -> Seq<A>

recommends
self.len() >= 1,
{ self.subrange(0, self.len() as int - 1) }

Drops the last element of a sequence and returns a sequence whose length is thereby 1 smaller.

If the input sequence is empty, the result is meaningless and arbitrary.

source

pub proof fn drop_last_distributes_over_add(a: Self, b: Self)

requires
0 < b.len(),
ensures
(a + b).drop_last() == a + b.drop_last(),

Dropping the last element of a concatenation of a and b is equivalent to skipping the last element of b and then concatenating a and b

source

pub open spec fn drop_first(self) -> Seq<A>

recommends
self.len() >= 1,
{ self.subrange(1, self.len() as int) }
source

pub open spec fn no_duplicates(self) -> bool

{
    forall |i, j| {
        (0 <= i < self.len() && 0 <= j < self.len() && i != j) ==> self[i] != self[j]
    }
}

returns true if the sequence has no duplicate elements

source

pub open spec fn disjoint(self, other: Self) -> bool

{
    forall |i: int, j: int| {
        0 <= i < self.len() && 0 <= j < other.len() ==> self[i] != other[j]
    }
}

Returns true if two sequences are disjoint

source

pub open spec fn to_set(self) -> Set<A>

{ Set::new(|a: A| self.contains(a)) }

Converts a sequence into a set

source

pub closed spec fn to_multiset(self) -> Multiset<A>

Converts a sequence into a multiset

source

pub broadcast proof fn to_multiset_ensures(self)

ensures
forall |a: A| #[trigger] (self.push(a).to_multiset()) =~= self.to_multiset().insert(a),
forall |i: int| {
    0 <= i < self.len()
        ==> (#[trigger] (self.remove(i).to_multiset())
            =~= self.to_multiset().remove(self[i]))
},
self.len() == #[trigger] self.to_multiset().len(),
forall |a: A| self.contains(a) <==> #[trigger] self.to_multiset().count(a) > 0,

Proof of function to_multiset() correctness

source

pub open spec fn insert(self, i: int, a: A) -> Seq<A>

recommends
0 <= i <= self.len(),
{ self.subrange(0, i).push(a) + self.subrange(i, self.len() as int) }

Insert item a at index i, shifting remaining elements (if any) to the right

source

pub proof fn insert_ensures(self, pos: int, elt: A)

requires
0 <= pos <= self.len(),
ensures
self.insert(pos, elt).len() == self.len() + 1,
forall |i: int| 0 <= i < pos ==> #[trigger] self.insert(pos, elt)[i] == self[i],
forall |i: int| pos <= i < self.len() ==> self.insert(pos, elt)[i + 1] == self[i],
self.insert(pos, elt)[pos] == elt,

Proof of correctness and expected properties of insert function

source

pub open spec fn remove(self, i: int) -> Seq<A>

recommends
0 <= i < self.len(),
{ self.subrange(0, i) + self.subrange(i + 1, self.len() as int) }

Remove item at index i, shifting remaining elements to the left

source

pub proof fn remove_ensures(self, i: int)

requires
0 <= i < self.len(),
ensures
self.remove(i).len() == self.len() - 1,
forall |index: int| 0 <= index < i ==> #[trigger] self.remove(i)[index] == self[index],
forall |index: int| {
    i <= index < self.len() - 1 ==> #[trigger] self.remove(i)[index] == self[index + 1]
},

Proof of function remove() correctness

source

pub open spec fn remove_value(self, val: A) -> Seq<A>

{
    let index = self.index_of_first(val);
    match index {
        Some(i) => self.remove(i),
        None => self,
    }
}

If a given element occurs at least once in a sequence, the sequence without its first occurrence is returned. Otherwise the same sequence is returned.

source

pub open spec fn reverse(self) -> Seq<A>

{
    if self.len() == 0 {
        Seq::empty()
    } else {
        Seq::new(self.len(), |i: int| self[self.len() - 1 - i])
    }
}

Returns the sequence that is in reverse order to a given sequence.

source

pub open spec fn zip_with<B>(self, other: Seq<B>) -> Seq<(A, B)>

recommends
self.len() == other.len(),
{
    if self.len() != other.len() {
        Seq::empty()
    } else if self.len() == 0 {
        Seq::empty()
    } else {
        Seq::new(self.len(), |i: int| (self[i], other[i]))
    }
}

Zips two sequences of equal length into one sequence that consists of pairs. If the two sequences are different lengths, returns an empty sequence

source

pub open spec fn fold_left<B>(self, b: B, f: FnSpec<(B, A), B>) -> res : B

{ if self.len() == 0 { b } else { f(self.drop_last().fold_left(b, f), self.last()) } }

Folds the sequence to the left, applying f to perform the fold.

Equivalent to Iterator::fold in Rust.

Given a sequence s = [x0, x1, x2, ..., xn], applying this function s.fold_left(b, f) returns f(...f(f(b, x0), x1), ..., xn).

source

pub open spec fn fold_left_alt<B>(self, b: B, f: FnSpec<(B, A), B>) -> res : B

{
    if self.len() == 0 {
        b
    } else {
        self.subrange(1, self.len() as int).fold_left_alt(f(b, self[0]), f)
    }
}

Equivalent to Self::fold_left but defined by breaking off the leftmost element when recursing, rather than the rightmost. See Self::lemma_fold_left_alt that proves equivalence.

source

pub proof fn lemma_fold_left_alt<B>(self, b: B, f: FnSpec<(B, A), B>)

ensures
self.fold_left(b, f) == self.fold_left_alt(b, f),

Self::fold_left and Self::fold_left_alt are equivalent.

source

pub open spec fn fold_right<B>(self, f: FnSpec<(A, B), B>, b: B) -> res : B

{ if self.len() == 0 { b } else { self.drop_last().fold_right(f, f(self.last(), b)) } }

Folds the sequence to the right, applying f to perform the fold.

Equivalent to DoubleEndedIterator::rfold in Rust.

Given a sequence s = [x0, x1, x2, ..., xn], applying this function s.fold_right(b, f) returns f(x0, f(x1, f(x2, ..., f(xn, b)...))).

source

pub open spec fn fold_right_alt<B>(self, f: FnSpec<(A, B), B>, b: B) -> res : B

{
    if self.len() == 0 {
        b
    } else {
        f(self[0], self.subrange(1, self.len() as int).fold_right_alt(f, b))
    }
}

Equivalent to Self::fold_right but defined by breaking off the leftmost element when recursing, rather than the rightmost. See Self::lemma_fold_right_alt that proves equivalence.

source

pub proof fn lemma_fold_right_split<B>(self, f: FnSpec<(A, B), B>, b: B, k: int)

requires
0 <= k <= self.len(),
ensures
self.subrange(0, k).fold_right(f, self.subrange(k, self.len() as int).fold_right(f, b))
    == self.fold_right(f, b),

A lemma that proves how Self::fold_right distributes over splitting a sequence.

source

pub proof fn lemma_fold_right_commute_one<B>(self, a: A, f: FnSpec<(A, B), B>, v: B)

requires
commutative_foldr(f),
ensures
self.fold_right(f, f(a, v)) == f(a, self.fold_right(f, v)),
source

pub proof fn lemma_fold_right_alt<B>(self, f: FnSpec<(A, B), B>, b: B)

ensures
self.fold_right(f, b) == self.fold_right_alt(f, b),

Self::fold_right and Self::fold_right_alt are equivalent.

source

pub proof fn lemma_multiset_has_no_duplicates(self)

requires
self.no_duplicates(),
ensures
forall |x: A| self.to_multiset().contains(x) ==> self.to_multiset().count(x) == 1,

Given a sequence with no duplicates, each element occurs only once in its conversion to a multiset

source

pub proof fn lemma_multiset_has_no_duplicates_conv(self)

requires
forall |x: A| self.to_multiset().contains(x) ==> self.to_multiset().count(x) == 1,
ensures
self.no_duplicates(),

If, in a sequence’s conversion to a multiset, each element occurs only once, the sequence has no duplicates.

source

pub proof fn lemma_add_last_back(self)

requires
0 < self.len(),
ensures
#[trigger] self.drop_last().push(self.last()) =~= self,

The concatenation of two subsequences derived from a non-empty sequence, the first obtained from skipping the last element, the second consisting only of the last element, is the original sequence.

source

pub proof fn lemma_indexing_implies_membership(self, f: FnSpec<(A,), bool>)

requires
forall |i: int| 0 <= i < self.len() ==> #[trigger] f(#[trigger] self[i]),
ensures
forall |x: A| #[trigger] self.contains(x) ==> #[trigger] f(x),

If a predicate is true at every index of a sequence, it is true for every member of the sequence as a collection. Useful for converting quantifiers between the two forms to satisfy a precondition in the latter form.

source

pub proof fn lemma_membership_implies_indexing(self, f: FnSpec<(A,), bool>)

requires
forall |x: A| #[trigger] self.contains(x) ==> #[trigger] f(x),
ensures
forall |i: int| 0 <= i < self.len() ==> #[trigger] f(self[i]),

If a predicate is true for every member of a sequence as a collection, it is true at every index of the sequence. Useful for converting quantifiers between the two forms to satisfy a precondition in the latter form.

source

pub proof fn lemma_split_at(self, pos: int)

requires
0 <= pos <= self.len(),
ensures
self.subrange(0, pos) + self.subrange(pos, self.len() as int) =~= self,

A sequence that is sliced at the pos-th element, concatenated with that same sequence sliced from the pos-th element, is equal to the original unsliced sequence.

source

pub proof fn lemma_element_from_slice(self, new: Seq<A>, a: int, b: int, pos: int)

requires
0 <= a <= b <= self.len(),
new == self.subrange(a, b),
a <= pos < b,
ensures
pos - a < new.len(),
new[pos - a] == self[pos],

Any element in a slice is included in the original sequence.

source

pub proof fn lemma_slice_of_slice(self, s1: int, e1: int, s2: int, e2: int)

requires
0 <= s1 <= e1 <= self.len(),
0 <= s2 <= e2 <= e1 - s1,
ensures
self.subrange(s1, e1).subrange(s2, e2) =~= self.subrange(s1 + s2, s1 + e2),

A slice (from s2..e2) of a slice (from s1..e1) of a sequence is equal to just a slice (s1+s2..s1+e2) of the original sequence.

source

pub proof fn unique_seq_to_set(self)

requires
self.no_duplicates(),
ensures
self.len() == self.to_set().len(),

A sequence of unique items, when converted to a set, produces a set with matching length

source

pub proof fn lemma_cardinality_of_set(self)

ensures
self.to_set().len() <= self.len(),

The cardinality of a set of elements is always less than or equal to that of the full sequence of elements.

source

pub proof fn lemma_cardinality_of_empty_set_is_0(self)

ensures
self.to_set().len() == 0 <==> self.len() == 0,

A sequence is of length 0 if and only if its conversion to a set results in the empty set.

source

pub proof fn lemma_no_dup_set_cardinality(self)

requires
self.to_set().len() == self.len(),
ensures
self.no_duplicates(),

A sequence with cardinality equal to its set has no duplicates. Inverse property of that shown in lemma unique_seq_to_set

source§

impl<A, B> Seq<(A, B)>

source

pub closed spec fn unzip(self) -> (Seq<A>, Seq<B>)

Unzips a sequence that contains pairs into two separate sequences.

source

pub proof fn unzip_ensures(self)

ensures
self.unzip().0.len() == self.unzip().1.len(),
self.unzip().0.len() == self.len(),
self.unzip().1.len() == self.len(),
forall |i: int| {
    0 <= i < self.len()
        ==> (#[trigger] self.unzip().0[i], #[trigger] self.unzip().1[i]) == self[i]
},

Proof of correctness and expected properties of unzip function

source

pub proof fn lemma_zip_of_unzip(self)

ensures
self.unzip().0.zip_with(self.unzip().1) =~= self,

Unzipping a sequence of sequences and then zipping the resulting two sequences back together results in the original sequence of sequences.

source§

impl<A> Seq<Seq<A>>

source

pub open spec fn flatten(self) -> Seq<A>

{
    if self.len() == 0 {
        Seq::empty()
    } else {
        self.first().add(self.drop_first().flatten())
    }
}

Flattens a sequence of sequences into a single sequence by concatenating subsequences, starting from the first element.

§Example
proof fn flatten_test() {
   let seq: Seq<Seq<int>> = seq![seq![1, 2, 3], seq![4, 5, 6], seq![7, 8, 9]];
   let flat: Seq<int> = seq.flatten();
   reveal_with_fuel(Seq::<Seq<int>>::flatten, 5); //Needed for Verus to unfold the recursive definition of flatten
   assert(flat =~= seq![1, 2, 3, 4, 5, 6, 7, 8, 9]);
}
source

pub open spec fn flatten_alt(self) -> Seq<A>

{
    if self.len() == 0 {
        Seq::empty()
    } else {
        self.drop_last().flatten_alt().add(self.last())
    }
}

Flattens a sequence of sequences into a single sequence by concatenating subsequences in reverse order, i.e. starting from the last element. This is equivalent to a call to flatten, but with concatenation operation applied along the oppositive associativity for the sake of proof reasoning in that direction.

source

pub proof fn lemma_flatten_one_element(self)

ensures
self.len() == 1 ==> self.flatten() == self.first(),

Flattening a sequence of a sequence x, where x has length 1, results in a sequence equivalent to the single element of x

source

pub proof fn lemma_flatten_length_ge_single_element_length(self, i: int)

requires
0 <= i < self.len(),
ensures
self.flatten_alt().len() >= self[i].len(),

The length of a flattened sequence of sequences x is greater than or equal to any of the lengths of the elements of x.

source

pub proof fn lemma_flatten_length_le_mul(self, j: int)

requires
forall |i: int| 0 <= i < self.len() ==> (#[trigger] self[i]).len() <= j,
ensures
self.flatten_alt().len() <= self.len() * j,

The length of a flattened sequence of sequences x is less than or equal to the length of x multiplied by a number greater than or equal to the length of the longest sequence in x.

source

pub proof fn lemma_flatten_and_flatten_alt_are_equivalent(self)

ensures
self.flatten() =~= self.flatten_alt(),

Flattening sequences of sequences in order (starting from the beginning) and in reverse order (starting from the end) results in the same sequence.

source§

impl Seq<int>

source

pub open spec fn max(self) -> int

recommends
0 < self.len(),
{
    if self.len() == 1 {
        self[0]
    } else if self.len() == 0 {
        0
    } else {
        let later_max = self.drop_first().max();
        if self[0] >= later_max { self[0] } else { later_max }
    }
}

Returns the maximum integer value in a non-empty sequence of integers.

source

pub proof fn max_ensures(self)

ensures
forall |x: int| self.contains(x) ==> x <= self.max(),
forall |i: int| 0 <= i < self.len() ==> self[i] <= self.max(),
self.len() == 0 || self.contains(self.max()),

Proof of correctness and expected properties for max function

source

pub open spec fn min(self) -> int

recommends
0 < self.len(),
{
    if self.len() == 1 {
        self[0]
    } else if self.len() == 0 {
        0
    } else {
        let later_min = self.drop_first().min();
        if self[0] <= later_min { self[0] } else { later_min }
    }
}

Returns the minimum integer value in a non-empty sequence of integers.

source

pub proof fn min_ensures(self)

ensures
forall |x: int| self.contains(x) ==> self.min() <= x,
forall |i: int| 0 <= i < self.len() ==> self.min() <= self[i],
self.len() == 0 || self.contains(self.min()),

Proof of correctness and expected properties for min function

source

pub closed spec fn sort(self) -> Self

source

pub proof fn lemma_sort_ensures(self)

ensures
self.to_multiset() =~= self.sort().to_multiset(),
sorted_by(self.sort(), |x: int, y: int| x <= y),
source

pub proof fn lemma_subrange_max(self, from: int, to: int)

requires
0 <= from < to <= self.len(),
ensures
self.subrange(from, to).max() <= self.max(),

The maximum element in a non-empty sequence is greater than or equal to the maxima of its non-empty subsequences.

source

pub proof fn lemma_subrange_min(self, from: int, to: int)

requires
0 <= from < to <= self.len(),
ensures
self.subrange(from, to).min() >= self.min(),

The minimum element in a non-empty sequence is less than or equal to the minima of its non-empty subsequences.

Auto Trait Implementations§

§

impl<A> Freeze for Seq<A>

§

impl<A> RefUnwindSafe for Seq<A>
where A: RefUnwindSafe,

§

impl<A> Send for Seq<A>
where A: Send,

§

impl<A> Sync for Seq<A>
where A: Sync,

§

impl<A> Unpin for Seq<A>
where A: Unpin,

§

impl<A> UnwindSafe for Seq<A>
where A: UnwindSafe,

Blanket Implementations§

source§

impl<T> Any for T
where T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for T
where T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

source§

impl<T, U> Into<U> for T
where U: From<T>,

source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

source§

type Error = Infallible

The type returned in the event of a conversion error.
source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.