如何证明给定语法的正确性？答案

【问题标题】：How to prove the correctness of a given grammar?如何证明给定语法的正确性？
【发布时间】：2017-09-05 10:31:45
【问题描述】：

我想知道编程语言开发人员如何验证和证明他们的语法是正确的。假设我为一种新语言创建了一个新语法。我可以通过提供不同类型的测试程序，使用单元测试工具测试我的语法。但是，我永远不会 100% 确保我的语法是正确的。语言开发者如何确保他们的语法在现实世界中是正确的？

假设我使用铅笔和纸为一门新语言创建了语法。但是，我犯了一个错误，我的语法接受以 + 结尾的表达式，如 2+2+。如果我没有发现错误，我将使用这个不正确的语法来实现我的语言。经过实施和单元测试，我可以找到错误。是否可以在开始实施之前找到它？

当然，我可以使用铅笔和纸（推导等）输入一些示例输入来尝试我的语法，但我可能会错过一些极端情况。有没有更好的方法或如何在真正的语言开发人员中测试他们的语法？

【问题讨论】：

语法“正确”是什么意思？或者您的意思是要问如何检查解析器是否正确识别了预期的语法？
理论上，你会产生一个正确性证明。我不知道这是否在现实世界中完成，但我对此表示怀疑。但是，如果没有正确性证明，您将不知道语法是否正确。所以也许人们不知道他们的语法是否正确——或者更确切地说，语法被定义为正确的，没有人真正知道他们描述的是什么语言！
我更新了我的问题。如何为语法做正确性证明？任何链接或解释？

标签： programming-languages grammar context-free-grammar formal-verification context-free-language

【解决方案1】：

证明是一个逻辑论证，它证明了一个主张的真实性。有很多方法可以证明某事，就像有很多思考问题的方法一样。证明离散结构（如语法）的常用方法是使用数学归纳法。基本上，您表明某些情况在基本情况下是正确的 - 可能是最简单的情况 - 然后表明，如果在一定规模以下的所有情况下都成立，那么对于下一个规模的情况也一定成立。

在我们的例子中：假设我们只是想证明你的语法没有在词尾生成 +。我们可以对在语言中构造字符串时使用的产生式数量进行归纳。我们将识别所有相关的基本情况，显示这些字符串的属性，然后显示语言中较长的字符串的构造方式使得在结尾不可能得到 +。这是一个例子。

S := S + S | (S) | x

基本情况：语言中最短的字符串是 x，生成为 S -> x。它不以 + 结尾。

归纳假设：假设使用最多 k 个产生式产生的所有字符串都不以 + 结尾。

归纳步骤：我们必须证明使用超过 k 个产生式产生的字符串不以 + 结尾。如果我们将规则 (S) 应用于从 S 生成的任何字符串，我们不添加 +，因此该属性成立。如果我们将 S + S 应用于从 S 生成的字符串，则 S + S 中的最后一个符号是 S 生成的较短字符串（至少短 2 个符号）的最后一个符号。根据归纳假设，该字符串不以 + 结尾，所以这个也没有。没有其他产生式，因此该语言中没有字符串以 + 结尾。量子力学

【讨论】：