Can anyone give me an example of a simple Dafny program, like reading two integers from the keyboard and output their sum?
I want to use Dafny for a programming course at our university, but then I really need I/O. I found 'print' for output, but cannot find anything for input.
There must be some (obvious) way to do this, right?
I searched questions tagged I/O, but did not find anything.
There is not a canonical method for that. Dafny is not really used in that way often. In theory it can be done. There was a similar question here. Reading from (Writing to) files in Dafny
Basically, you create references to external functions that are in the host target language and use those. Note the C sharp fileionative.cs in that repo.
http://dafny.org/dafny/DafnyRef/DafnyRef.html#sec-compilation
I created a console version of the file io answer here and here. You can then run dafny consoleio.dfy consoleionative.cs and it will ask you your name and greet you.
If you want to parse an integer, you would need to either call a native function to do that, or write Dafny code to convert a string to an integer. If you tell me which of these approaches you prefer, I can try to extend the example with them.
