9. 계약에 의한 설계(DbC)

Ada 2012에서 표준화된 계약에 의한 설계(Design by Contract, DbC)는 프로그래머가 형식적이고 검증 가능한 명세를 소스 코드에 직접 내장할 수 있게 하여 Ada의 신뢰성 기능을 향상시킵니다. 이러한 계약은 실행 가능한 문서 역할을 하며, 고수준 요구사항을 구현에 연결합니다. 컴파일러 스위치(-gnata)로 활성화하면, 이러한 계약은 실행 시간에 검사되어 위반 시 Assert_Failure 예외를 발생시킵니다.

Ada에서 DbC의 핵심 구성 요소는 다음과 같습니다:

• 전제조건(Preconditions): 서브프로그램이 호출되기 전에 참이어야 하는 조건입니다. 이는 호출자 측의 의무입니다. with pre =>...로 지정됩니다.

  function square_root (x : Float) return Float with pre => x >= 0.0;
  

• 후조건(Postconditions): 서브프로그램이 성공적으로 완료되었을 때 참이 될 것을 보장하는 조건입니다. 이는 서브프로그램 구현 측의 의무입니다. with post =>...로 지정됩니다. 후조건은 'old 속성으로 매개변수의 초기 값을, 'result 속성으로 함수의 결과를 참조할 수 있습니다.

  procedure increment (value : in out Integer) with post => value = value'old + 1;
  

• 형식 불변식 및 술어(Type Invariants and Predicates): 주어진 형식의 모든 객체에 대해 항상 참이어야 하는 조건입니다. 술어(with static_predicate => ...)는 해당 형식의 값이 생성되거나 수정될 때마다 검사되는 속성입니다. 불변식(with type_invariant => ...)은 개인 형식의 속성으로, 공개 연산의 경계에서 검사됩니다.

계약은 유용한 도구입니다. 컴파일된 코드와 일치하는 문서를 제공합니다. 테스트와 디버깅을 위한 정확한 기반 역할을 하며, 형식적 검증 도구에 대한 중요한 입력이 됩니다.