행동하위태핑

Behavioral subtyping

객체지향적 프로그래밍에서, 행동적 서브타이핑은 서브클래스가 통사적 안전성("방법 미발견" 오류의 부재 등)뿐만 아니라 행동적 정확성에 관해서도, 슈퍼클래스 타입의 참조를 통해 서브클래스 객체에 접근하는 클라이언트의 기대를 만족시켜야 한다는 원칙이다.구체적으로는 객체의 추정형식의 사양을 사용하여 클라이언트가 증명할 수 있는 속성은 객체가 실제로 해당 유형의 하위형식의 구성원이더라도 보유해야 한다.[1]

예를 들어, 요소를 추가하는 put 메서드와 요소를 제거하는 get 메서드가 모두 있는 Stack 유형과 Queue 유형을 고려해 보십시오.이러한 형식과 관련된 문서가 스택에 대해 형식 스택의 방법이 예상대로 작동해야 하며(즉, 후 입선 출 동작을 나타내야 함), 형식 큐의 방법은 대기열에 대해 예상된 대로 작동해야 함(즉, 선입 선출 동작을 나타내야 함)을 명시한다고 가정합시다.이제 해당 유형의 Stack이 Queue 유형의 하위 클래스로 선언되었다고 가정해 보십시오.대부분의 프로그래밍 언어 컴파일러는 설명서를 무시하고 형식 안전을 유지하는 데 필요한 검사만 수행한다.각 대기열 유형의 메서드에 대해 Stack은 이름과 서명이 일치하는 메서드를 제공하므로, 이 검사는 성공할 것이다.그러나 큐 유형의 참조를 통해 스택 객체에 액세스하는 클라이언트는 큐의 설명서에 따라 FIFO 동작을 예상하지만 LIFO 동작을 관찰하여 이러한 클라이언트의 정확성 증명을 무효화하고 잠재적으로 프로그램 전체의 잘못된 동작을 유발할 수 있다.

Stack 타입이 Queue 타입의 동작 하위 타입이 아니기 때문에 이 예는 동작 하위 타입을 위반한다. Stack 타입의 문서에 의해 기술된 동작(즉, LIFO 동작)이 타입 Queue의 문서화(FIFO 동작이 필요함)를 준수하는 경우는 아니다.

이와는 대조적으로, 스택과 큐가 모두 Bag 타입의 하위 클래스인 프로그램은, 단지 어떤 요소를 제거한다는 것을 얻는 것에 대한 사양이, 행동적 서브타이핑을 만족시키고, 고객들이 그들이 상호작용하는 개체의 추정된 유형에 근거하여 수정성에 대해 안전하게 논할 수 있게 해준다.실제로 스택 또는 큐 사양을 충족하는 모든 물체는 백 사양을 만족한다.

유형 S가 유형 T의 행동적 하위 유형인지 여부는 유형 T의 규격(즉 문서)에만 의존한다는 점을 강조하는 것이 중요하다. 유형 T의 구현은, 유형 T가 있다면, 이 질문과는 완전히 무관하다.사실, T형은 실행조차 할 필요가 없다; 그것은 순전히 추상적인 클래스일 수도 있다.또 다른 사례로, 위의 Stack 타입은 Bag 타입의 구현이 FIFO 행동을 나타내더라도 Bag 타입의 행동 하위 타입이다. 중요한 것은 Bag 타입의 사양에 의해 어떤 요소가 제거되었는지 명시하지 않는다는 것이다.이는 또한 관련된 각 유형에 대한 특정 (행동적) 규격에 대해서만 행동적 하위 유형을 논의할 수 있으며, 관련된 유형이 잘 정의된 행동 규격이 없는 경우 행동적 하위 유형을 의미 있게 논의할 수 없다는 것을 의미한다.

동작 하위 유형 확인

S타입은 S사양서에 의해 허용되는 각 동작이 T사양에도 의해 허용되는 경우 T타입의 동작 하위타입이다.이것은 특히 T의 각 방법 M에 대해 S의 M 사양이 T의 방법보다 강하다는 것을 요구한다.

전제조건 P와s 사후조건 Q가s 제시한 방법 명세서는 P가s P보다t 약하고(즉t, P가 P를s 내포함), Q가s Q보다t 강한 경우t(즉ts Q가 Q를 내포함) 전제조건 P와tt 사후조건 Q(공식적으로 Ps, Q)가st 제시한 방법 명세보다 강하다.즉, 사후조건을 강화하고 전제조건을 약화시킴으로써 방법사양을 강화할 수 있다.실제로 방법 규격은 이미 지원되는 입력에 대해 출력에 더 구체적인 제약조건을 부과하거나 또는 더 많은 입력을 지원해야 하는 경우에 더 강하다.

