Input/Output

Jan 15, 2015 at 9:42 PM
Edited Jan 15, 2015 at 11:43 PM
I'm appalled that I can't find anything written or discussed about this subject. How on earth is a program supposed to do anything useful without any interaction with the os other than "print"? All code examples are classes or methods out of context. I can't even find dafny and stdin mentioned anywhere together and Main() does not take arguments. Nor can I find any way to connect any external library that might allow for os interaction. How can I do either of those things?
Jan 16, 2015 at 10:25 AM
The main useful thing I have done with Dafny is prove that particular Programs have particular properties. i.e. create Dafny models of other systems and then prove things about them. So I have never tried to do any I/O. But, if your Dafny program does not have a main method, and you ask Dafny to compile it, it will produce a .net DLL. This should allow you to at least call Dafny procedures from .net (say C#) programs. I suppose that it might also be possible (using the DLL) to extend a Dafny class from C# code and override some of its methods to do I/O. I have not attempted this and do not know if it is actually possible.
Marked as answer by Deagels on 1/16/2015 at 9:25 AM