小智 5
澄清是好的，但我不喜欢做必要的握手。
我在下面的第一个答案主要是基于你的短语“一种全新的语法”，我认为这是对这样一个问题的一半答案：
假设，假设我需要非常接近 J 语法的语法。关于 Isabelle/HOL，这需要什么？
我的答案：
Pure为起点。请看下面我的第一个回答。Isabelle/HOL 中的语法定制使我们都成为潜在的真正艺术家。
有一些高级方法可以利用定义语法的力量，例如parse_translation，使用 Isabelle/ML，但我不使用高级方法。我使用一些基本的关键词来定义的语法：notation，no_notation，syntax，和translations，随着abbreviation时任我希望重新排列的功能的输入参数，或者我不想把事情弄糟符号为标准HOL功能。
notation, no_notation, 容易的我用no_notation的不多，但你的武器库中需要它。例如，请参阅我可以重载分配给 bool 和 list 的运算符的符号吗？.
使用notation很容易，只要你看到几个例子。
对于中缀运算符 ，以下plus :: 'a => 'a => 'a是一些示例：
notation plus (infixl "[+]" 65)
notation (input) plus (infixl "[+]" 65)
notation (output) plus (infixl "[+]" 65)
在那个例子中，我进入了可能弄乱 for 符号的领域plus，它是标准 HOL 类型类的运算符。
上面不会弄乱输出显示的行是使用(input).
对于notation，要查找示例，请在 THY 文件或src/HOL文件夹中执行 grep ，因为这里的变体太多，无法为您提供大量示例。
abbreviation，而不是把其他事情搞砸假设我想要一个非常紧密的标准even谓词绑定。我可以做这样的事情：
notation (input) even ("even _" [1000] 1000)
notation (output) even ("even _" [1000] 999)
我说“可以”，因为我不知道这会如何弄乱 的标准函数应用程序even，所以我不想这样做。
为什么999？这只是来自反复试验和经验，我知道仅下一行就搞砸了declare[[show_brackets]]：
notation even ("even _" [1000] 1000)
这就是定义语法的方式。这是反复试验的组合，找到用作模板的示例，体验，然后注意到你把事情搞砸了。
我忘记了所有abbreviation帮助我解决的事情。的创新使用abbreviation可以使您不必使用更复杂的方法。
您可以使用它来重新排列参数，用于某些符号目的：
abbreviation list_foo :: "'a list => 'a => 'a list" where
"list_foo xs x == x # xs"
notation
list_foo ("_ +#+ _" [65, 65] 64)
该示例是几个示例中的一个示例。我只是想举一个简单的例子，我有类似的东西(infixl "_ +#+ _" [65, 65] 64)。我定义符号的方式没有太多变化，所以我必须找到一个例子Set.thy来告诉我我需要去掉infixl，因为我想[65, 65] 64用作如何定义语法的变化。
我的优先级是否正确[65, 65] 64？我不知道。这只是一个简单的例子。
syntax 和 translations你必须在你的武器库中拥有它，但它会给你带来很多耗时的悲伤。做 grep 并找到例子。试试这个和那个。当您偶然发现一些有用的东西，并且您认为需要它时，请将其保存在某个地方。如果你不这样做，并且你做了一个小小的改变，破坏了你拥有的东西，而且你没有保存你原来的东西，那么你会后悔不得不花费大量时间试图恢复原来的东西。
在伊萨尔参考手册，ISAR-ref.pdf＃175有一点信息。此外，您可以notation在该 PDF 中查找使用。
在您的评论中，您说：
我已经有了想要实现的“编程逻辑” （cs.utoronto.ca/~hehner/FMSD），而 J 是一种特别适合形式证明的语言。我只是想弄清楚如何重用 Isabelle 的逻辑基础结构，而不是自己编写。
对于这样的问题，即使是对冲的，任何人的简短、不安全的回答是这样的：
在 Isabelle/HOL 中，您很可能无法对 J 进行任何操作。
一个更安全、简短的答案是这样的：
最有可能的是，在 Isabelle/HOL 中尝试用 J 做你想做的事情时，你会遇到重大问题。
这些是简短而快速的答案。如果它实际上试图解决为什么这样的问题，那么对这样的问题的答案怎么可能简短？
它最终是一个“我所知道的一切”的答案，因为很多时候并不是它不能完成，而是合适的人群，在足够长的时间内，在合适的技术下，没有还是做到了。
我下面的标题成为我的观点。我尝试相当快地完成其余部分，但仍然记录事情。
Isabelle/HOL 发展到今天的样子，从Robin Milner开始，我归类为火箭科学逻辑。
从我所有的搜索和所有的聆听来看，在证明助手可用于正式验证以任何 ole 命令式编程语言编写的任何 ole 程序之前，似乎还有很多火箭科学逻辑需要开发。
你有一个逻辑，HOL，但你暗示你将实施类似于很多人想要的东西，并且已经想要了很长时间。
下面的内容是为了支持我在这里所说的。
会有传统的算法分析形式，例如Cormen 和 Leiserson 的《算法导论》，第 3 版。
我将在 Isabelle/HOL机械化证明和正式验证程序中调用程序证明。我还认为某些铅笔和纸的校样是正式的。
那么，在传统的非机械化证明中，是的，我猜 J 是一种非常适合形式证明的语言，我这么说是因为您已经告诉过我了。但是，大型流行的编程语言，尤其是 C++ 和 Java，都有关于形式化算法分析主题的教科书。因此，使用传统的、非机械化的证明，它们也必须是可以推理的。
不，它不是一种非常适合正式、机械化证明的语言。它使用（比使用更好的词？）命令式编程，并且它似乎是面向对象的。
在很大程度上，我只是在重复我读过的其他人说的话。我将开始发表声明作为我个人的结论。这将使事情变得更短。
函数式编程语言适用于形式证明。传统编程涉及变异变量，据说这会增加证明的难度。
我在邮件列表中寻找关于面向对象语言的声明，但是如果你听，人们会说他们已经做了这个或那个特别的事情，但它从来都不是这样的，“这是一个完整的开发和形式化，很容易让你验证用通用编程语言 X 编写的程序”。
除其他外，形式证明是关于一组被强制执行的公理，其中公理的选择是多年来火箭科学逻辑的结果，因为规范不是一组看似合乎逻辑的公理持续的。
对于形式验证，您无法绕过公理的实施。在教科书中，数字常量只是出现并被使用，然后他们对它们进行推理。
在形式证明中，数常数，尤其是实数，很难使用。问问自己，“Isabelle/HOL 中的自然数、整数、有理数和实数常数是什么？” 现在，如果你回答了这个问题，那么问问自己，“我如何在 Isabelle/HOL 中进行涉及自然数、整数、有理数和实数的证明？”
现在，将这些问题与数字常量仅出现在大多数教科书中并被使用的事实进行对比。这不是它在形式证明中的工作方式。没有数字系统和常数的神奇外观。在涉及数字的证明的自动化中可能有一点魔法，但我很确定如果我的计划变得依赖于这样的魔法，我注定要失败。
NICTA有L4.verified 项目。（更新：在sel4.systems 上，与通用动力 C4 系统共同信用。像 GD 这样的大公司参与支持我的论点，即命令式编程语言的形式验证是很长一段时间以来非常需要的东西。 )
报价：
我们选择了一个操作系统内核来演示这一点：seL4。它是一个小型的第三代高性能微内核，大约有 8,700 行 C 代码。
为什么这么有选择性？为什么没有任何 ole C 程序？我想验证 C 很难。NICTA，他们不是一个没有经验、没有资金的小团体。
（更新：NICTA也有相关的AutoCorres 项目，其快速入门指南 PDF。发布版本为 v1.0，于 2014 年 12 月 16 日发布。这一定意味着他们实现了主要目标他们应该实现。当我在 AutoCorres 网页上阅读他们的概述时，我认为它支持我所说的。在我看来，他们参与了一些火箭科学逻辑以使 C 变成另一种形式，至少一点火箭科学逻辑。我对什么构成火箭科学逻辑没有权威。我想我可以肯定地说他们正在使用博士级别的逻辑来获得他们的结果。）
我下载了A Practical Theory of Programming一书的 PDF 。
我开始在那本书中寻找的第一件事是“什么是数字以及它们是如何形式化的”。
数字系统，我们认为它们是理所当然的，但它们代表了形式证明的所有困难。
在一本书中，当数字常量刚刚出现并开始被使用时，很可能意味着相应的数字系统没有真正的形式化。为什么？建立数字系统常数是非常涉及的。
如果数字常数没有正式建立，那里就没有真正的正式证明。如果他们正式建立起来，生活仍然不容易。
这里有一些关于处理真实数字的困难：拉里保尔森在 2014 年在美国宇航局的演讲。
我立即开始寻找的另一件事是传统循环的示例，您可以在其中反复修改变量。
它从Section 5.2.0 While Loop, aPToP.pdf#76 开始。示例在下一页，练习 265：
while ¬ x = y = 0 do
if y > 0 then y := y - 1
else (x := x - 1. var· y := n)
好了，这是使用可变状态的经典示例（我搜索了“可变状态”以实际查看我是否正确使用了该短语，但没有明确的结论）。
你有一个变量，你正在改变它的内容。所以，我听说，或者我得出的结论，这代表了为什么当你想要验证你用 J 编写的程序时，你注定要失败。
不是我要你下场。当您在 GitHub 上发布“Isabelle/HOL 中 J 编程语言的形式化 - 许多演示表明可以轻松地对 J 程序进行正式验证”时，我会在那里。
我有一种预感，如果我的主要应用程序是编程，Coq 会更好。
我通过在coq上进行 Google 搜索将要求保持在最低限度。
第一个链接是Ynot。
这是否支持您应该能够采用 J 并在 Isabelle/HOL 中实施它的想法？
不给我。它支持我的想法，如果有人知道很多，并且可以就他们将使用的语言做出设计决策，那么他们可以在证明助手中对命令式程序进行形式验证。
另一方面，你首先选择编程语言，然后围绕它塑造一个证明助手。
在这一点上，我对 J 的兴趣基本上是 0，范围从 0 到 10。
不过，假设您建立了一个网站，“这件事进展如何”，我用 RSS 阅读器订阅了它。
并不是我不想让你在 Isabelle/HOL 中正式验证 J 程序，而是我认为你做不到，所以我没有理由关心它，因为我不不需要它
然而，如果我在我的 RSS 阅读器中看到你网站的新活动，它告诉我你成功了，你把你的代码放在 GitHub 上，那么我的兴趣就会上升到 10。有人在 Isabelle 中为成熟的编程语言做形式化/HOL，可以很好地实现证明，例如函数式编程，而不仅仅是语言的一小部分，这是值得关注的事情。
四天过去了，放假了，专家可能不来了，给你我的答案。
我试图尽快得到简短的回答，但我先说几件事（实际上，很多事情），以尝试为我的快速回答提供一些支持。
我认为您使用的 Isabelle 词汇并不完全正确（“内部语法”），但我采用了您的两个短语，并加上了我大胆的强调：
我不想花时间澄清，所以这就是我认为你的要求，在那里我添加了一些细节，从听取专家的意见，并根据他们的情况为自己找出一些事情说过：
不幸的是，我的简短回答并没有完全成立。
为了让您了解您的要求，我现在引用主 J 网页的内容，其中重点是我的：
J 是一种现代的、高级的、通用的、高性能的编程语言。
我现在将通用重新表述为成熟的，像 C，像 Pascal，像许多高级通用编程语言一样，我提醒你，你需要两件事：
definition，primrec，datatype，和fun，其中让一个人定义的功能和新的数据类型，具有的标准库沿Isabelle/HOL 类型，例如对、列表等。现在，我声称，作为我个人的结论，你想要实现的东西至少和 Isabelle/HOL 一样难以实现，这是很多人多年来完成的结果。
请考虑 Peter Lammich 在我需要一个固定的可变数组中的 Isabelle 用户列表中所说的话：
HOL 本身不支持可变数组。
然而，有一个 Imperative_HOL，它有一个支持可变数组的堆 monad。
然后是 afp/Collections/Lib/Diff_Array，它提供了一个数组的实现，它的行为纯粹是函数式的，但如果只访问最后一个版本，则效率很高。
但是，如果您不是追求高效的可执行性，而只是寻找内存的抽象模型，那么使用上述类型是没有意义的，因为效率是以额外的形式化开销为代价的。
我在引用中的观点是，Isabelle/HOL 虽然强大到足以成为作为证明助手的主要竞争对手之一，但并未在其逻辑的主要部分实现标准数组，您在导入Complex_Main.
让我们(L, P)成对，L逻辑在哪里P，编程语言在哪里。我想谈谈两对，，(Isabelle/HOL, Haskell)你想要什么(x, J)，x你还没有确定的逻辑在哪里。
Isabelle/HOL 和 Haskell 之间有非常密切的关系。例如，Isabelle/HOL 的类型类被宣传为类 Haskell 类型类，并且，Haskell 是一种纯函数式编程语言，而 Isabelle/HOL 是纯的。我不想走得更远，因为作为一个非专家，我肯定会说一些不对的东西。
我想说明的一点是：
我不想以权威的身份说话。但是从聆听中，我的结论是：这就是逻辑。显然，实现编程语言比开发逻辑来推理程序要容易得多。
简短的回答是，在我看来，您正在寻找的示例代码是 Isabelle/HOL，因为尽管在Isabelle2014/src其他逻辑中还有一些示例，但我引用了您所说的和想要的，以及我所引用的我说你在说和想要，是你想要和需要一个full blown逻辑，比如 Isabelle/HOL。
从这里，我尝试抛出一些快速的想法。
那是我的笑话。
你正在和一位在该行业工作多年的高级工程师交谈，并学习了多年来在汽车行业积累的专业知识，你说，“我喜欢汽车的想法，但我的想法是用氮气燃料电池代替汽油。我该怎么做？”
分发网页上Isabelle2014 的理论库下的链接与文件夹中的Isabelle2014/src文件夹匹配。
在src文件夹中，你会看到文件夹CCL，Cube，CTT，等。
我相信这些对学习有好处，虽然可能仍然难以理解，但那些不是你所描述的。您要求对某种编程语言建模的完整实现。
我想至少对于 C 来说是有的。我找到了vcc.codeplex.com/。再说一次，我不是专家，所以我不想确切地说那里有什么，什么不是。
我的观点是 C 和 C++ 已经存在很长时间了，并且被大量使用，上面的链接显示，长期以来，有专业人士对验证 C 程序感兴趣，这很有意义.
但是，经过这么多年，为什么程序验证不是 C/C++ 编程的一个组成部分？
听过这里那里和邮件列表上的那些人，听过像 Scala 架构师 Martin Odersky 这样的人，他们一直想谈论可变和不可变状态，传统编程，如 C，我假设 J , 将属于使用可变状态的类别，非常使用它。随着时间的推移，我多次听说可变状态使得难以推理程序的作用。
我的观点是，设计编程语言一定比推理程序容易得多。
如果这个问题有一些竞争，我可能会不那么冗长，尽管可能不会，尽管可能如此，因为我什至没有给出答案。
我的最后一点是再次强调以上几点。了解一点历史是值得的，我在丘奇和库里之前就开始了。
我知道 Isabelle/HOL 是剑桥开始的结果，首先是 ML 的作者 Robin Milner，然后是 HOL 小组的 Mike Gordon，然后是 Larry Paulson，他是使用 Pure 作为最小逻辑来定义其他逻辑的作者，以及然后 Tobias Nipkow 与他合作，将 HOL 作为 Isabelle 中的逻辑开始，然后 Makarius Wenzel 为这一切添加了更高级别的语法，Isar（它不仅仅是语法糖；它是结构化证明功能的基础），连同 PIDE 前端，以及世界各地的其他人一直以来都做出了许多贡献，其中许多来自德国 TUM 的大集团，但还有澳大利亚的 CERN（更新：欧洲核子研究中心？这不是开玩笑；我确实知道 CERN 和 NICTA 之间的区别；世界，这不是一件容易的事情），回到欧洲地区，某个瑞士机构，ETH，还有更多的地方分布在德国和奥地利，UIBK，然后回到英国？我遗漏了谁？我，当然，还有世界各地的许多其他人。
跑题点？这就是你要求的东西，体现了一个行业的专业知识。要求它也不错。这是彻头彻尾的大胆，我所说的可能完全错误，并且错过了 ，通用编程语言的实现逻辑src的HOWTO 中的那个文件夹，所有的十个最简单的步骤，现在发送 9.95 美元，或欧元如果这就是你所拥有的，你会进行转换，我相信你，但是等等，还有更多，将目录更改为 Isabelle2014/medicaldoctor 并学习如何成为脑外科医生，也是。
这是另一个笑话，我声称。只是一个空间填充物，仅此而已。
无论如何，请考虑此处的第 47 至 60 行HOL.thy：
setup {* Axclass.class_axiomatization (@{binding type}, []) *}
default_sort type
setup {* Object_Logic.add_base_sort @{sort type} *}
axiomatization where fun_arity: "OFCLASS('a ? 'b, type_class)"
instance "fun" :: (type, type) type by (rule fun_arity)
axiomatization where itself_arity: "OFCLASS('a itself, type_class)"
instance itself :: (type) type by (rule itself_arity)
typedecl bool
judgment
Trueprop :: "bool => prop" ("(_)" 5)
每隔一段时间，我就会努力理解这几行。很长一段时间以来，我的出发点是typedecl bool，我并不关心试图了解在这之前是什么，除了HOL.thyimport 之外Pure。
最近，在尝试找出 Isabelle 中的类型和排序时，通过听取专家的意见，我终于看到这一行是我们得到的东西x::'a::type：
setup {* Object_Logic.add_base_sort @{sort type} *}
还有一点？我回到我之前说的。因为您想要完整的，所以您的示例是 Isabelle/HOL，但仅前 57 行HOL.thy不容易理解。但是如果你不从HOL开始，你要去哪里看？好吧，如果您发现的事情最终很容易，那么很可能部分原因是多年来数百人并没有将他们的努力放在最好的开始方式上。
或者，它可能只是被列为作者的 3 个人，Nipkow、Wenzel 和 Paulson。无论如何，即使HOL.thy不是那么长，只有 2019 行，但背后仍然有多年的经验和教育。当然，要了解 in 是什么HOL.thy，您至少必须对Pureis有一个模糊的了解。
看看src/Cube文件夹。这是我上面提到的示例逻辑之一。
只有两个文件，Cube.thy和Example.thy. 这应该很容易，但这就是问题所在，它太容易了。它不会反映 Isabelle/HOL 的复杂程度。
你的问题不是我的问题。Isabelle/HOL 非常适合数学推理，例如它能够用类型类抽象运算符。并且它有更多的好处，比如使用函数式编程定义函数，导出为 OCaml、Haskell、SML、Haskell 和 Eval。
我只是一个初学者，这就是我的全部。如果有更好的答案，那么我希望有人提出。
| 归档时间： |
|
| 查看次数： |
438 次 |
| 最近记录： |