사후 조건

컴퓨터 프로그래밍에서 포스트 조건은 코드 섹션의 실행 직후 또는 정식 사양의 연산 후에 항상 참이어야 하는 조건 또는 술어입니다.사후 조건은 코드 자체 내의 어사션을 사용하여 테스트되는 경우가 있습니다.대부분의 경우 사후 조건은 해당 코드 섹션의 설명서에 포함됩니다.

예를 들어 다음과 같습니다.요인 결과는 항상 정수이며 1보다 크거나 같습니다.따라서 입력 숫자의 계수를 계산하는 프로그램에는 계산 후 결과가 정수이고 1보다 크거나 같은 조건이 붙습니다.다른 예로는 입력 숫자의 제곱근을 계산하는 프로그램이 결과가 숫자이고 그 제곱이 입력과 같다는 조건을 가질 수 있습니다.

객체 지향 프로그래밍의 전제 조건

일부 소프트웨어 설계 접근법에서 전제조건 및 클래스 불변성과 함께 사후조건은 계약에 의한 소프트웨어 구축방법 설계의 구성요소이다.

루틴의 전제조건은 루틴 실행 ^[1]완료 시 보증되는 속성 선언입니다.그 루틴의 계약과 관련되기 때문에, 포스트 컨디션은, 그 전제 조건이 유지되고 있는 상태로 루틴이 호출되었을 경우, 포스트 컨디션에 의해서 선언된 속성이 보증되는 것을 잠재 발신자에게 보증한다.

에펠의 예

에펠로 작성된 다음 예시는 클래스 속성의 값을 설정합니다.hour발신자가 제공한 인수에 따라a_hourpost condition은 키워드 뒤에 있습니다.ensure이 예에서는 전제조건이 유지되는 경우(즉, 다음과 같은 경우) 사후조건이 보증된다.a_hour하루 중 유효한 시간을 나타냄)의 실행 후set_hour, 클래스 속성hour같은 가치를 가지다a_hour. 태그 "hour_set:" 는 이 postcondition 구에 대해 설명하고 런타임 postcondition 위반 시 이를 식별하는 역할을 합니다.

    set_hours (1시간: 정수)             -- "hour" 를 "a_hour" 로 설정합니다.         요구하다             valid_filename(유효): 0 <=> 1시간 그리고. 1시간 <=> 23         하다             한 시간 := 1시간         확신해주다             시간 설정: 한 시간 = 1시간         끝. 

사후 조건 및 상속

상속이 존재하는 경우 하위 클래스(하위 클래스)에 의해 상속되는 루틴은 계약(즉, 사전 조건 및 사후 조건)에 따라 상속됩니다.즉, 상속된 루틴의 구현이나 재정의도 상속된 계약에 따라 작성해야 합니다.사후 조건은 재정의된 루틴에서 수정할 수 있지만 ^[2]강화만 될 수 있습니다.즉, 재정의된 루틴이 클라이언트에 제공하는 이점은 증가하지만 이러한 이점은 감소하지 않을 수 있습니다.

「 」를 참조해 주세요.

• 전제 조건
• 계약에 의한 설계
• 호어 논리
• 조건에 의해 유지되는 불변량
• 데이터베이스 트리거

레퍼런스