Trait View

Help

pub trait View {
    type V;

    // Required method
    spec fn view(&self) -> Self::V;
}

Expand description

Types used in executable code can implement View to provide a mathematical abstraction of the type. For example, Vec implements a view method that returns a Seq. For base types like bool and u8, the view V of the type is the type itself. Types only used in ghost code, such as int, nat, and Seq, do not need to implement View.

Required Associated Types§

type V

Required Methods§

spec fn view(&self) -> Self::V

Implementations on Foreign Types§

impl View for bool

type V = bool

fn view(&self) -> bool

impl View for char

type V = char

fn view(&self) -> char

impl View for i8

type V = i8

fn view(&self) -> i8

impl View for i16

type V = i16

fn view(&self) -> i16

impl View for i32

type V = i32

fn view(&self) -> i32

impl View for i64

type V = i64

fn view(&self) -> i64

impl View for i128

type V = i128

fn view(&self) -> i128

impl View for isize

type V = isize

fn view(&self) -> isize

impl View for str

uninterp fn view(&self) -> Seq<char>

type V = Seq<char>

impl View for u8

type V = u8

fn view(&self) -> u8

impl View for u16

type V = u16

fn view(&self) -> u16

impl View for u32

type V = u32

fn view(&self) -> u32

impl View for u64

type V = u64

fn view(&self) -> u64

impl View for u128

type V = u128

fn view(&self) -> u128

impl View for ()

type V = ()

fn view(&self)

impl View for usize

type V = usize

fn view(&self) -> usize

impl View for String

uninterp fn view(&self) -> Seq<char>

type V = Seq<char>

impl View for DefaultHasher

uninterp fn view(&self) -> Seq<Seq<u8>>

type V = Seq<Seq<u8>>

impl<'a> View for Cow<'a, str>

open spec fn view(&self) -> Self::V

{
    match self {
        Cow::Borrowed(borrowed) => borrowed@,
        Cow::Owned(owned) => owned@,
    }
}

type V = Seq<char>

impl<'a> View for Chars<'a>

uninterp fn view(&self) -> (int, Seq<char>)

type V = (int, Seq<char>)

impl<'a, T: 'a> View for Iter<'a, T>

uninterp fn view(self: &Iter<'a, T>) -> (int, Seq<T>)

type V = (int, Seq<T>)

impl<'a, T: View + Clone> View for Cow<'a, [T]>

open spec fn view(&self) -> Self::V

{
    match self {
        Cow::Borrowed(borrowed) => borrowed@,
        Cow::Owned(owned) => owned@,
    }
}

type V = Seq<T>

impl<'a, T: View + Clone> View for Cow<'a, T>

open spec fn view(&self) -> Self::V

{
    match self {
        Cow::Borrowed(borrowed) => borrowed@,
        Cow::Owned(owned) => owned@,
    }
}

type V = <T as View>::V

impl<A0: View> View for (A0,)

type V = (<A0 as View>::V,)

fn view(&self) -> (A0::V,)

impl<A0: View, A1: View> View for (A0, A1)

type V = (<A0 as View>::V, <A1 as View>::V)

fn view(&self) -> (A0::V, A1::V)

impl<A0: View, A1: View, A2: View> View for (A0, A1, A2)

type V = (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V)

fn view(&self) -> (A0::V, A1::V, A2::V)

impl<A0: View, A1: View, A2: View, A3: View> View for (A0, A1, A2, A3)

type V = (<A0 as View>::V, <A1 as View>::V, <A2 as View>::V, <A3 as View>::V)

fn view(&self) -> (A0::V, A1::V, A2::V, A3::V)

impl<A: View + ?Sized> View for &A

open spec fn view(&self) -> A::V

{ (**self).view() }

type V = <A as View>::V

impl<A: View + ?Sized> View for Box<A>

open spec fn view(&self) -> A::V

{ (**self).view() }

type V = <A as View>::V

impl<A: View> View for Rc<A>

open spec fn view(&self) -> A::V

{ (**self).view() }

type V = <A as View>::V

impl<A: View> View for Arc<A>

open spec fn view(&self) -> A::V

{ (**self).view() }

type V = <A as View>::V

impl<Key, S> View for HashSet<Key, S>

uninterp fn view(&self) -> Set<Key>

type V = Set<Key>

impl<Key, Value, S> View for HashMap<Key, Value, S>

uninterp fn view(&self) -> Map<Key, Value>

type V = Map<Key, Value>

impl<T> View for Option<T>

open spec fn view(&self) -> Option<T>

{ *self }

type V = Option<T>

impl<T> View for [T]

uninterp fn view(&self) -> Seq<T>

type V = Seq<T>

impl<T> View for Iter<'_, T>

uninterp fn view(&self) -> (int, Seq<T>)

type V = (int, Seq<T>)

impl<T, A: Allocator> View for VecDeque<T, A>

uninterp fn view(&self) -> Seq<T>

type V = Seq<T>

impl<T, A: Allocator> View for IntoIter<T, A>

uninterp fn view(self: &IntoIter<T, A>) -> (int, Seq<T>)

type V = (int, Seq<T>)

impl<T, A: Allocator> View for Vec<T, A>

uninterp fn view(&self) -> Seq<T>

type V = Seq<T>

impl<T, const N: usize> View for [T; N]

open spec fn view(&self) -> Seq<T>

{ array_view(*self) }

type V = Seq<T>

impl<T: ?Sized> View for *const T

open spec fn view(&self) -> Self::V

{ (*self as *mut T).view() }

type V = PtrData<T>

impl<T: ?Sized> View for *mut T

uninterp fn view(&self) -> Self::V

type V = PtrData<T>

Implementors§

impl View for CheckedU8

The view of an $cty instance is the true value of the instance.

type V = nat

impl View for CheckedU16

The view of an $cty instance is the true value of the instance.

type V = nat

impl View for CheckedU32

The view of an $cty instance is the true value of the instance.

type V = nat

impl View for CheckedU64

The view of an $cty instance is the true value of the instance.

type V = nat

impl View for CheckedU128

The view of an $cty instance is the true value of the instance.

type V = nat

impl View for CheckedUsize

The view of an $cty instance is the true value of the instance.

type V = nat

impl View for StringHashSet

type V = Set<Seq<char>>

impl<'a> View for CharsGhostIterator<'a>

type V = Seq<char>

impl<'a, Key> View for SetIterGhostIterator<'a, Key>

type V = Seq<Key>

impl<'a, Key, Value> View for KeysGhostIterator<'a, Key, Value>

type V = Seq<Key>

impl<'a, Key, Value> View for MapIterGhostIterator<'a, Key, Value>

type V = Seq<(Key, Value)>

impl<'a, Key, Value> View for ValuesGhostIterator<'a, Key, Value>

type V = Seq<Value>

impl<'a, T> View for vstd::std_specs::slice::IterGhostIterator<'a, T>

type V = Seq<T>

impl<'a, T> View for vstd::std_specs::vecdeque::IterGhostIterator<'a, T>

type V = Seq<T>

impl<A: StepSpec + Step> View for RangeGhostIterator<A>

type V = Seq<A>

impl<Key> View for HashSetWithView<Key>
where Key: View + Eq + Hash,

type V = Set<<Key as View>::V>

impl<Key, Value> View for HashMapWithView<Key, Value>
where Key: View + Eq + Hash,

type V = Map<<Key as View>::V, Value>

impl<T> View for PointsTo<T>

type V = PointsToData<T>

impl<T, A: Allocator> View for IntoIterGhostIterator<T, A>

type V = Seq<T>

impl<Value> View for StringHashMap<Value>

type V = Map<Seq<char>, Value>