0
$\begingroup$

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!

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.