One way of improving software system’s reliability is to let developers know the usage protocol of system and enforce them to follow the protocol. Hoare’s pre-/post-condition style specification for software system can precisely present the usage protocol of system, but it describes the protocol implicitly. Typestates are a more intuitive and abstract way of presenting pre/post-conditions for a usage protocol for Object-Oriented Program. Thus, developers can employ the concept of Typestates to specify and verify usage protocols of OOP system instead of pre/post-conditions. There are a few supports on Typestates protocols whereas many support on pre-/post-condition specification system in terms of tooling.
In this paper, we propose to use Typestates to specify and verify the behavior of a type (i.e. an interface or a class), based on previous research on Typestates protocol specification [6][15]. To do this, we present a set of formal translation rules for encoding Typestates protocol specification into pre/post-condition spe-cification, and illustrate our generic strategy with applying it to specific OOP language, Java/JML. We present a way of supporting mixing Typestates proto-col specification with pre/post-condition specification. We also show how we handle the violation of code contract in inheritance that make our approach to mix two specification methodology consistently. In addition, we evaluate our approach with Java/JML environment to show the usefulness of our approach.
소프트웨어 시스템의 신뢰도를 높이는 방법 중 하나는 개발자들이 시스템에 대한 사용규약(usage protocol)을 이해하고 규약을 따르도록 하는 것입니다. 호어(C. A. Hoare)의 사전/사후 조건(pre/post-condition)은 시스템의 사용규약을 정확하게 표현합니다. 그러나 사용규약을 명시적으로 묘사하지는 못합니다. 타입스테이트는 객체지향 프로그래밍에 있어서 사용규약에 대한 사전/사후 조건을 좀 더 직관적이고 추상적으로 표현할 수 있는 방법입니다. 그러므로, 개발자는 이를 이용하여 사전/사후 조건 대신 객체지향 시스템에 대한 사용규약을 명세화하고 검증하는데 타입스테이트 개념을 사용할 수 있습니다. 현재 사전/사후 방식의 명세화 시스템에 대한 지원은 다양한 데 반해 타입스테이트에 대한 지원은 미비합니다.
이 연구에서는 이전에 논의된 타입스테이트 규약 명세화 연구 방법에 기반하여 타입의 행위(behavior)를 명세하고 검증하는데 타입스테이트를 사용합니다 [6][15]. 이를 위해서 타입스테이스 사용규약 명세를 사전/사후조건 명세로 번역하는 규칙을 포함한 접근법을 제공하며, 자바(Java)/JML와 같은 특정 객체지향 언어에 적용하는 구체적인 접근법도 제공합니다. 또한 사전/사후 조건 명세와 타입스테이트 사용규약 명세가 혼용될 수 있는 방법을 제시합니다. 그리고, 상속 개념을 위배하는 경우, 두 명세가 일관성(consistency)을 유지할 수 있도록 하기 위한 해결책을 제시하고 있습니다. 끝으로, 이 연구에서 제시한 접근법이 자바(Java)/JML 환경에서 어떻게 유용하게 이용할 수 있는지를 보여주어 접근법에 대한 평가를 제시합니다.
