Formal Methods and specification of program

I have command $$choose$$ that assign one value from array $${x1...xn}$$ to variable $$x$$.

Every call it assigns the same value to the variable.

I need to create the specification for this program.

I have come up with

Input:$$a\in{N}$$, $$n\in{N}$$

Output: $$x, \exists{i}\in{0...n-1}: x = a[i]$$

However, this says that every call returns one number from the array - not every time the same number of the array. I am trying to think of adjustments so it would work as described, but I am failing to do so.

How could i formally define it such as it would return every time the same number from the array?

Thanks for the help!