Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637// ANCHOR: exampleuse vstd::contrib::exec_spec::*;use vstd::prelude::*;
verus! {
exec_spec_verified! {
struct Point { x: i64, y: i64,}
spec fn on_line(points: Seq<Point>) -> bool { forall |i: usize| #![auto] 0 <= i < points.len() ==> points[i as int].y == points[i as int].x}
}
} // verus!// ANCHOR_END: example// ANCHOR: checkverus! {
fn main() { let p1 = ExecPoint { x: 1, y: 1 }; let p2 = ExecPoint { x: 2, y: 2 }; let points = vec![p1, p2]; assert(on_line(points.deep_view())); let b = exec_on_line(points.as_slice()); assert(b);}
} // verus!// ANCHOR_END: check