Skip to content

Commit 182ca6c

Browse files
vakarasvakaras
committed
Add original Binary Search Rosetta examples from the artefact.
1 parent 202ca0e commit 182ca6c

2 files changed

Lines changed: 380 additions & 0 deletions

File tree

‎prusti-tests/tests_old/verify_overflow/pass/rosetta/artefact_Binary_search_shared.rs‎

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,169 @@
1+
//! An adaptation of the example from
2+
//! https://rosettacode.org/wiki/Binary_search#Rust
3+
//!
4+
//! The original example:
5+
//! ```rust
6+
//! use std::cmp::Ordering::*;
7+
//! fn binary_search<T: Ord>(arr: &[T], elem: &T) -> Option<usize>
8+
//! {
9+
//! let mut size = arr.len();
10+
//! let mut base = 0;
11+
//!
12+
//! while size > 0 {
13+
//! size /= 2;
14+
//! let mid = base + size;
15+
//! base = match arr[mid].cmp(elem) {
16+
//! Less => mid,
17+
//! Greater => base,
18+
//! Equal => return Some(mid)
19+
//! };
20+
//! }
21+
//!
22+
//! None
23+
//! }
24+
//! ```
25+
//!
26+
//! Changes:
27+
//!
28+
//! + Wrapped built-in types and functions.
29+
//! + Replaced a slice with a reference into a vector.
30+
//! + Change the loop into the supported shape.
31+
//! + Remove the return statement.
32+
//!
33+
//! Verified properties:
34+
//!
35+
//! + Absence of panics.
36+
//! + Absence of overflows.
37+
//!
38+
//! The original example contains a bug, which can be showed by using
39+
//! the following counter-example:
40+
//!
41+
//! ```rust
42+
//! fn main() {
43+
//! let v = vec![0, 1, 2, 3, 4, 5, 6];
44+
//! println!("{:?}", binary_search(&v, &6));
45+
//! }
46+
//! ```
47+
//!
48+
//! This program should print `Some(6)`, but it prints None. The fixed
49+
//! version would be:
50+
//!
51+
//! ```rust
52+
//! use std::cmp::Ordering::*;
53+
//! fn binary_search<T: Ord>(arr: &[T], elem: &T) -> Option<usize>
54+
//! {
55+
//! let mut size = arr.len();
56+
//! let mut base = 0;
57+
//!
58+
//! while size > 0 {
59+
//! let half = size / 2;
60+
//! let mid = base + half;
61+
//! base = match arr[mid].cmp(elem) {
62+
//! Less => mid,
63+
//! Greater => base,
64+
//! Equal => return Some(mid)
65+
//! };
66+
//! size -= half;
67+
//! }
68+
//!
69+
//! None
70+
//! }
71+
//! ```
72+
//!
73+
//! This file contains a verified version of it.
74+
75+
#![allow(dead_code)]
76+
extern crate prusti_contracts;
77+
78+
pub struct VecWrapper<T>{
79+
v: Vec<T>
80+
}
81+
82+
impl<T> VecWrapper<T> {
83+
84+
#[trusted]
85+
#[pure]
86+
pub fn len(&self) -> usize {
87+
self.v.len()
88+
}
89+
90+
#[trusted]
91+
#[requires="0 <= index && index < self.len()"]
92+
pub fn index(&self, index: usize) -> &T {
93+
&self.v[index]
94+
}
95+
}
96+
97+
pub enum UsizeOption {
98+
Some(usize),
99+
None,
100+
}
101+
102+
impl UsizeOption {
103+
#[pure]
104+
pub fn is_some(&self) -> bool {
105+
match self {
106+
UsizeOption::Some(_) => true,
107+
UsizeOption::None => false,
108+
}
109+
}
110+
#[pure]
111+
pub fn is_none(&self) -> bool {
112+
match self {
113+
UsizeOption::Some(_) => false,
114+
UsizeOption::None => true,
115+
}
116+
}
117+
}
118+
119+
pub enum Ordering {
120+
Less,
121+
Equal,
122+
Greater,
123+
}
124+
125+
use self::Ordering::*;
126+
127+
#[trusted]
128+
fn cmp<T>(_a: &T, _b: &T) -> Ordering {
129+
unimplemented!();
130+
}
131+
132+
fn binary_search<T: Ord>(arr: &VecWrapper<T>, elem: &T) -> UsizeOption {
133+
let mut size = arr.len();
134+
let mut base = 0;
135+
136+
let mut result = UsizeOption::None;
137+
let mut continue_loop = size > 0;
138+
139+
140+
#[invariant="continue_loop == (size > 0 && result.is_none())"]
141+
#[invariant="base + size <= arr.len()"]
142+
while continue_loop {
143+
let half = size / 2;
144+
let mid = base + half;
145+
146+
let mid_element = arr.index(mid);
147+
let cmp_result = cmp(mid_element, elem);
148+
base = match cmp_result {
149+
Less => {
150+
mid
151+
},
152+
Greater => {
153+
base
154+
},
155+
// Equal
156+
_ => {
157+
result = UsizeOption::Some(mid);
158+
base // Just return anything because we are finished.
159+
}
160+
};
161+
162+
size -= half;
163+
continue_loop = size > 0 && result.is_none();
164+
}
165+
166+
result
167+
}
168+
169+
fn main() {}

