我想知道编程语言开发人员如何验证并证明他们的语法是正确的。假设我为一种新语言创建了一个新语法。我可以通过提供不同类型的测试程序，使用单元测试工具测试我的语法。但是，我永远不会 100% 确保我的语法是正确的。语言开发人员如何确保他们的语法在现实世界中是正确的？
假设我用铅笔和纸为一种新语言创建了一个语法。但是，我犯了一个错误，我的语法接受以 + 结尾的表达式，如 2+2+。如果我没有发现错误，我将使用这个不正确的语法来实现我的语言。经过实施和单元测试，我可以找到错误。在开始任何实施之前是否可以找到它？
当然，我可以使用铅笔和纸（推导等）输入一些示例输入来尝试我的语法，但我可能会错过一些极端情况。有没有更好的方法或者在真正的语言开发人员中如何测试他们的语法？
证明是证明主张真实性的逻辑论证。有很多方法可以证明某事，就像有很多思考问题的方法一样。证明离散结构（如语法）的常用方法是使用数学归纳法。基本上，您表明某些情况在基本情况下是正确的 - 可能是最简单的情况 - 然后表明，如果在一定规模下的所有情况下都成立，那么对于下一个规模的情况也一定成立。
在我们的例子中：假设我们只想证明您的语法没有在单词末尾生成 +。我们可以对在语言中构造字符串时使用的产生式数量进行归纳。我们将识别所有相关的基本情况，显示这些字符串的属性，然后显示语言中较长的字符串的构造方式使得在结尾不可能得到 +。这是一个例子。
S := S + S | (S) | X
基本情况：语言中最短的字符串是 x，生成为 S -> x。它不以 + 结尾。
归纳假设：假设使用多达 k 个产生式产生的所有字符串不以 + 结尾。
归纳步骤：我们必须显示使用超过 k 个产生式产生的字符串不以 + 结尾。如果我们将规则 (S) 应用于从 S 生成的任何字符串，我们不添加 +，因此该属性成立。如果我们将 S + S 应用于从 S 生成的字符串，则 S + S 中的最后一个符号是 S 生成的较短字符串（至少短 2 个符号）的最后一个符号。根据归纳假设，该字符串不以 + 结尾，所以这个也没有。没有其他产生式，因此该语言中没有字符串以 + 结尾。量子点