creusot_contracts::std::collections::hash_set

Function set_produces

Source 
pub fn set_produces<T: DeepModel, I: View<ViewTy = FSet<T::DeepModelTy>>>(
    start: I,
    visited: Seq<T>,
    end: I,
) -> bool
Expand description

logic

pearlite! { start@.len() == visited.len() + end@.len()
    && (forall<x: T::DeepModelTy> start@.contains(x) ==> (exists<x1: T> x1.deep_model() == x && visited.contains(x1)) || end@.contains(x))
    && (forall<x: T> visited.contains(x) ==> start@.contains(x.deep_model()) && !end@.contains(x.deep_model()))
    && (forall<x: T::DeepModelTy> end@.contains(x) ==> start@.contains(x) && !exists<x1: T> x1.deep_model() == x && visited.contains(x1))
    && (forall<i: Int, j: Int>
        0 <= i && i < visited.len() && 0 <= j && j < visited.len()
        && visited[i].deep_model() == visited[j].deep_model()
        ==> i == j)
}