Trait vstd::string::StrSliceExecFns

source · 
pub trait StrSliceExecFns {
    // Required methods
    fn unicode_len(&self) -> usize;
    fn get_char(&self, i: usize) -> char;
    fn substring_ascii<'a>(&'a self, from: usize, to: usize) -> &'a str;
    fn substring_char<'a>(&'a self, from: usize, to: usize) -> &'a str;
    fn get_ascii(&self, i: usize) -> u8;
    fn as_bytes_vec(&self) -> Vec<u8>;
    fn from_rust_str<'a>(&'a self) -> &'a str;
    fn into_rust_str<'a>(&'a self) -> &'a str;
}

Required Methods§

source

exec fn unicode_len(&self) -> usize

source

exec fn get_char(&self, i: usize) -> char

source

exec fn substring_ascii<'a>(&'a self, from: usize, to: usize) -> &'a str

source

exec fn substring_char<'a>(&'a self, from: usize, to: usize) -> &'a str

source

exec fn get_ascii(&self, i: usize) -> u8

source

exec fn as_bytes_vec(&self) -> Vec<u8>

source

fn from_rust_str<'a>(&'a self) -> &'a str

👎Deprecated: from_rust_str is no longer necessary
source

fn into_rust_str<'a>(&'a self) -> &'a str

👎Deprecated: into_rust_str is no longer necessary

Implementations on Foreign Types§

source§

impl StrSliceExecFns for str

source§

exec fn unicode_len(&self) -> usize

ensures
l as nat == self@.len(),

The len() function in rust returns the byte length. It is more useful to talk about the length of characters and therefore this function was added. Please note that this function counts the unicode variation selectors as characters. Warning: O(n)

source§

exec fn get_char(&self, i: usize) -> char

requires
i < self@.len(),
ensures
self@.index(i as int) == c,
self.is_ascii() ==> forall |i: int| i < self@.len() ==> (self@.index(i) as nat) < 256,

Warning: O(n) not O(1) due to unicode decoding needed

source§

exec fn substring_ascii<'a>(&'a self, from: usize, to: usize) -> &'a str

requires
self.is_ascii(),
from < self@.len(),
to <= self@.len(),
ensures
ret@ == self@.subrange(from as int, to as int),
ret.is_ascii() == self.is_ascii(),
source§

exec fn substring_char<'a>(&'a self, from: usize, to: usize) -> &'a str

requires
from < self@.len(),
to <= self@.len(),
ensures
ret@ == self@.subrange(from as int, to as int),
ret.is_ascii() == self.is_ascii(),
source§

exec fn get_ascii(&self, i: usize) -> u8

requires
self.is_ascii(),
ensures
self.view().index(i as int) as u8 == b,
source§

exec fn as_bytes_vec(&self) -> Vec<u8>

requires
self.is_ascii(),
ensures
ret.view() == Seq::new(self.view().len(), |i| self.view().index(i) as u8),
source§

exec fn from_rust_str<'a>(&'a self) -> &'a str

👎Deprecated: from_rust_str is no longer necessary
source§

exec fn into_rust_str<'a>(&'a self) -> &'a str

👎Deprecated: into_rust_str is no longer necessary

Implementors§