정확성을 보존하는 프로그램 변환

이 논문은 프로그램의 부분 정확성 속성에 대한 술어 미적 정형화(Ki, Go)를 프로그램 변환下에서의 정확성 보존을 포함하도록 확장합니다. "속성을 보존하는 프로그램 변환"의 일반 개념은 프로그래밍 및 프로그래밍 언어 이론에 기본적입니다. 프로그램 정확성 증명의 맥락에서, 정확성을 보존하는 변환은 덜 효율적이지만 증명하기 더 쉬운 프로그램을 개선하는 데 사용될 수 있습니다. 정확성을 보존하는 프로그램 변환(CPTs)의 사용에 대한 기본 주장은 다음과 같습니다: G가 특정 입력-출력 관계 Ain-Aout에 대해 정확하다고 증명된 프로그램(단정식이 첨부된)이라고 가정합니다. 이제 G의 일부, 예를 들어 표현식, 단정식, 문장 등이 다른 그러한 부분 S'로 대체되어 프로그램 G'를 생성한다고 가정합니다. 목표는 G'도 Ain-Aout에 대해 정확하다는 것을 증명하는 것이며, 따라서 대체가 전체 프로그램의 정확성을 보존한다고 말할 수 있습니다. Moreover, 대체가 국부적 효과만 미치는 경우(예: 루프의 본문), 그러면 정확성 보존의 증명은 대체로 영향을 받는 프로그램의 해당 부분으로 제한되어야 합니다. 섹션 2에서는 프로그램 정확성을 증명하기 위한 현재 패러다임을 검토합니다. 섹션 3의 예시는 정확하고 간단하지만 비효율적인 초기 프로그램에 대한 일련의 개선에서 CPTs를 보여줍니다. 섹션 4에서는 프로그램의 부분 정확성 속성의 정형화를 Knuth의 의미론적 방법(Kn1)을 사용하여 의미론적 언어 정의로 다시 표현합니다. 이 정형화는 섹션 5에서 CPT를 수행하는 메커니즘을 설명하는 데 사용됩니다. 섹션 6에서는 섹션 4 및 5의 정형화에 대한 여러 질문을 논의하고 일반화를 제안합니다. 마지막으로 섹션 7은 구체적인 예로 돌아가 가장 효과적인 CPT 사용은 도식적 형태의 식별에 있다고 제안합니다. 관련 연구는 섹션 8에서 언급됩니다.