我想知道編程語言開發人員如何驗證並證明他們的語法是正確的。假設我爲一個新的語言創建了一個新的語法。我可以通過提供不同類型的測試程序來使用單元測試工具來測試我的語法。但是，我絕不會100％確保我的語法是正確的。語言開發人員如何確保他們的語法在現實世界中是正確的？如何證明給定語法的正確性？
比方說，我用鉛筆和紙創建了一種新語言的語法。但是，我犯了一個錯誤，我的語法接受以+ + 2 + 2 +結尾的表達式。如果我沒有發現它的錯誤，我會用這個不正確的語法來實現我的語言。在執行和單元測試之後，我可以找到錯誤。在開始實施之前是否有可能找到它？
當然，我可以嘗試使用鉛筆和紙（派生等）的一些示例輸入我的語法，但我可能會錯過一些角落案例。有沒有更好的方法，或者真正的語言開發人員如何測試他們的語法？
證明是一個邏輯論證，證明了索賠的真實性。有許多方法可以證明某件事情，因爲有一種思考問題的方式。證明離散結構（如語法）的常用方法是使用數學歸納法。基本上，你會發現在基本情況下有些事情是真實的 - 最簡單的情況是可能的 - 然後表明如果對於所有大小不一的情況都是如此，那麼對於下一個大小的情況，它必須是正確的。
在我們的案例中：假設我們只想證明您的語法在單詞的末尾沒有生成+。我們可以對語言中構造字符串時使用的製作次數進行歸納。我們將識別所有相關的基本案例，顯示這些字符串的屬性，然後顯示語言中較長的字符串的構造方式使得在末尾不可能獲得+。這是一個例子。
S：= S + S | （S）| x
基本情況：語言中最短的字符串是x，生成爲S - > x。它不以+結束。
歸納假設：假設所有使用高達幷包括k個產品的字符串都不以+結束。
感應步驟：我們必須顯示使用多於k個製作產生的字符串不以+結束。如果我們將規則（S）應用於從S生成的任何字符串，我們不會添加+，因此屬性可以保持。如果我們將S + S應用於從S生成的字符串，則S + S中的最後一個符號是由S生成的較短字符串的最後一個符號（至少2個符號較短）。通過歸納假設，該字符串沒有以+ ，這個也沒有。沒有其他產品，因此語言中沒有字符串以+結尾。 QED
語法是「正確的」是什麼意思？還是你的意思是要問如何檢查一個解析器正確識別預期的語法？ – rici
從理論上講，你會產生一個正確性證明。我不知道這是否在現實世界中完成，但我懷疑它。但是，如果沒有正確的證據，你就不知道語法是正確的。所以也許人們不知道他們的語法是否正確 - 或者說，語法被定義爲正確的，沒有人真正知道他們描述的語言！ – Patrick87
我更新了我的問題。我如何做一個語法的正確性證明？任何鏈接或解釋？ –