scala - 伊莎贝尔(Isabelle)和斯卡拉(Scala)

Closed. This question does not meet Stack Overflow guidelines。它当前不接受答案。












想改善这个问题吗？更新问题，以便将其作为on-topic用于堆栈溢出。

3年前关闭。



Improve this question




我正在寻找创建Eclipse PDE，并且需要与Isabelle进行通信。我确实找到了一些出版物，指出Scala可用于与Isabelle进行通信。

我正在寻找一个示例，该示例如何使用Scala在Isabelle中创建证明。

最佳答案

为了后代，请从an older answer引用我自己:

Isabelle本身是在Standard ML中实现的，但是为了与外部世界通信，它使用了称为PIDE(= Prover IDE)的协议。 PIDE的参考实现与Isabelle捆绑在一起并用Scala编写，因此可以与任何JVM语言一起使用。 PIDE的主要应用程序是Isabelle / jEdit，它使用jEdit编辑器为Isabelle构建IDE，包括标记，连续检查，...

通过重用基础协议，您可以在Isabelle之上实现自己的应用程序。

据我所知，当前最先进的示例是Leon，它是用于Scala程序的自动验证和综合工具包。在内部，它使用libisabelle与Isabelle进行通信。 (完全公开:我是libisabelle的作者。)a paper概述了它的工作原理。

libisabelle本身可以作为一个独立的库使用，其中包括一些基本的文档，使您可以入门。有关更多详细信息，请参见the repository。本质上，它使您能够

从Scala内部管理Isabelle安装(下载，解压缩)

摘要不同的Isabelle版本(当前受支持:2016年和2016-1版本候选)

Isabelle会话的

生命周期管理(构建，启动，停止)

将Isabelle / ML函数视为Scala函数

像Scala中的Isabelle术语语法这样的

好东西(term"$n > 0 --> ($b & ${HOLogic.True})")

没有内置的例程可以建立目标状态并应用一些证明步骤，但是必要的基础结构就在那里。

关于scala - 伊莎贝尔(Isabelle)和斯卡拉(Scala)，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/40848265/