伊莎贝尔和斯卡拉 [英] Isabelle and Scala

问题描述

我正在考虑创建 Eclipse PDE，需要与 Isabelle 进行通信.我确实发现一些出版物指出 Scala 可用于与 Isabelle 进行通信.

I am looking at creating an Eclipse PDE and need to communicate with with Isabelle. I do find some publication stating that Scala can be used to communicate to Isabelle.

我正在寻找如何使用 Scala 在 Isabelle 中创建证明的示例.

I am looking for an example how to use Scala to create proves in Isabelle.

推荐答案

为了后代，引用我自己从 一个较旧的答案:

For posterity, quoting myself from an older answer:

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

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, ...

通过重用底层协议，您可以在 Isabelle 之上实现自己的应用程序.

By reusing the underlying protocol, you can implement your own application on top of Isabelle.

据我所知，目前最先进的例子是 Leon，这是一个自动验证&Scala 程序的综合工具包.在内部，它使用 libisabelle 与 Isabelle 进行通信.(完全披露:我是 libisabelle 的作者.)一篇论文.

As far as I'm aware, the current most advanced example for this is Leon, which is an automated verification & synthesis toolkit for Scala programs. Internally, it uses libisabelle to communicate with Isabelle. (Full disclosure: I'm the author of libisabelle.) An overview of how this works is given in a paper.

libisabelle 本身可以作为一个独立的库使用，包括一些应该允许您开始使用的基本文档.有关更多详细信息，请参阅存储库.从本质上讲，它允许您

libisabelle itself is available as a stand-alone library including some basic documentation that should allow you to get started. See the repository for more details. In essence, it allows you to

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

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

There is no built-in routine to set up a goal state and apply some proof steps, but the necessary infrastructure is all there.

这篇关于伊莎贝尔和斯卡拉的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！