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!


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.