주어진 문법의 정확성을 증명하는 방법은 무엇입니까?

Question

프로그래밍 언어 개발자가 어떻게 문법이 올바른지 검증하고 증명하는지 궁금합니다. 새로운 언어에 대한 새로운 문법을 만들었다 고 가정 해 봅시다. 여러 종류의 테스트 프로그램을 제공함으로써 단위 테스트 도구로 문법을 테스트 할 수 있습니다. 그러나, 나는 결코 나의 문법이 정확하다는 것을 100 % 보장하지 않을 것이다. 언어 개발자는 실제 문법이 올바른지 어떻게 확인합니까?

연필과 종이를 사용하여 새로운 언어의 문법을 만들었습니다. 그러나 실수를했고 문법은 2 + 2 +와 같이 끝나는 표현을 허용합니다. 실수를 발견하지 못하면이 잘못된 문법을 사용하여 제 언어를 구현할 것입니다. 구현 및 단위 테스트 후에 오류를 찾을 수 있습니다. 구현을 시작하기 전에 찾을 수 있습니까?

필자는 연필과 종이 (파생 ​​등)를 사용하여 샘플 입력으로 문법을 시험해 볼 수는 있지만 일부 모서리의 경우가 누락 될 수 있습니다. 실제 언어 개발자가 문법을 테스트하는 방법이 더 좋은가?

Answer 1

증거는 주장의 진실성을 입증하는 논리적 인 주장입니다. 문제를 생각하는 방법이 있기 때문에 뭔가를 증명할 수있는 많은 방법이 있습니다. 문법과 같은 개별 구조에 대한 것들을 증명하는 일반적인 방법은 수학적 유도를 사용하는 것입니다. 기본적으로 가능한 경우 가장 간단한 경우 인 기본 케이스에 사실이 있음을 보여주고 특정 크기 이하의 모든 케이스에 해당되는 경우 다음 크기의 케이스에 해당해야합니다.

우리의 경우 : 귀하의 문법이 단어의 끝에 +를 생성하지 않았다는 것을 증명하기를 원한다고 가정 해보십시오. 언어로 문자열을 만드는 데 사용되는 제작물 수를 유도 할 수 있습니다. 모든 관련 기본 사례를 식별하고,이 문자열에 대한 속성 보유를 표시 한 다음, 언어에서 더 긴 문자열이 +가 끝날 수없는 방식으로 구성된다는 것을 보여줍니다. 여기에 예제가 있습니다.

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

기본 경우 : 언어에서 가장 짧은 문자열은 x이며 S -> x로 생성됩니다. +로 끝나지 않습니다.

유도 가설 : k 작품까지 포함하여 생성 된 모든 문자열이 +로 끝나지 않는다고 가정하십시오.

유도 단계 : k 개가 넘는 프로덕션을 사용하여 생성 된 문자열은 +로 끝나지 않아야합니다. S에서 생성 된 문자열에 규칙 (S)을 적용하면 속성에 +가 추가되지 않습니다. S에서 생성 된 문자열에 S + S를 적용하면 S + S의 마지막 기호는 S에 의해 생성 된 더 짧은 문자열 (최소 2 개의 기호가 더 짧음)의 마지막 기호입니다. 유도 가설에 따르면 해당 문자열은 + , 어느 쪽도 이것을하지 않는다. 다른 제작물이 없기 때문에 언어의 문자열은 +로 끝나지 않습니다. QED