CONST

 ArSize : 4;
 ArSize_1 : ArSize - 1; 
 ArSizeP1 : ArSize + 1;

TYPE

 indT : 0..ArSize_1;
 bloatedindT : -1..ArSize;
 
 dT  : 0..ArSize; 
 arT : Array[indT] of dT;

VAR

 ar : arT;
 
 done : boolean;
 status : boolean;
 
 verifymode : boolean;
 curind : indT;
 itemsought : dT;
 
 low : bloatedindT;
 high : bloatedindT;

STARTSTATE

 verifymode := false;
 done := false;
 status := false; -- false means not found and true means found
 
 curind := 0;
 itemsought := 0;
 
 For i:indT Do
  ar[i] := 0;
 End;

 put "Start state over";
 
ENDSTARTSTATE;

RULE "Rand create 1"
 !verifymode ==>
    curind := (curind+1) % ArSize;
    --put "cur ind is ";
    --put curind;
    --put "\n";
ENDRULE;

RULE "Rand create 1"
 !verifymode ==>
    itemsought := (itemsought+1) % ArSizeP1;
ENDRULE;

RULE "Rand Array Assign"
 !verifymode ==>
    ar[curind] := itemsought;
ENDRULE;

-- mu -b -c binsrch.m
-- make binsrch
-- binsrch -vbfs -b40 -tv -ndl -m200 -p4 -d binsrch-trace

-- tests fine
-- Invariant
--  !(ar[0] = 3 & ar[1] = 1 & ar[2] = 2 & ar[3] = 0)
-- ;

RULE "Switch"
  !verifymode ==>
    verifymode := true;
    low := 0;
    high := ArSize_1;
ENDRULE;  

--- now do the binary search -- possible to have any array and any itemsought now ---

RULE "Done with success"
  verifymode 
  & !done
  & 
    ar[ (low+high)/2 ] = itemsought ==>
       done := true;
       status := true;
ENDRULE;

RULE "Switch high ptr"
  verifymode 
  & !done
  &
    itemsought < ar[ (low+high)/2 ] ==>
      high := (low+high)/2 - 1;
ENDRULE;

RULE "Switch low ptr"
  verifymode 
  & !done
  &
    itemsought > ar[ (low+high)/2 ] ==>
      low := (low+high)/2 + 1;
ENDRULE;

RULE "Done with failure"
  verifymode 
  & !done
  & low > high ==>
       done := true;
       status := false; -- redundant, but let's do it
ENDRULE;

INVARIANT
  (done & status -> ar[ (low+high)/2 ] = itemsought)
  &
  (done & !status -> !(Exists i:indT Do  ar[i] = itemsought Endexists))
;