binary_search.c 2.97 KB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
1 2 3
#include <stddef.h>
#include <stdbool.h>
#include <refinedc.h>
4
#include <alloc.h>
Michael Sammler's avatar
Michael Sammler committed
5 6 7 8 9

//@rc::import binary_search_extra from refinedc.examples.binary_search

typedef bool (*comp_fn)(void *, void *);

10 11 12
[[rc::parameters("R : {Z → Z → Prop}", "ls : {list Z}", "x : Z", "p : loc", "ty : {Z → type}", "px : loc")]]
[[rc::args("function_ptr<{fn(∀ (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) → ∃ (b) : (bool), b @ boolean bool_it; px ◁ₗ ty x ∗ py ◁ₗ ty y ∗ ⌜b ↔ R x y⌝}>",
      "p @ &own<array<LPtr, {(fun x => &own (ty x) : type) <$> ls}>>", "{length ls} @ int<i32>", "px @ &own<{ty x}>")]]
Michael Sammler's avatar
Michael Sammler committed
13 14 15 16 17 18
[[rc::requires("{StronglySorted R ls}", "{Transitive R}")]]
[[rc::exists("n : nat")]]
[[rc::returns("n @ int<i32>")]]
[[rc::ensures("{∀ i y, (i < n)%nat → ls !! i = Some y → R y x}",
              "{∀ i y, (n ≤ i)%nat → ls !! i = Some y → ¬ R y x}")]]
[[rc::ensures("p @ &own<array<LPtr, {(fun x => &own (ty x) : type) <$> ls}>>")]]
19
[[rc::ensures("px @ &own<{ty x}>")]]
Michael Sammler's avatar
Michael Sammler committed
20 21 22
[[rc::tactics("all: try by [revert select (∀ i j, _ → _ → ¬ R _ _); apply; [| done];solve_goal].")]]
[[rc::tactics("all: try by apply: (binary_search_cond_1 y); solve_goal.")]]
[[rc::tactics("all: try by apply: (binary_search_cond_2 y); solve_goal.")]]
23
int binary_search(comp_fn comp, void **xs, int n, void *x) {
Michael Sammler's avatar
Michael Sammler committed
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
  int l = 0, r = n;
  [[rc::exists("vl : nat", "vr : nat")]]
  [[rc::inv_vars("l : vl @ int<i32>", "r : vr @ int<i32>")]]
  [[rc::constraints("{vl <= vr}", "{vr <= length ls}")]]
  [[rc::constraints("{∀ i y, (i < vl)%nat → ls !! i = Some y → R y x}",
                    "{∀ i y, (vr ≤ i)%nat → ls !! i = Some y → ¬ R y x}")]]
  while(l < r) {
    int k = l + (r - l) / 2;
    if (comp(xs[k], x)) {
      l = k + 1;
      } else {
      r = k;
    }
  }
  return l;
}
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77

[[rc::parameters("x : Z", "y : Z", "px : loc", "py : loc")]]
[[rc::args("px @ &own<x @ int<size_t>>", "py @ &own<y @ int<size_t>>")]]
[[rc::exists("b : bool")]]
[[rc::returns("b @ boolean<bool_it>")]]
[[rc::ensures("px @ &own<x @ int<size_t>>", "py @ &own<y @ int<size_t>>", "{b ↔ Z.le x y}")]]
bool compare_int(void *x, void *y) {
  size_t *xi = x, *yi = y;
  return *xi <= *yi;
}

[[rc::requires("[alloc_initialized]")]]
[[rc::tactics("all: try by repeat constructor; lia.")]]
[[rc::tactics("all: try by apply _.")]]
[[rc::tactics("all: try by do 4 (destruct x'; [ naive_solver lia |]); exfalso; apply: (H0 3%nat) => //; lia.")]]
void test() {
  size_t *ptrs[5];
  ptrs[0] = alloc(sizeof(size_t));
  ptrs[1] = alloc(sizeof(size_t));
  ptrs[2] = alloc(sizeof(size_t));
  ptrs[3] = alloc(sizeof(size_t));
  ptrs[4] = alloc(sizeof(size_t));
  *ptrs[0] = 0;
  *ptrs[1] = 1;
  *ptrs[2] = 2;
  *ptrs[3] = 3;
  *ptrs[4] = 4;

  size_t needle = 2;
  int res = binary_search(compare_int, (void **)ptrs, 5, &needle);
  assert(res == 3);

  free(sizeof(size_t), ptrs[0]);
  free(sizeof(size_t), ptrs[1]);
  free(sizeof(size_t), ptrs[2]);
  free(sizeof(size_t), ptrs[3]);
  free(sizeof(size_t), ptrs[4]);
}