[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# How to define a Sorted Array

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.