프로그램 파생
Program derivation컴퓨터 과학에서 프로그램 파생은 프로그램의 명세서로부터 수학적 수단으로 파생되는 것이다.
프로그램을 도출한다는 것은 형식적인 명세서를 작성하는 것을 의미하며, 이는 보통 실행 불가능한 것이다. 그리고 나서 그 명세를 만족시키는 실행 가능한 프로그램을 얻기 위해 수학적으로 정확한 규칙을 적용한다.이렇게 획득한 프로그램은 시공에 의해 정확하다.프로그램과 정확성 증명이 함께 구성된다.
일반적으로 공식적인 검증에서 취하는 접근방식은 먼저 프로그램을 작성한 후 그것이 주어진 명세서에 부합한다는 증거를 제공하는 것이다.이것의 주요 문제점은
- 결과적인 증거는 종종 길고 번거롭다.
- 프로그램이 어떻게 개발되었는지에 대한 통찰력은 없다; 그것은 "모자 속의 토끼처럼" 보인다.
- 만약 프로그램이 어떤 미묘한 방법으로 부정확하게 된다면, 그것을 검증하려는 시도는 길고 결실이 없는 것이 확실할 것이다.
프로그램 파생은 이러한 단점을 보완하기 위해 노력한다.
- 적절한 수학적 개념의 개발을 통해 증거를 더 짧게 보관한다.
- 규격의 형식적인 조작을 통해 설계 결정을 내리는 것.
프로그램 파생과 대략 동의어인 용어는 변환 프로그래밍, 알고리즘, 연역 프로그래밍이다.
새-메르텐스 형식주의는 프로그램 파생에 대한 접근법이다.
참고 항목
참조
- Edsger W. Dijkstra, Wim H. J. Feijen, A Method of Programming, Addison-Wesley, 1988, 188쪽
- 1990년대 프로그램, Springer-Verlag, 1990년대의 Edward Cohen
- Anne Kaldewaij, 프로그래밍: 알고리즘의 파생, 프렌티스 홀, 1990, 216페이지
- David Gries, The Science of Programming, Springer-Verlag, 1981, 350페이지
- Carroll Morgan(컴퓨터 과학자), Programming from Specifications, International Series in Computer Science(2차 개정판), Fratice-Hall, 1998.
- 에릭 C.R. 헤너, 프로그래밍의 실용 이론, 2008년 235쪽
- A.J.M. 반 게스트렌.수학적인 논쟁의 형태에 대해서.컴퓨터 과학 강의 노트 #445, Springer-Verlag, 1990.증빙서류 작성법을 명료하고 정밀하게 가르친다.
- 마틴 렘. "소규모 프로그래밍 연습"은 컴퓨터 프로그래밍의 과학, Vol.3 (1983)에서 Vol.14 (1990)까지 등장했다.
- 롤랜드 백하우스프로그램 구성: 사양에서 구현 계산 중.와일리, 2003년 ISBN978-0-470-84882-1.
- 데릭 G. 쿠리, 브루스 W.왓슨.프로그래밍에 대한 시공별 정확성 접근법스프링거-베를라크, 2012.ISBN 978-3-642-27919-5.작고 다루기 쉬운 정밀도를 이용하여 수학적으로 올바른 알고리즘을 도출하는 방법에 대한 단계별 설명을 제공한다.
