0回答
我正试着在Dafny中做多态性，但我不能让它工作。我找不到任何文档来帮助我解决这个问题。下面是代码： var Leaf?Main() { root.left := new Node();
}Dafny
浏览 0提问于2018-07-17得票数 0
回答已采纳
我不知道如何从dafny程序中获取C#程序。
我已经在Visual Studio Code中下载了dafny，还下载了C#。我在dafny中有一个程序，可以右键单击该程序并选择编译和运行，但我想生成一个如视频(8:46)所示的C#程序：。
浏览 0提问于2019-04-05得票数 4
在exercise_1a中，怎样才能使断言cnt > 0有效？cnt := cnt + 1; assert cnt > 0; // *** invalid ***令人惊讶的是
浏览 2提问于2020-06-19得票数 0
我想询问一个特定的Dafny程序是否验证。Dafny通常用于在visual中以交互方式开发程序。
但是，我需要以一种非交互的方式执行查询。特别是，我需要从python程序中查询Dafny。这个是可能的吗？
浏览 2提问于2016-04-06得票数 0
回答已采纳
1回答
我从阅读文献中了解到，断言语句只有用户才能看到验证者认为某一点的内容。然而，在我自己的经验中，我看到在引理的情况下，断言语句实际上改变了验证者的想法，并允许证明引理。谢谢
浏览 1提问于2020-04-06得票数 0
回答已采纳
1回答
我需要向Dafny函数提供数据并得到它们的输出。为此，我试图创建一个调用Dafny函数的C#程序。为此，我应该
$ csc dafny
浏览 4提问于2021-05-28得票数 0
回答已采纳
1回答
我正在研究几种语言的语言比较，这些语言都考虑到了验证(Whiley，Dafny和Frama-C等)。给出了一个函数的示例，该函数将一个数组的区域复制到另一个数组中，在目标数组中具有不同的位置。我想出的规范在Dafny中是这样的：
method copy( src: array<int>, sStart: nat, dest: array<int>, dStart: nat,
浏览 1提问于2015-12-02得票数 3
回答已采纳
正如在Dafny GitHub上的Wiki中提到的，当Dafny不能证明程序中的断言时，这可能是由于我的程序不正确或Dafny不完整所致。但是我想达夫尼的反例子在我试着理解它之后是假的，所以我仍然不知道我的程序是否正确。
我的问题如下。如果我设法使用另一个Boogie后端(如Corral )来检查使用/print从Dafny编译的Boo
浏览 2提问于2018-09-12得票数 1
回答已采纳
1回答
我正在尝试将一个简单的max示例()编译为java：Additional target code written to max-java/dafnymax element of
浏览 2提问于2021-04-15得票数 1
Dafny中的实数是什么？它们是否表示为IEEE 754-2008浮点数？如果不是，那是什么呢？也就是说，在Dafny中真实类型的规范是什么？
浏览 0提问于2018-01-30得票数 2
回答已采纳
here // assertion DOES NOT verify
} 唯一的区别是stepMany的第二个参数。该断言适用于33个以内的所有参数，而对于超过34个参数则失败。 Dafny可以处理的递归调用有最大数量吗？我已尝试搜索文档，但一无所获。
浏览 12提问于2020-09-01得票数 1
在这种方法中：{Dafny验证OK，test()返回Foo。这在技术上是正确的(它确实返回一个正确类型的值)，但是我期望Dafny抱怨结果没有被该方法本身设置。test()所做的事情与执行以下操作类似：在一个C函数中，它应该返回一个int。是否有一种方法可以让Dafny验证方法结果总是在方法返回之前设置
浏览 5提问于2022-09-06得票数 1
回答已采纳
我想在几个程序中重用相同的Dafny代码。是否可以将一个Dafny文件包含在另一个文件中？手册没有描述任何方法。
浏览 3提问于2014-04-02得票数 3
回答已采纳
1回答
我正在尝试构建并运行一个example program by James Wilcox that combines Dafny code and C# code。我在苹果电脑上使用mono。答案中的build命令对我不起作用： $ dafny fileiotest.dfy fileionative.cs
Dafny program verifier finished如何“添加对程序集的引用”？可以在dafny命令行
浏览 18提问于2020-12-02得票数 0
1回答
new T[|s|]; a := new T[|s|] (i => (s[i]));我想用第三行替换正文中的前两行，以避免类型T中的限定符(0)，但它会引发"index out of range“错误。
浏览 1提问于2018-11-09得票数 1
我想在Dafny中添加一些基本的方便特性，比如在Dafny中定义set union的能力(参见)。但是达夫尼的内部结构似乎没有很好的记录，我也不知道从哪里开始。
我怎样才能添加这样的功能？
浏览 0提问于2018-04-03得票数 0
回答已采纳
我一直在Dafny蹒跚前行，并不了解触发器。也许结果是，我编写的程序似乎给验证器带来了很大的困难。有时我花费大量的时间摆弄我的证明，试图说服Dafny/Boogie它是有效的；当我得到一些工作，有时它是缓慢的验证(这严重降低了我继续的能力)。
很难问一个准确的问题，因为我不知道我不知道的是什么。它们是如何推断出来的？，一旦我理解了所有这些，，我接下来应该读什么？
浏览 28提问于2018-06-04得票数 2
回答已采纳
我知道一个Dafny源文件可以包含在另一个Dafny源文件中，这会导致在验证之前对文件进行文本连接。但是我没有一个清晰的心理模型来描述包含、导入以及何时验证哪些文件之间的关系。
浏览 0提问于2018-01-29得票数 1
云服务器
ICP备案
对象存储
实时音视频
云直播
腾讯云开发者
