대수적 명세

Algebraic specification

대수 규격은[1][2][3][4] 시스템 동작을 공식적으로 명시하기 위한 소프트웨어 엔지니어링 기법이다.1980년경 CS 연구의 매우 활발한 주제였다.[5]

개요

대수 규격은 다음을 통해 보다 효율적인 프로그램을 체계적으로 개발하고자 한다.

  1. 공식적으로 데이터 유형 및 해당 데이터 유형에 대한 수학적 연산 정의
  2. (메모리 내) 표현 크기 및 계산 결과의 획득 효율성과 같은 구현 세부사항 추상화
  3. 데이터 유형에 대한 연산 및 연산 공식화
  4. 이러한 제한된 동작 및 데이터 유형으로 운영을 공식적으로 제한함으로써 자동화를 허용한다.

대수 규격은 하나 이상의 데이터 유형을 정의하고 해당 데이터 형식에서 작동하는 함수의 컬렉션을 지정함으로써 이러한 목표를 달성한다.이러한 기능은 다음과 같은 두 가지 등급으로 나눌 수 있다.

  1. 생성자 함수: 데이터 요소를 생성하거나 초기화하거나, 단순한 요소로부터 복잡한 요소를 구성하는 함수
  2. 추가 함수: 데이터 유형에서 작동하며 생성자 함수의 관점에서 정의되는 함수.

예

부울 데이터 형식에 대한 공식 대수적 규격을 고려한다.

하나의 가능한 대수 규격은 데이터 요소에 대해 두 가지 생성자 함수, 즉 참 생성자와 거짓 생성자를 제공할 수 있다.따라서 부울 데이터 요소를 선언, 생성 및 값으로 초기화할 수 있었다.이 시나리오에서 XOR와 AND와 같은 다른 모든 결합 요소는 추가 기능일 것이다.따라서 데이터 요소는 "참" 또는 "거짓" 값으로 인스턴스화할 수 있으며, 데이터 요소에 대한 작업을 수행하는 데 추가 기능을 사용할 수 있다.

또는 다른 생성자 함수 집합인 거짓 생성자와 비 생성자를 사용하여 부울 데이터 유형의 전체 시스템을 지정할 수 있다.이 경우, "참" 값을 산출하는 추가 함수를 정의할 수 있다.

따라서 대수 규격은 데이터 요소의 모든 가능한 상태와 상태 간의 모든 가능한 전환을 설명한다.

참고 항목

메모들

  1. ^ Ehrig, Hartmut; Mahr, Bernd (1989). Algebraic Specification. Academic Press. ISBN 0-201-41635-2.
  2. ^ Bergstra, J.A.; Heering, J.; Klint, J. (1985). Algebraic Specification. EATCS Monographs on Theoretical Computer Science. Vol. 6. Springer-Verlag.
  3. ^ Wirsing, Martin (1990). Jan van Leeuwen (ed.). Algebraic Specification. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 675–788.
  4. ^ Sannella, Donald; Tarlecki, Andrzej (2012). Foundations of Algebraic Specification and Formal Software Development. EATCS Monographs on Theoretical Computer Science. Springer-Verlag. ISBN 978-3-642-17335-6.
  5. ^ Wagner, Eric G. (December 2002). "Algebraic specifications: some old history and new thoughts". Nordic Journal of Computing. 9 (4): 373–404. ISSN 1236-6064.


Stub icon

이 컴퓨터 과학 기사는 단조롭다.위키피디아를 확장하여 도울 수 있다.