Larch 명세 언어의 정형적 의미론 = Formal Semantics of Larch Specification Languages (An Extended Abstract)

국문 초록 (Abstract)

정형적 인터페이스 명세는 프로그램 모듈에 관한 모호성이 배제된 정확한 문서이다. 정형성은 명세 언어와 같은 정형적 표기법이 수학을 바탕으로하는 정형적 의미를 갖고 있기 때문에 가능하다. 본 논문에서는 양층형 방식의 Larch 인터페이스 명세 언어의 정형적 의미론을 정립한다. 특히 객체지향을 지원하는 Larch/Smalltalk을 중심으로 하여 모델지향적 및 증명론적 의미을 정의한다. 모델지향적 방법은 직관적이고 풍부한 수학적 이론을 바탕으로 하기 때문에 명세의 의미를 쉽게 파악할 수 있게 한다. 반면 증명론적 방법은 정형적 분석 및 증명을 위한 토대를 제공한다. 즉, 주어진 프로그램이 명세를 만족하는가 하는 정형적 증명 및 프로그램에 관한 추론을 용이하게 한다.

목차 (Table of Contents)

• 요약
• 1. 개요
• 2. 기본 개념과 모델
• 3. 모델지향적 의미론
• 4. 증명론적 의미론
• 5. 결론
• 참고 문헌