How to define a Sorted Array

[Piyush Bansal <bansal....@xxxxxxxxx>]

Hi,

I am writing tla+ algorithm for Binary Search, I need to define input array 'arr' to sorted. For the verification purpose I did
 

variables arr = [ i \in 1..N |-> i + 1].

Complete pluscal algorithm for BinarySearc.tla is as follows:


---------------------------- MODULE BinarySearch ----------------------------
EXTENDS Naturals, TLC

CONSTANT N      (* Size of arrays *)
CONSTANT MAXINT (* Max integer value *)
(***************************************************************************
--fair algorithm Binsearch {
    variables arr = [ i \in 1..N |-> i + 1];  
              x \in 2..N;          (* Value to find *)
              found = FALSE;
              l = 1;               (* All elements to the left of l are < x *)
              r = N;               (* All elements to the right of r are > x *)
              p = 1;               (* Pivot *)

    (* Main *)
    {     
        print <<arr, x>>;
        
        while ((l <= r) /\ (~ found)) {
            p := (l + r) \div 2;
          
            if (arr[p] = x)
                found := TRUE
            else if (arr[p] < x)e 
                l := p+1
            else (* arr[p] > x *)
                r := p-1
        };
        
        assert( found <=> (\E j \in 1..N : arr[j] = x) )      
    }
}

 ***************************************************************************)
==============================================================================


Is it possible to define array 'arr' as CONSTANT, so that I can input it in the TLC model checker with other constants.


Regards,
Piyush

PS: I tried to (1)attach the BinarySearch.tla and (2) Change the font, but not able to do. Can some guide me for this as well.