‎prusti-tests/tests_old/verify_overflow/pass/rosetta/artefact_Binary_search_shared_monomorphised.rs‎

Lines changed: 211 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,211 @@
1+
//! An adaptation of the example from
2+
//! https://rosettacode.org/wiki/Binary_search#Rust
3+
//!
4+
//! The original example:
5+
//! ```rust
6+
//! use std::cmp::Ordering::*;
7+
//! fn binary_search<T: Ord>(arr: &[T], elem: &T) -> Option<usize>
8+
//! {
9+
//! let mut size = arr.len();
10+
//! let mut base = 0;
11+
//!
12+
//! while size > 0 {
13+
//! size /= 2;
14+
//! let mid = base + size;
15+
//! base = match arr[mid].cmp(elem) {
16+
//! Less => mid,
17+
//! Greater => base,
18+
//! Equal => return Some(mid)
19+
//! };
20+
//! }
21+
//!
22+
//! None
23+
//! }
24+
//! ```
25+
//!
26+
//! Changes:
27+
//!
28+
//! + Wrapped built-in types and functions.
29+
//! + Add additional functions for capturing functional specification.
30+
//! + Replaced a slice with a reference into a vector.
31+
//! + Changed the loop into the supported shape.
32+
//! + Removed the return statement.
33+
//! + Monomorphised types.
34+
//!
35+
//! Verified properties:
36+
//!
37+
//! + Absence of panics.
38+
//! + Absence of overflows.
39+
//! + If the result is `None`, then the input vector did not contain the
40+
//! element.
41+
//! + If the result is `Some(index)` then the `arr[index] == elem`.
42+
//!
43+
//! The original example contains a bug, which can be showed by using
44+
//! the following counter-example:
45+
//!
46+
//! ```rust
47+
//! fn main() {
48+
//! let v = vec![0, 1, 2, 3, 4, 5, 6];
49+
//! println!("{:?}", binary_search(&v, &6));
50+
//! }
51+
//! ```
52+
//!
53+
//! This program should print `Some(6)`, but it prints None. The fixed
54+
//! version would be:
55+
//!
56+
//! ```rust
57+
//! use std::cmp::Ordering::*;
58+
//! fn binary_search<T: Ord>(arr: &[T], elem: &T) -> Option<usize>
59+
//! {
60+
//! let mut size = arr.len();
61+
//! let mut base = 0;
62+
//!
63+
//! while size > 0 {
64+
//! let half = size / 2;
65+
//! let mid = base + half;
66+
//! base = match arr[mid].cmp(elem) {
67+
//! Less => mid,
68+
//! Greater => base,
69+
//! Equal => return Some(mid)
70+
//! };
71+
//! size -= half;
72+
//! }
73+
//!
74+
//! None
75+
//! }
76+
//! ```
77+
//!
78+
//! This file contains a verified version of it.
79+
80+
#![allow(dead_code)]
81+
extern crate prusti_contracts;
82+
83+
pub struct VecWrapperI32{
84+
v: Vec<i32>
85+
}
86+
87+
impl VecWrapperI32 {
88+
#[trusted]
89+
#[pure]
90+
pub fn len(&self) -> usize {
91+
self.v.len()
92+
}
93+
94+
#[trusted]
95+
#[pure]
96+
#[requires="0 <= index && index < self.len()"]
97+
pub fn lookup(&self, index: usize) -> i32 {
98+
self.v[index]
99+
}
100+
101+
#[trusted]
102+
#[requires="0 <= index && index < self.len()"]
103+
#[ensures="self.lookup(index) == *result"]
104+
pub fn index(&self, index: usize) -> &i32 {
105+
&self.v[index]
106+
}
107+
}
108+
109+
pub enum UsizeOption {
110+
Some(usize),
111+
None,
112+
}
113+
114+
impl UsizeOption {
115+
#[pure]
116+
pub fn is_some(&self) -> bool {
117+
match self {
118+
UsizeOption::Some(_) => true,
119+
UsizeOption::None => false,
120+
}
121+
}
122+
#[pure]
123+
pub fn is_none(&self) -> bool {
124+
match self {
125+
UsizeOption::Some(_) => false,
126+
UsizeOption::None => true,
127+
}
128+
}
129+
}
130+
131+
pub enum Ordering {
132+
Less,
133+
Equal,
134+
Greater,
135+
}
136+
137+
use self::Ordering::*;
138+
139+
#[ensures="(match result {
140+
Equal => *a == *b,
141+
Less => *a < *b,
142+
Greater => *a > *b,
143+
})"]
144+
fn cmp(a: &i32, b: &i32) -> Ordering {
145+
if *a == *b { Equal }
146+
else if *a < *b { Less }
147+
else { Greater }
148+
}
149+
150+
151+
#[requires="forall k1: usize, k2: usize :: (0 <= k1 && k1 < k2 && k2 < arr.len()) ==>
152+
arr.lookup(k1) <= arr.lookup(k2)"]
153+
#[ensures="result.is_none() ==>
154+
(forall k: usize :: (0 <= k && k < arr.len()) ==> *elem != arr.lookup(k))"]
155+
#[ensures="match result {
156+
UsizeOption::Some(index) => (
157+
0 <= index && index < arr.len() &&
158+
arr.lookup(index) == *elem
159+
),
160+
UsizeOption::None => true,
161+
}"]
162+
fn binary_search(arr: &VecWrapperI32, elem: &i32) -> UsizeOption {
163+
let mut size = arr.len();
164+
let mut base = 0;
165+
166+
let mut result = UsizeOption::None;
167+
let mut continue_loop = size > 0;
168+
169+
170+
#[invariant="continue_loop == (size > 0 && result.is_none())"]
171+
#[invariant="base + size <= arr.len()"]
172+
#[invariant="forall k1: usize, k2: usize :: (0 <= k1 && k1 < k2 && k2 < arr.len()) ==>
173+
arr.lookup(k1) <= arr.lookup(k2)"]
174+
#[invariant="forall k: usize:: (0 <= k && k < base) ==> arr.lookup(k) < *elem"]
175+
#[invariant="result.is_none() ==>
176+
(forall k: usize :: (base + size <= k && k < arr.len()) ==> *elem != arr.lookup(k))"]
177+
#[invariant="match result {
178+
UsizeOption::Some(index) => (
179+
0 <= index && index < arr.len() &&
180+
arr.lookup(index) == *elem
181+
),
182+
UsizeOption::None => true,
183+
}"]
184+
while continue_loop {
185+
let half = size / 2;
186+
let mid = base + half;
187+
188+
let mid_element = arr.index(mid);
189+
let cmp_result = cmp(mid_element, elem);
190+
base = match cmp_result {
191+
Less => {
192+
mid
193+
},
194+
Greater => {
195+
base
196+
},
197+
// Equal
198+
_ => {
199+
result = UsizeOption::Some(mid);
200+
base // Just return anything because we are finished.
201+
}
202+
};
203+
204+
size -= half;
205+
continue_loop = size > 0 && result.is_none();
206+
}
207+
208+
result
209+
}
210+
211+
fn main() {}

0 commit comments

Comments
 (0)