예를 들어 전제 조건 0 ≤ x와 사후 조건 0 ≤ 결과를 지정하는 인수 x의 절대값을 계산하는 방법에 대한 (매우 약한) 규격을 고려하십시오.이 규격은 이 방법이 x에 대한 음수 값을 지원할 필요는 없으며, 결과가 음수가 아니라는 것만 확인하면 된다고 말한다.이 규격을 강화하는 두 가지 가능한 방법은 상태 결과 = x, 즉 결과가 x의 절대값과 같거나 전제조건을 "참"으로 약화시켜 x에 대한 모든 값이 지원되어야 한다는 것이다.물론, 우리는 두 가지 모두를 x의 어떤 값에 대해서도 x의 절대값과 같아야 한다는 명세서로 결합할 수 있다.

단, 사후 조건(Qs ⇏ Qt)을 강화하지 않고 사양(Ps, Q) ⇒(Pt, Qst)을 강화할 수 있다는 점에 유의한다.[2][3]전제 조건 0 ≤ x와 사후 조건 결과 = x를 지정하는 절대값 방법에 대한 규격을 고려한다.전제 조건 "참"과 사후 조건 결과 = x를 지정하는 규격은 사후 조건 결과 = x를 강화(또는 약화)하지 않더라도 이 규격을 강화한다.전제조건 P와s 사후조건 Q를s 가진 명세가t 전제조건 P와t 사후조건 Q를 가진 명세서보다 강해야 할 필요조건은st P가 P보다 약하고 "Qss 또는 not P"가 "Qtt 또는 not P"보다 강하다는 것이다.실제로 "결과 = x 또는 거짓"은 "결과 = x 또는 x < 0"을 강화한다.

"대체 가능성"

데이터 추상화, 클래스 계층에 OOPSLA 1987년 프로그래밍 언어 연구 회의에서 영향력 있는 기조 address[4]에서, 바바라 Liskov은:"다음 대체 부동산과 같은 뭐 여기 일입니다:만약 1{\displaystyle o_{1}마다 각 개체에 대해}형 S의 개체 o2는 다음과 같이 말했다 {)T형식의 o1{\1}}{을 2S를 대신할 때 P의 동작은 변하지 않는다."이 특성화는 이후 리스크노프 대체 원리(LSP)로 널리 알려져 왔다.하지만 불행하게도, 그것은 몇 가지 문제가 있다.첫째로, 그것의 원래 형태에서, 그것은 너무 강하다: 우리는 하위 클래스의 행동이 슈퍼클래스의 그것과 동일하기를 거의 원하지 않는다; 하위 클래스 객체를 슈퍼클래스 객체로 대체하는 것은 비록 행동 하위 타이핑이 존중된다면, 프로그램의 desir를 유지하는 방식으로 프로그램의 행동을 변화시키려는 의도로 종종 행해진다.유능한 재산둘째, 사양에 대한 언급은 하지 않기 때문에 S형의 구현을 T형의 구현과 비교하는 잘못된 판독을 유도한다.이것은 여러 가지 이유로 문제가 있는데, 하나는 T가 추상적이고 실행이 없는 일반적인 경우를 지원하지 않기 때문이다.셋째로, 그리고 가장 미묘하게, 객체지향적 명령 프로그래밍의 맥락에서, 주어진 유형의 물체에 대해 보편적으로 또는 실존적으로 수량화하거나, 한 물체를 다른 물체로 대체하는 것이 무엇을 의미하는지를 정확하게 정의하기는 어렵다.[3]위의 예에서 우리는 Stack 객체를 Bag 객체로 대체하는 것이 아니라 Stack 객체를 Bag 객체로 사용하는 것이다.

리스크노프 자신은 2016년 인터뷰에서 기조연설에서 제시했던 것이 '비공식 규칙'이었고, 이후 제넷 윙이 '이것이 무엇을 의미하는지를 정확히 파악하려고 노력하라'고 제안해 '행동적 서브타이핑'에 대한 공동출판을[1] 이끌어냈고, 실제로 '기술적으로 '행동적 서브타이핑'이라고 불린다'[5]고 설명했다.인터뷰 동안, 그녀는 개념을 논하기 위해 대체 용어를 사용하지 않는다.

메모들

  1. ^ a b Liskov, Barbara; Wing, Jeannette (1994-11-01). "A behavioral notion of subtyping". ACM Transactions on Programming Languages and Systems. 16 (6): 1811–1841. doi:10.1145/197320.197383.
  2. ^ Parkinson, Matthew J. (2005). Local reasoning for Java (PDF) (PhD). University of Cambridge.
  3. ^ a b Leavens, Gary T.; Naumann, David A. (August 2015). "Behavioral subtyping, specification inheritance, and modular reasoning". ACM Transactions on Programming Languages and Systems. 37 (4). doi:10.1145/2766446.
  4. ^ Liskov, B. (May 1988). "Keynote address - data abstraction and hierarchy". ACM SIGPLAN Notices. 23 (5): 17–34. doi:10.1145/62139.62141.
  5. ^ van Vleck, Tom (April 20, 2016). Interview with Barbara Liskov. ACM. Archived from the original on 2021-12-21.

참조

  • Parkinson, Matthew J.; Bierman, Gavin M. (January 2008). "Separation logic, abstraction and inheritance". ACM SIGPLAN Notices. 43 (1): 75–86. doi:10.1145/1328897.1328451.