SHARE
TWEET

Untitled

a guest Apr 20th, 2019 90 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. #![allow(dead_code)]
  2.  
  3. extern crate prusti_contracts;
  4.  
  5. pub struct VecWrapperI32{
  6.     v: Vec<i32>
  7. }
  8.  
  9. impl VecWrapperI32 {
  10.  
  11.     #[trusted]
  12.     #[pure]
  13.     #[ensures="result >= 0"]
  14.  
  15.     pub fn len(&self) -> usize {
  16.         self.v.len()
  17.     }
  18.  
  19.     #[trusted]
  20.     #[pure]
  21.     #[requires="0 <= index && index < self.len()"]
  22.  
  23.     pub fn lookup(&self, index: usize) -> i32 {
  24.         self.v[index]
  25.     }
  26.  
  27.     #[trusted]
  28.     #[requires="0 <= index && index < self.len()"]
  29.     #[ensures="self.lookup(index) == *result"]
  30.  
  31.     pub fn index(&self, index: usize) -> &i32 {
  32.         &self.v[index]
  33.     }
  34. }
  35.  
  36. pub enum UsizeOption {
  37.     Some(usize),
  38.     None,
  39. }
  40.  
  41. impl UsizeOption {
  42.     #[pure]
  43.  
  44.     pub fn is_some(&self) -> bool {
  45.         match self {
  46.             UsizeOption::Some(_) => true,
  47.             UsizeOption::None => false,
  48.         }
  49.     }
  50.  
  51.     #[pure]
  52.  
  53.     pub fn is_none(&self) -> bool {
  54.         match self {
  55.             UsizeOption::Some(_) => false,
  56.             UsizeOption::None => true,
  57.         }
  58.     }
  59. }
  60.  
  61. pub enum Ordering {
  62.     Less,
  63.     Equal,
  64.     Greater,
  65. }
  66. use self::Ordering::*;
  67.  
  68. #[ensures="(match result {
  69.             Equal => *a == *b,
  70.             Less => *a < *b,
  71.             Greater => *a > *b,
  72.         })"]
  73.  
  74. fn cmp(a: &i32, b: &i32) -> Ordering {
  75.     if *a == *b { Equal }
  76.     else if *a < *b { Less }
  77.     else { Greater }
  78. }
  79.  
  80. #[requires="forall k1: usize, k2: usize :: (0 <= k1 && k1 < k2 && k2 < arr.len()) ==>
  81.              arr.lookup(k1) <= arr.lookup(k2)"]
  82. #[ensures="result.is_none() ==>
  83.             (forall k: usize :: (0 <= k && k < arr.len()) ==> *elem != arr.lookup(k))"]
  84. #[ensures="match result {
  85.                 UsizeOption::Some(index) => (
  86.                     0 <= index && index < arr.len() &&
  87.                     arr.lookup(index) == *elem
  88.                 ),
  89.                 UsizeOption::None => true,
  90.             }"]
  91. fn binary_search(arr: &VecWrapperI32, elem: &i32) -> UsizeOption {
  92.     let mut size = arr.len();
  93.     let mut base = 0;
  94.     let mut result = UsizeOption::None;
  95.     let mut continue_loop = size > 0;
  96.  
  97.     #[invariant="0 <= base"]
  98.     #[invariant="0 <= size"]
  99.     #[invariant="continue_loop == (size > 0 && result.is_none())"]
  100.     #[invariant="base + size <= arr.len()"]
  101.     #[invariant="forall k1: usize, k2: usize :: (0 <= k1 && k1 < k2 && k2 < arr.len()) ==>
  102.             arr.lookup(k1) <= arr.lookup(k2)"]
  103.     #[invariant="forall k: usize:: (0 <= k && k < base) ==> arr.lookup(k) < *elem"]
  104.     #[invariant="result.is_none() ==>
  105.                 (forall k: usize :: (base + size <= k && k < arr.len()) ==> *elem != arr.lookup(k))"]
  106.     #[invariant="match result {
  107.                     UsizeOption::Some(index) => (
  108.                         0 <= index && index < arr.len() &&
  109.                         arr.lookup(index) == *elem
  110.                     ),
  111.                     UsizeOption::None => true,
  112.                 }"]
  113.  
  114.     while continue_loop {
  115.         let half = size / 2;
  116.         let mid = base + half;
  117.         let mid_element = arr.index(mid);
  118.         let cmp_result = cmp(mid_element, elem);
  119.         base = match cmp_result {
  120.             Less    => {
  121.                 mid
  122.             },
  123.             Greater => {
  124.                 base
  125.             },
  126.             Equal   => {
  127.                 result = UsizeOption::Some(mid);
  128.                 base   // Just return anything because we are finished.
  129.             }
  130.         };
  131.         size -= half;
  132.         continue_loop = size > 0 && result.is_none();
  133.     }
  134.     result
  135. }
  136.  
  137. fn main() {}
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!
 
Top