提问人：A. Meijster 提问时间：6/30/2023 更新时间：7/4/2023 访问量：61
如何在 Dafny 中进行键盘输入？
How to do keyboard input in Dafny?
问：
谁能给我一个简单的 Dafny 程序的例子，比如从键盘上读取两个整数并输出它们的总和？
我想用 Dafny 来学习我们大学的编程课程，但我真的需要 I/O。 我找到了输出的“打印”，但找不到任何输入。
一定有一些（显而易见的）方法可以做到这一点，对吧？
我搜索了标记为 I/O 的问题，但没有找到任何内容。
答：
0赞
Hath995
7/3/2023
#1
没有规范的方法。Dafny 并不经常以这种方式使用。理论上是可以做到的。这里也有类似的问题。在 Dafny 中读取（写入）文件
基本上，您可以创建对主机目标语言中的外部函数的引用并使用这些函数。请注意该存储库中的 C sharp fileionative.cs。
http://dafny.org/dafny/DafnyRef/DafnyRef.html#sec-compilation
0赞
James Wilcox
7/4/2023
#2
我在这里和这里创建了一个控制台版本的文件io答案。然后你可以跑，它会问你的名字并问候你。dafny consoleio.dfy consoleionative.cs
如果要解析整数，则需要调用本机函数来执行此操作，或者编写 Dafny 代码以将字符串转换为整数。如果你告诉我你更喜欢这些方法中的哪一种，我可以尝试用它们来扩展这个例子。
评论