我正在与 Stainless 一起工作, Scala 程序的软件验证程序。我想调试一个示例程序的验证过程。在上一篇文章中，我为 interactive theorem prover 解决了这个集成问题。 .但是现在，我面临两个问题:
显然，验证软件在编译时运行。也就是我在sbt控制台中输入并运行编译命令，然后验证过程似乎就完成了。你可以试试这个 verified example .这种情况对我来说是新的，因为我习惯于在执行时调试程序。
或者，我发现它 was possible (2013) 在 Intellij Idea 中调试插件，released 可能就是这种情况。 (参见 sbt 部分)在 Sbt 上使用不锈钢的插件。
所以澄清一下，我正在寻找一个完整的设置，它允许我从终端/使用某些特定软件调试验证过程，以便我可以遵循不锈钢和我自己的项目的控制流/变量等.
详情
This是不锈钢的当前配置页面。
This我的问题是关于如何在 Intellij Idea 上解决这个问题(我猜更具挑战性)
管道
如果它有助于我离开这里发布的工具的管道(从文档中获取):
其他观察
在 Intellij Idea 中有一个 Unresolved 问题支持。
我必须尝试的另一种方法是 Scala REPL。
最佳答案
我也在寻找这个工具，但我没有找到任何好处。我尝试记录器，对我来说很好。
scala-logger: Simple Scala friendly logging interface.
Logback Project for backend
关于scala - 调试用 Scala 编写的作为 sbt 插件的软件验证程序，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/51227087/