Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364#![cfg_attr(verus_keep_ghost, verifier::exec_allows_no_decreases_clause)]use std::collections::VecDeque;use vstd::pervasive::runtime_assert;#[allow(unused_imports)]use vstd::std_specs::vecdeque::*;use vstd::prelude::*;
verus! {
fn vec_deque_test(){ let mut v1: VecDeque<u32> = VecDeque::<u32>::new(); let mut v2: VecDeque<u32> = VecDeque::<u32>::new(); v1.push_back(3); v1.push_back(4); let front = v1.pop_front(); runtime_assert(front.is_some()); runtime_assert(front.unwrap() == 3); assert(v1@ == seq![4u32]);
v2.push_back(5); assert(v2.len() == 1); v2.push_back(7); assert(v2@.len() == 2); v2.insert(1, 6); assert(v2@ == seq![5u32, 6u32, 7u32]);
v1.append(&mut v2); assert(v2@.len() == 0); assert(v1@.len() == 4); assert(v1@ == seq![4u32, 5u32, 6u32, 7u32]); v1.remove(2); assert(v1@ == seq![4u32, 5u32, 7u32]); let mut x = v1.pop_front(); runtime_assert(x.is_some()); runtime_assert(x.unwrap() == 4); x = v1.pop_front(); runtime_assert(x.is_some()); runtime_assert(x.unwrap() == 5); x = v1.pop_front(); runtime_assert(x.is_some()); runtime_assert(x.unwrap() == 7); x = v1.pop_front(); runtime_assert(x.is_none());
v1.push_back(10); v1.push_back(11); assert(v1@ == seq![10u32, 11u32]);
let mut i: usize = 0; for x in it: v1.iter() invariant i == it.index@, v1@ == seq![10u32, 11u32], { assert(x > 9); assert(x < 12); i = i + 1; }}
} // verus!