// ---------------------------------------------------------
// Searching arrays by the binary Algorithm
// ---------------------------------------------------------

//****************************************
//CONSTANTS
//****************************************
val M:ℕ;
val N:ℕ;

//****************************************
//VARIABLES
//****************************************
type index = ℕ[N-1];
type nat  = ℕ[M];
type array = Array[N,nat];
type ret = ℤ[-1,N-1];

//****************************************
//SUPPORTING FUNCTIONS
//****************************************
//i(left:index,right:index)
//  returns the middle index between left and right
fun i(left:index,right:index):ret = left+(right-left)/2;

//****************************************
//SUPPORTING STATEMENTS
//****************************************
//isSorted(a:array,m:index,n:index)
//  states if all elements from m to n are sorted
pred isSorted(a:array,m:index,n:index)
⇔ ∀i:index.m ≤ i ∧ i < n ⇒ a[i] ≤ a[i+1];
 
//****************************************
//CONDITIONS
//****************************************
//pre-Condition
//  (*) a is sorted
pred pre(a:array,x:nat)
⇔ isSorted(a,0,N-1);

//post-Condition
//  (*) result is negative if a does not contain x
//  (*) else its the index of x
pred post(a:array,x:nat,result:ret)
⇔ (result = -1 ⇔ ∀i:index.a[i] ≠ x)
  ∧ (result ≥ 0 ⇒ a[result] = x);
  
//invariant
//  (*) if out is not negative, a[out] = x
//  (*) if out is negative and or left is smaller then
//      right, then x is found
//  (*) else x does not occur left of left or right of right
pred inv(a:array,x:nat,left:ℕ[N-1+1],right:ℤ[-1,N-1],out:ret)
⇔ -1 ≤ right-left
  ∧ (out ≥ 0 ⇒ a[out] = x)
  ∧ (
    out = -1 ∨ left ≤ right
    ⇒ ∀i:index.(0 ≤ i ∧ i < left) ∨ (right < i ∧ i ≤ N-1)
    ⇒ a[i] ≠ x
  );

//pre-Condition for recursive implementation
//  (*) normal pre-condition must hold
//  (*) inveriant must hold
pred preRec(a:array,x:nat,left:ℕ[N-1+1],right:ℤ[-1,N-1])
⇔ pre(a,x) ∧ inv(a,x,left,right,-1);
    
//termination term
//  the indexes left and right are moving closer to each
//  other.
fun termin(left:ℕ[N-1+1],right:ℤ[-1,N-1],out:ret):ℕ[2*N+1]
= if out = -1 then right-left+1 else 0;

//termination term
//  the indexes left and right are moving closer to each 
//  other.
fun terminRec(left:ℕ[N-1+1],right:ℤ[-1,N-1]):ℕ[N]
= right-left+1;

//loop condition
pred loop_cond(left:ℕ[N-1+1],right:ℤ[-1,N-1],out:ret)
⇔ out = -1 ∧ left ≤ right;
  
//****************************************
//VERIFICATION CONDITIONS
//****************************************
//Verification Condition 1
//   given the precondition,
//   (*) invariant holds before the loop started
theorem VC_beginning(a:array,x:nat,out:ret,left:index,right:index)
  requires pre(a,x);
⇔ out = -1 ∧ left = 0 ∧ right = N-1
  ⇒ inv(a,x,left,right,out);

//Verification Condition 2
//  given the precondition,
//  (*) invariant is preserved by every loop iteration
//  (*) termination term decreases at every iteration
theorem VC_iteration(a:array,x:nat,out:ret,left:index,right:index)
  requires pre(a,x);
⇔ inv(a,x,left,right,out) ∧ loop_cond(left,right,out)
  ⇒ if a[i(left,right)] = x then
    inv(a,x,i(left,right)+1,i(left,right),i(left,right))
    ∧ termin(left,i(left,right)-1,i(left,right)) < termin(left,right,out)
  else if a[i(left,right)] > x then
    inv(a,x,left,i(left,right)-1,out)
    ∧ termin(left,i(left,right)-1,out) < termin(left,right,out)
  else
    inv(a,x,i(left,right)+1,right,out)
    ∧ termin(i(left,right)+1,right,out) < termin(left,right,out);

