binary_search.c 2.97 KB
Newer Older
 Michael Sammler committed Nov 11, 2020 1 2 3 ``````#include #include #include `````` Michael Sammler committed Nov 11, 2020 4 ``````#include `````` Michael Sammler committed Nov 11, 2020 5 6 7 8 9 `````` //@rc::import binary_search_extra from refinedc.examples.binary_search typedef bool (*comp_fn)(void *, void *); `````` Michael Sammler committed Nov 11, 2020 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 &own (ty x) : type) <\$> ls}>>", "{length ls} @ int", "px @ &own<{ty x}>")]] `````` Michael Sammler committed Nov 11, 2020 13 14 15 16 17 18 ``````[[rc::requires("{StronglySorted R ls}", "{Transitive R}")]] [[rc::exists("n : nat")]] [[rc::returns("n @ int")]] [[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 &own (ty x) : type) <\$> ls}>>")]] `````` Michael Sammler committed Nov 11, 2020 19 ``````[[rc::ensures("px @ &own<{ty x}>")]] `````` Michael Sammler committed Nov 11, 2020 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.")]] `````` Michael Sammler committed Nov 11, 2020 23 ``````int binary_search(comp_fn comp, void **xs, int n, void *x) { `````` Michael Sammler committed Nov 11, 2020 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", "r : vr @ int")]] [[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; } `````` Michael Sammler committed Nov 11, 2020 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>", "py @ &own>")]] [[rc::exists("b : bool")]] [[rc::returns("b @ boolean")]] [[rc::ensures("px @ &own>", "py @ &own>", "{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]); }``````