Trait vstd::string::StrSliceExecFns

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

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>

Implementations on Foreign Types§

source§

impl StrSliceExecFns for str

source§

exec fn unicode_len(&self) -> l : usize

ensures
l as nat == @.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) -> c : char

requires
i < @.len(),
ensures
@.index(i as int) == c,
self.is_ascii() ==> forall |i: int| i < @.len() ==> (@.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) -> ret : &'a str

requires
self.is_ascii(),
from < @.len(),
to <= @.len(),
ensures
@ == @.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) -> ret : &'a str

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

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

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

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

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

Implementors§