설계-계약
설계-계약 (Design by contracts)
계약(contract)은 프로그래밍에서 기대 사항을 코드화(codify)하는 데 사용돼요. 서브프로그램의 매개변수 모드는 계약의 단순한 형태로 볼 수 있어요. 서브프로그램 Op의 스펙이 in 모드로 매개변수를 선언하면, Op의 호출자는 in 인자가 Op에 의해 변경되지 않을 것을 알아요. 즉, 호출자는 Op가 제공하는 인자를 수정하지 않고 인자에 저장된 정보만 읽을 것이라고 기대해요. 제약(constraint)과 하위 타입(subtype)도 계약의 다른 예시예요. 일반적으로 이런 선언들은 애플리케이션의 일관성을 개선해요.
설계-계약(design-by-contract) 프로그래밍은 사전조건·사후조건(pre/postconditions), 하위 타입 술어(subtype predicates), 타입 불변식(type invariants)을 포함하는 기법을 말해요. 이 장에서 이 주제들을 다룰게요.
출처: 설계-계약 문서
본문
사전조건과 사후조건 (Pre- and postconditions)
사전조건과 사후조건은 서브프로그램의 입력·출력 매개변수와 함수의 반환 값에 대한 기대를 제공해요. 서브프로그램 Op를 호출하기 전에 충족되어야 하는 요구사항이 있다면 그것이 사전조건(precondition) 이에요. 마찬가지로 서브프로그램 Op 호출 후에 충족되어야 하는 요구사항이 있다면 그것이 사후조건(postcondition) 이에요. 사전조건과 사후조건을 서브프로그램 호출자와 피호출자 사이의 약속으로 생각할 수 있어요: 사전조건은 호출자에서 피호출자로의 약속이고, 사후조건은 반대 방향의 약속이에요.
사전조건과 사후조건은 서브프로그램 선언의 애스펙트(aspect) 절로 지정돼요. with Pre => <condition> 절은 사전조건을, with Post => <condition> 절은 사후조건을 지정해요.
다음 코드는 사전조건의 예시를 보여줘요:
procedure Show_Simple_Precondition is
procedure DB_Entry (Name : String;
Age : Natural)
with Pre => Name'Length > 0
is
begin
-- Missing implementation
null;
end DB_Entry;
begin
DB_Entry ("John", 30);
-- Precondition will fail!
DB_Entry ("", 21);
end Show_Simple_Precondition;
이 예시에서 데이터베이스의 name 필드가 빈 문자열을 포함하지 못하게 하고 싶어요. DB_Entry 프로시저의 Name 매개변수에 사용된 문자열의 길이가 0보다 크도록 요구하는 사전조건을 사용해 이 요구사항을 구현해요. DB_Entry 프로시저가 Name 매개변수에 빈 문자열로 호출되면 사전조건이 충족되지 않아 호출이 실패해요.
GNAT 툴체인에서 (In the GNAT toolchain)
GNAT는 사전·사후조건을 처리할 때 런타임 어서션(assertion)을 생성해요. 하지만 기본적으로 어서션은 활성화되지 않아요. 따라서 런타임에 사전·사후조건을 검사하려면 -gnata 스위치를 사용해 어서션을 활성화해야 해요.
다음 예시로 가기 전에, 사전·사후조건을 간결하게 작성하는 데 매우 유용한 정량 표현식(quantified expressions) 을 잠시 다뤄볼게요. 정량 표현식은 배열이나 컨테이너의 요소가 기대하는 조건과 일치하는지 나타내는 Boolean 값을 반환해요. 형태는 (for all I in A'Range => <condition on A(I)>이에요. A는 배열이고 I는 인덱스예요. for all을 사용하는 정량 표현식은 조건이 모든 요소에 대해 참인지 검사해요. 예를 들어:
(for all I in A'Range => A (I) = 0)
이 정량 표현식은 배열 A의 모든 요소가 값 0을 가질 때만 참이에요.
다른 종류의 정량 표현식은 for some을 사용해요. 형태는 비슷해요: (for some I in A'Range => <condition on A(I)>. 하지만 이 경우 자격 표현식은 조건이 모든 요소가 아니라 일부 요소에 대해서만 참인지 검사해요(그래서 이름이 for some이에요).
다음 예시로 사후조건을 설명할게요:
with Ada.Text_IO; use Ada.Text_IO;
procedure Show_Simple_Postcondition is
type Int_8 is range -2 ** 7 .. 2 ** 7 - 1;
type Int_8_Array is
array (Integer range <>) of Int_8;
function Square (A : Int_8) return Int_8 is
(A * A)
with Post => (if abs A in 0 | 1
then Square'Result = abs A
else Square'Result > A);
procedure Square (A : in out Int_8_Array)
with Post => (for all I in A'Range =>
A (I) = A'Old (I) *
A'Old (I))
is
begin
for V of A loop
V := Square (V);
end loop;
end Square;
V : Int_8_Array := (-2, -1, 0, 1, 10, 11);
begin
for E of V loop
Put_Line ("Original: "
& Int_8'Image (E));
end loop;
New_Line;
Square (V);
for E of V loop
Put_Line ("Square: "
& Int_8'Image (E));
end loop;
end Show_Simple_Postcondition;
부호 있는 8비트 타입 Int_8과 그 타입의 배열(Int_8_Array)을 선언해요. Int_8_Array 타입의 객체에 대해 Square 프로시저를 호출한 후 배열의 각 요소가 제곱되도록 보장하고 싶어요. for all 표현식을 사용하는 사후조건으로 이걸 해요. 이 사후조건은 또한 'Old 애트리뷰트를 사용해 (호출 전의) 매개변수의 원래 값을 참조해요.
또한 Int_8 타입에 대한 Square 함수 호출의 결과가 그 호출의 입력보다 크도록 보장하고 싶어요. 이를 위해 함수의 'Result 애트리뷰트를 사용하고 입력 값과 비교하는 사후조건을 작성해요.
단일 서브프로그램 선언에 사전조건과 사후조건을 모두 사용할 수 있어요. 예를 들어:
with Ada.Text_IO; use Ada.Text_IO;
procedure Show_Simple_Contract is
type Int_8 is range -2 ** 7 .. 2 ** 7 - 1;
function Square (A : Int_8) return Int_8 is
(A * A)
with
Pre => (Integer'Size >= Int_8'Size * 2
and Integer (A) *
Integer (A) <=
Integer (Int_8'Last)),
Post => (if abs A in 0 | 1
then Square'Result = abs A
else Square'Result > A);
V : Int_8;
begin
V := Square (11);
Put_Line ("Square of 11 is "
& Int_8'Image (V));
-- Precondition will fail...
V := Square (12);
Put_Line ("Square of 12 is "
& Int_8'Image (V));
end Show_Simple_Contract;
이 예시에서 Int_8 타입에 대한 Square 함수 호출의 입력 값이 그 함수에서 오버플로를 일으키지 않도록 보장하고 싶어요. 임시 계산에 사용되는 Integer 타입으로 입력 값을 변환하고, 결과가 Int_8 타입에 적절한 범위에 있는지 확인함으로써 이걸 해요. 이 예시에는 이전 예시와 같은 사후조건이 있어요.
술어 (Predicates)
술어(predicate)는 타입에 대한 기대를 지정해요. 사전·사후조건과 비슷하지만 서브프로그램 대신 타입에 적용돼요. 그들의 조건은 주어진 타입의 각 객체에 대해 검사되며, 타입 T의 객체가 그 타입의 요구사항에 부합(conformant)하는지 검증할 수 있게 해줘요.
술어에는 정적(static)과 동적(dynamic) 두 종류가 있어요. 간단히 말해 정적 술어는 컴파일 타임에 객체를 검사하는 데 사용되고, 동적 술어는 런타임 검사에 사용돼요. 보통 정적 술어는 스칼라 타입에, 동적 술어는 더 복잡한 타입에 사용돼요.
정적 및 동적 술어는 각각 다음 절로 지정돼요:
with Static_Predicate => <property>with Dynamic_Predicate => <property>
동적 술어를 설명하기 위해 다음 예시를 사용할게요:
with Ada.Calendar; use Ada.Calendar;
with Ada.Containers.Vectors;
with Ada.Strings.Unbounded;
use Ada.Strings.Unbounded;
procedure Show_Dynamic_Predicate_Courses is
package Courses is
type Course_Container is private;
type Course is record
Name : Unbounded_String;
Start_Date : Time;
End_Date : Time;
end record
with Dynamic_Predicate =>
Course.Start_Date <= Course.End_Date;
procedure Add (CC : in out Course_Container;
C : Course);
private
package Course_Vectors is new
Ada.Containers.Vectors
(Index_Type => Natural,
Element_Type => Course);
type Course_Container is record
V : Course_Vectors.Vector;
end record;
end Courses;
package body Courses is
procedure Add (CC : in out Course_Container;
C : Course) is
begin
CC.V.Append (C);
end Add;
end Courses;
use Courses;
CC : Course_Container;
begin
Add (CC,
Course'(
Name =>
To_Unbounded_String
("Intro to Photography"),
Start_Date =>
Time_Of (2018, 5, 1),
End_Date =>
Time_Of (2018, 5, 10)));
-- This should trigger an error in the
-- dynamic predicate check
Add (CC,
Course'(
Name =>
To_Unbounded_String
("Intro to Video Recording"),
Start_Date =>
Time_Of (2019, 5, 1),
End_Date =>
Time_Of (2018, 5, 10)));
end Show_Dynamic_Predicate_Courses;
이 예시에서 Courses 패키지는 Course 타입과 Course_Container 타입을 정의해요. Course_Container 객체는 모든 과정을 포함해요. 각 과정의 날짜가 일관적이도록, 특히 시작 날짜가 종료 날짜보다 늦지 않도록 보장하고 싶어요. 이 규칙을 강제하기 위해 각 객체에 대해 검사를 수행하는 Course 타입용 동적 술어를 선언해요. 술어는 그 타입의 변수가 보통 사용되는 곳에서 타입 이름을 사용하는데, 이것은 테스트되는 객체 인스턴스에 대한 참조예요.
위 예시는 무제한 문자열과 날짜를 사용한다는 점에 주의하세요. 두 타입 모두 Ada 표준 라이브러리에서 사용할 수 있어요. 자세한 내용은 다음 절을 참조하세요:
- 무제한 문자열 타입(
Unbounded_String): Unbounded Strings 절 - 날짜와 시간: Dates & Times 절
앞서 언급했듯 정적 술어는 주로 스칼라 타입에 사용되고 컴파일 중에 검사돼요. 이는 특히 열거형의 비연속적인 요소를 표현하는 데 유용해요. 전형적인 예는 주중 요일 목록이에요:
type Week is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);
Week에 기반한 범위를 가진 subtype을 지정해 주중의 근무일 하위 목록을 쉽게 만들 수 있어요. 예를 들어:
subtype Work_Week is Week range Mon .. Fri;
Ada의 범위는 연속적인 목록으로만 지정할 수 있어요. 특정 요일을 고를 수는 없죠. 하지만 근무 주간의 첫째, 중간, 마지막 날만 포함하는 목록을 만들고 싶을 수 있어요. 그렇게 하려면 정적 술어를 사용해요:
subtype Check_Days is Work_Week
with Static_Predicate =>
Check_Days in Mon | Wed | Fri;
완전한 예시를 볼게요:
with Ada.Text_IO; use Ada.Text_IO;
procedure Show_Predicates is
type Week is (Mon, Tue, Wed, Thu,
Fri, Sat, Sun);
subtype Work_Week is Week range Mon .. Fri;
subtype Test_Days is Work_Week
with Static_Predicate =>
Test_Days in Mon | Wed | Fri;
type Tests_Week is array (Week) of Natural
with Dynamic_Predicate =>
(for all I in Tests_Week'Range =>
(case I is
when Test_Days =>
Tests_Week (I) > 0,
when others =>
Tests_Week (I) = 0));
Num_Tests : Tests_Week :=
(Mon => 3, Tue => 0,
Wed => 4, Thu => 0,
Fri => 2, Sat => 0,
Sun => 0);
procedure Display_Tests (N : Tests_Week) is
begin
for I in Test_Days loop
Put_Line ("# tests on "
& Test_Days'Image (I)
& " => "
& Integer'Image (N (I)));
end loop;
end Display_Tests;
begin
Display_Tests (Num_Tests);
-- Assigning non-conformant values to
-- individual elements of the Tests_Week
-- type does not trigger a predicate
-- check:
Num_Tests (Tue) := 2;
-- However, assignments with the "complete"
-- Tests_Week type trigger a predicate
-- check. For example:
--
-- Num_Tests := (others => 0);
-- Also, calling any subprogram with
-- parameters of Tests_Week type
-- triggers a predicate check. Therefore,
-- the following line will fail:
Display_Tests (Num_Tests);
end Show_Predicates;
여기 근무 주간의 사흘에만 테스트를 수행하고 싶은 애플리케이션이 있어요. 이 날들은 Test_Days 하위 타입에 지정돼요. 매일 발생하는 테스트 수를 추적하고 싶어요. Tests_Week 타입을 배열로 선언하고, 그 객체는 매일 수행된 테스트 수를 포함해요. 요구사항에 따라 이 테스트는 앞서 언급한 사흘에만 수행되어야 하고, 다른 날에는 테스트가 수행되지 않아야 해요. 이 요구사항은 Tests_Week 타입의 동적 술어로 구현돼요. 마지막으로 이 테스트들에 대한 실제 정보는 Tests_Week 타입의 인스턴스인 Num_Tests 배열에 저장돼요.
Tests_Week 타입의 동적 술어는 Num_Tests의 초기화 중에 검증돼요. 부합하지 않는 값이 있으면 검사가 실패해요. 하지만 예시에서 볼 수 있듯 배열의 개별 요소에 대한 대입은 검사를 일으키지 않아요. (배열이나 레코드 같은) 복잡한 데이터 구조의 초기화가 단일 대입으로 수행되지 않을 수 있으므로 이 시점에서는 일관성을 검사할 수 없어요. 하지만 객체가 인자로 서브프로그램에 전달되는 즉시, 서브프로그램이 객체의 일관성을 요구하므로 동적 술어가 검사돼요. 이는 예시의 마지막 Display_Tests 호출에서 발생해요. 여기서 이전 대입이 부합하지 않는 값을 가지므로 술어 검사가 실패해요.
타입 불변식 (Type invariants)
타입 불변식은 타입에 대한 기대를 지정하는 또 다른 방법이에요. 술어는 비-비공개(non-private) 타입에 사용되는 반면, 타입 불변식은 비공개(private) 타입에 대한 기대를 정의하는 데만 전용으로 사용돼요. 패키지 P의 타입 T가 타입 불변식을 가지면, 타입 T의 객체에 대한 연산 결과는 항상 그 불변식과 일관적이에요.
타입 불변식은 with Type_Invariant => <property> 절로 지정돼요. 술어처럼 property 는 타입 T의 객체가 그 요구사항에 부합하는지 검사할 수 있게 해주는 조건을 정의해요. 이런 의미에서 타입 불변식을 비공개 타입용의 일종의 술어로 볼 수 있어요. 하지만 검사 측면에서 몇 가지 차이가 있어요. 다음 표가 차이를 요약해요:
| 요소 (Element) | 서브프로그램 매개변수 검사 (Subprogram parameter checks) | 대입 검사 (Assignment checks) |
|---|---|---|
| 술어 (Predicates) | 모든 in 및 out 매개변수 (On all in and out parameters) |
대입 및 명시적 초기화 시 (On assignments and explicit initializations) |
| 타입 불변식 (Type invariants) | 같은 공개 스코프에 선언된 서브프로그램에서 반환된 out 매개변수 (On out parameters returned from subprograms declared in the same public scope) |
모든 초기화 시 (On all initializations) |
이전 예시를 다시 작성하고 동적 술어를 타입 불변식으로 바꿀 수 있어요. 이렇게 보일 거예요:
with Ada.Text_IO; use Ada.Text_IO;
with Ada.Calendar; use Ada.Calendar;
with Ada.Containers.Vectors;
with Ada.Strings.Unbounded;
use Ada.Strings.Unbounded;
procedure Show_Type_Invariant is
package Courses is
type Course is private
with Type_Invariant => Check (Course);
type Course_Container is private;
procedure Add (CC : in out Course_Container;
C : Course);
function Init
(Name : String;
Start_Date, End_Date : Time)
return Course;
function Check (C : Course)
return Boolean;
private
type Course is record
Name : Unbounded_String;
Start_Date : Time;
End_Date : Time;
end record;
function Check (C : Course)
return Boolean is
(C.Start_Date <= C.End_Date);
package Course_Vectors is new
Ada.Containers.Vectors
(Index_Type => Natural,
Element_Type => Course);
type Course_Container is record
V : Course_Vectors.Vector;
end record;
end Courses;
package body Courses is
procedure Add (CC : in out Course_Container;
C : Course) is
begin
CC.V.Append (C);
end Add;
function Init
(Name : String;
Start_Date, End_Date : Time)
return Course is
begin
return
Course'(Name =>
To_Unbounded_String (Name),
Start_Date => Start_Date,
End_Date => End_Date);
end Init;
end Courses;
use Courses;
CC : Course_Container;
begin
Add (CC,
Init (Name =>
"Intro to Photography",
Start_Date =>
Time_Of (2018, 5, 1),
End_Date =>
Time_Of (2018, 5, 10)));
-- This should trigger an error in the
-- type-invariant check
Add (CC,
Init (Name =>
"Intro to Video Recording",
Start_Date =>
Time_Of (2019, 5, 1),
End_Date =>
Time_Of (2018, 5, 10)));
end Show_Type_Invariant;
주요 차이는 이전 예시에서 Course 타입이 Courses 패키지의 보이는(공개) 타입이었지만, 이 예시에서는 비공개 타입이라는 점이에요.