scala - 伊莎贝尔和斯卡拉

Question

<分区>

Answer 1

为了后代，引用我自己的话 an older answer :

Isabelle itself is implemented in Standard ML, but for communicating with the external world, it uses a protocol called PIDE (= Prover IDE). The reference implementation of PIDE is bundled with Isabelle and written in Scala, so it can be used with any JVM language. The primary application of PIDE is Isabelle/jEdit, which uses the jEdit editor to build an IDE for Isabelle, including markup, continuous checking, ...

通过重用底层协议(protocol)，您可以在 Isabelle 之上实现您自己的应用。

据我所知，当前最高级的示例是 Leon ，这是一个用于 Scala 程序的自动验证和综合工具包。在内部，它使用 libisabelle与伊莎贝尔交流。 (完全披露:我是 libisabelle 的作者。) a paper 中给出了其工作原理的概述。 .

libisabelle 本身可以作为一个独立的库使用，包括一些可以让您入门的基本文档。参见 the repository更多细节。本质上，它允许您

• 在 Scala 中管理 Isabelle 安装(下载、解压)
• 不同 Isabelle 版本的摘要(目前支持:2016 和 2016-1 候选版本)
• Isabelle session 的生命周期管理(构建、启动、停止)
• 将 Isabelle/ML 函数视为 Scala 函数
• 像 Scala 中的 Isabelle 术语语法这样的好东西 (term"$n > 0 --> ($b & ${HOLogic.True})")

没有内置例程来设置目标状态和应用一些证明步骤，但必要的基础设施都在那里。