According to this answer I found (https://stackoverflow.com/a/47005291/13083263), we are able to define functions without code. I.e., dafny would simply use the pre and pos conditions for verification.
My question is: how can one do that?
For instance, the following code:
function test(n: nat): (m: nat)
ensures m == n+1
Gets me the error
Function _module._default.test has no body
>Solution :
A function defined without a body can be only be used for verification. For example, it could be called from requires / ensures elements or ghost code.
One option is to define a function with the {: extern} attribute (see here), and then provide a native implementation for it.