//Verification Condition 3
//  given the precondition,
//  (*) on termination invariant implies postcondition
theorem VC_end(a:array,x:nat,out:ret,left:index,right:index)
  requires pre(a,x);
⇔ inv(a,x,left,right,out) ∧ ¬loop_cond(left,right,out)
  ⇒ post(a,x,out);

//Verification Condition 4
//  given the precondition,
//  (*) termination term is never negative
theorem VC_termination(a:array,x:nat,out:ret,left:index,right:index)
  requires pre(a,x);
⇔ inv(a, x, left,right, out)
  ⇒ termin(left,right,out) ≥ 0;

//Verification Condition 1 for resursive implementation
//   given the precondition,
//   (*) all preconditions of the subfunctions hold.
theorem VC_pre(a:array,x:nat,left:ℕ[N-1+1],right:ℤ[-1,N-1])
  requires preRec(a,x,left,right);
⇔ if left > right ∨ a[i(left,right)] = x then
    true
  else if a[i(left,right)] > x then
    preRec(a,x,left,i(left,right)-1)
  else
    preRec(a,x,i(left,right)+1,right);

//Verification Condition 2
//  given the precondition,
//  (*) the postcondition holds given that all subfunctions can
//      be defined by there postconditions.
theorem VC_post(a:array,x:nat,left:ℕ[N-1+1],right:ℤ[-1,N-1])
  requires preRec(a,x,left,right);
⇔ if left > right then
    post(a,x,-1)
  else if a[i(left,right)] = x then
    post(a,x,i(left,right))
  else if a[i(left,right)] > x then
    ∀b:ret.post(a,x,b) ⇒ post(a,x,b)
  else
    ∀b:ret.post(a,x,b) ⇒ post(a,x,b);

//Verification Condition 3
//  given the precondition,
//  (*) the termination term always positive or zero
//  (*) each recursion reduces the termination term
theorem VC_terminationRec(a:array, x:nat, left:ℕ[N-1+1], right:ℤ[-1,N-1])
  requires preRec(a,x,left,right);
⇔ terminRec(left,right) ≥ 0
  ∧ if left > right ∨ a[i(left,right)] = x then
    true
  else if a[i(left,right)] > x then
    terminRec(left,i(left,right)-1) < terminRec(left,right)
  else
    terminRec(i(left,right)+1,right) < terminRec(left,right);

//****************************************
//  IMPLEMENTATION
//****************************************
proc binarySearch(a:array, x:nat):ret
  requires pre(a,x);
  ensures post(a,x,result);
{
  var out:ret ≔ -1;
  var left:ℕ[N-1+1] ≔ 0;
  var right:ℤ[-1,N-1] ≔ N-1;
  while out = -1 ∧ left ≤ right do
    invariant inv(a,x,left,right,out);
    decreases termin(left,right,out);
  {
    var i:index ≔ left + (right-left)/2;
    if a[i] = x then
      out ≔ i;
    else if a[i] > x then
      right ≔ i-1;
    else
      left ≔ i+1;
  }
  return out;
}

//Resurive implementaion
fun binarySearchRec(a:array, x:nat, left:ℕ[N-1+1], right:ℤ[-1,N-1]):ret
  requires preRec(a,x,left,right);
  ensures post(a,x,result);
  decreases terminRec(left,right);
= if left > right then
    -1
  else if a[i(left,right)] = x then
    i(left,right)
  else if a[i(left,right)] > x then
    binarySearchRec(a,x,left,i(left,right)-1)
  else
    binarySearchRec(a,x,i(left,right)+1,right);
fun binarySearchRecursive(a:array, x:nat):ret
  requires pre(a,x);
  ensures post(a,x,result);
= binarySearchRec(a,x,0,N-1);