Trying to better understand how to write specifications for automated theorem proving and testing, etc. One seemingly simple example is generating a random number. I would like to know how to specify this behavior, that a function
rand() returns a "random" number. It is straightforward to say it returns a "number", as in Haskell or any functional language you might just do
rand = number -> number, but I would like to go further and somehow include in the specification that this number will be random. At least at a general / high level, I'm wondering how you would even write this out in natural language let alone (the goal) of some structured language or DSL.
My only attempt has been:
rand = number -> number that is random
While it seems like it works in natural language, it really doesn't and is secretly hiding the fact that it is a circular argument. It is essentially this:
rand = number -> random(number)
Which is this:
rand = number -> rand(number)
Basically a "type"
rand vs. a function
rand, but the function produces some object that is typed like the function. Phew, I start to get confused. Wondering what it would look like to write this in a more structured (perhaps even formal) way, though a complete/exact/accurate answer isn't totally necessary.
A related example is rounding a number.
round = number -> number that is rounded
Same situation basically as the random. I don't see how to specify that the output is a rounded number.
The reason for this question is to create a specification for a random number function to prevent regressions and optimize unit tests.