정제 미적분
Refinement calculus정제 미적분은 프로그램 구축을 위한 단계적 정교화에 대한 공식화된 접근법입니다.최종 실행 가능 프로그램의 필요한 동작은 추상적이고 실행 불가능할 수 있는 "프로그램"으로 지정되며, 이후 일련의 정확성 보존 변환에 의해 효율적으로 실행 가능한 프로그램으로 [1]개선됩니다.
1978년 박사학위 논문 '프로그램 개발의 개선 단계에 대한 정확성'에서 접근방식을 창안한 Ralph-Johan Back과 Carroll Morgan, 특히 그의 책 Programming from Specifications(Programming from Specifications, 1994년 2판)에서 이 접근방식을 창안한 사람이 지지자이다. ISBN0-13-123274-6)를 참조해 주세요.후자의 경우, 그 동기는 행동 보존 프로그램 개선의 엄격한 관계를 통해 Abrial의 사양 표기법 Z를 Dijkstra의 보호 명령어에 기초한 실행 가능한 프로그래밍 표기법과 연결시키는 것이었다.이 경우 동작보존이란 프로그램에 의해 충족되는 모든 Hoare 트리플은 프로그램의 미세화에 의해 충족되어야 한다는 것을 의미하며, 이러한 개념은 프로그램 사이에 건전하게 배치될 수 있는 모든 프로그램에 대한 사전 및 사후 조건으로서의 사양 문장으로 직접 이어진다.
레퍼런스
- ^ Butler, Michael. "Refinement Calculus Tutorial". Retrieved 22 April 2020.
