불변 기반 프로그래밍

불변 기반 프로그래밍은^[1] 실제 프로그램 문 앞에 사양과 불변수가 작성되는 프로그래밍 방법론입니다.프로그래밍 프로세스 중에 불변량을 적는 것은 많은 이점이 있습니다. 프로그래머가 실제로 프로그램 동작을 구현하기 전에 프로그램 동작에 대한 의도를 명확히 해야 하며, 실행 중에 불변량을 동적으로 평가하여 일반적인 프로그래밍 오류를 파악할 수 있습니다.게다가 충분히 강하면, 불변량은 프로그램 문의 형식적인 의미론에 근거해 프로그램의 정확성을 증명하기 위해서 사용될 수 있다.간단한 프로그램이 아닌 프로그램의 완전한 검증을 위해서는 일반적으로 강력한 공식 증명 시스템에 연결된 복합 프로그래밍 및 사양 언어가 필요합니다.이 경우 고도의 증명 자동화도 가능하다.

대부분의 기존 프로그래밍 언어에서 주요 구성 구조는 루프, 루프 및 문과 같은 제어 흐름 블록입니다.이러한 언어는 프로그래머가 불변수를 쓰기 전에 제어 흐름에 대한 결정을 내리도록 하기 때문에 불변수 우선 프로그래밍에는 이상적이지 않을 수 있습니다.게다가, 대부분의 프로그래밍 언어들은 양자화 연산자가 부족하고 일반적으로 고차 특성을 표현할 수 없기 때문에 기술 명세서와 불변량을 잘 지원하지 않습니다.

이 프로그램을 그 증거와 함께 개발하자는 아이디어는 E.W.에서 비롯되었다. 다이크스트라M.H. van Emden, J.C. 레이놀즈 및 R-J Back은 프로그램 스테이트먼트 전에 실제로 불변수를 작성하는 것을 여러 가지 다른 형태로 검토했습니다.

「 」를 참조해 주세요.

• 에펠(프로그래밍 언어)

메모들