동작적 의미론
(연산 의미론에서 넘어옴)
동작적 의미론(operational semantics)은 용어에 수학적 의미를 부여하는 대신 실행 및 절차에 대한 논리적 설명을 통해 증명을 구성하여 정확성, 안전성 또는 보안과 같은 프로그램의 원하는 특정 속성을 검증하는 형식적인 프로그래밍 언어 의미론의 범주이다. (표시적 의미론) 동작적 의미론은 두 가지 범주로 분류된다. 구조적 동작적 의미론(작은 단계 의미론)은 컴퓨터 기반 시스템에서 계산의 개별 단계가 어떻게 발생하는지 공식적으로 설명한다. 반대로 자연 의미론(큰 단계 의미론)은 실행의 전체 결과를 얻는 방법을 설명한다. 프로그래밍 언어의 형식적 의미론을 제공하는 다른 접근 방식에는 공리적 의미론과 표시적 의미론이 포함된다.
프로그래밍 언어의 동작적 의미론은 유효한 프로그램이 일련의 계산 단계로 해석되는 방식을 설명한다. 이러한 시퀀스는 프로그램의 의미이다. 함수형 프로그래밍의 맥락에서 종료 시퀀스의 마지막 단계는 프로그램의 값을 반환한다. (일반적으로 프로그램이 비결정적일 수 있기 때문에 단일 프로그램에 대해 많은 반환 값이 있을 수 있으며, 결정적 프로그램의 경우에도 의미론이 해당 값에 도달하는 작업 순서를 정확히 지정하지 않을 수 있으므로 계산 순서가 많을 수 있다.)
아마도 동작적 의미론의 최초의 공식적인 구현은 리스프의 의미론을 정의하기 위해 람다 미적분학을 사용한 것일 것이다.[1] SECD 머신 전통의 추상 기계도 밀접하게 관련되어 있다.
같이 보기
[편집]각주
[편집]- ↑ McCarthy, John. “Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I”. 2013년 10월 4일에 원본 문서에서 보존된 문서. 2006년 10월 13일에 확인함.
외부 링크
[편집]
위키미디어 공용에 동작적 의미론 관련 미디어 분류가 있습니다.
