초록 ▼

본 연구의 목적은 소프트웨어가 점차로 더욱 복잡해지고 거대해지는 시점에서 보다 쉽고 효율적인 모듈화 프로그래밍을 지원하기 위해 특정 프로그래밍 언어를 기반으로 하지 않는 범용 고차 모듈 시스템을 개발하여 학부 및 대학원 교육에 이용하고 여러 프로그래밍 언어에 적용해 보임으로써 학계 및 산업계에 보급하는 것이다. 본 연구에서는 이러한 연구 목적을 바탕으로 특정 기반언어에 종속되지 않은 고차 모듈 시스템을 설계, 구현, 검증하였다.
본 연구의 이론적인 측면에서는 고차 모듈 시스템과 모듈 시스템을 차용할 기반언어 사이의 필수적인 연

본 연구의 목적은 소프트웨어가 점차로 더욱 복잡해지고 거대해지는 시점에서 보다 쉽고 효율적인 모듈화 프로그래밍을 지원하기 위해 특정 프로그래밍 언어를 기반으로 하지 않는 범용 고차 모듈 시스템을 개발하여 학부 및 대학원 교육에 이용하고 여러 프로그래밍 언어에 적용해 보임으로써 학계 및 산업계에 보급하는 것이다. 본 연구에서는 이러한 연구 목적을 바탕으로 특정 기반언어에 종속되지 않은 고차 모듈 시스템을 설계, 구현, 검증하였다.
본 연구의 이론적인 측면에서는 고차 모듈 시스템과 모듈 시스템을 차용할 기반언어 사이의 필수적인 연관 관계를 면밀히 분석하고 이를 바탕으로 모듈 시스템과 기반언어를 분리하여 설계하였다. 즉, 어떤 프로그래밍 언어와도 호환될 수 있도록 기반언어의 문법구조와 의미구조를 추상화하여 표현하고 이를 바탕으로 모듈 시스템의 문법구조와 의미구조를 정의하였다. 또한 최종적으로 모듈함수를 비롯한 모든 모듈 요소를 제거하기 위해 경로변환, 모듈함수제거, 모듈제거 기법을 설계하였다. 경로변환 기법은 기반언어에 독립적인 모듈함수제거와 모듈제거 기법을 정의하기위해 필요한 선행기법이다. 모듈함수제거와 모듈제거는 프로그램 실행 중에 모듈언어 처리로 인한 오버헤드가 생기지 않게 함으로써 프로그램의 효율성을 높여준다. 또한 모듈제거 변환은 별도로 모듈 수준에서의 프로그램의 동적 의미구조를 정의하지 않더라도 프로그램을 실행할 수 있게 해준다. 모듈 수준에서의 프로그램의 동적 의미구조를 정의하기 위해서는 기반언어의 동적 의미구조가 어떻게 정의되어 있는지 알고 있어야 하고 이는 범용 모듈 시스템을 설계한다는 연구목적과도 부합되지 않는다. 최종적으로 완성한 고차 모듈 시스템의 의미론과 타입 체계에 대해서 건전성과 완전성을 증명하였다.
본 연구의 구현 측면에서는 기반언와와 모듈 시스템 간의 상호작용이 최소화되도록 하여 기반언어와는 독립된 모듈 시스템을 구현하였다. 구현은 모듈함수를 제공하는 Objective CAML을 이용하였으며, 구현과정은 모듈화 프로그래밍 원칙에 따라 기반언어의 인터페이스만을 정의하고 이를 이용하여 모듈함수의 형태로 고차 모듈 시스템을 구현하였다. 세부적으로는 설계한 고차 모듈 시스템의 타입 검사기와 모든 모듈 관련 언어요소를 제거하는 경로변환기, 모듈함수제거 변환기, 모듈제거 변환기의 세 가지 변환 기법을 구현하였다. 각각의 변환은 순차적으로 적용되었다. 즉, 원천언어는 경로변환 기법의 입력 값이고 그 결과 값은 모듈함수제거 기법의 입력 값이 된다. 모듈함수제거 기법의 결과 값은 다시 모듈제거 기법의 입력 값이 되고 그 결과 값은 기반언어가 된다. 이 세 가지 변환 기법은 작성된 프로그램을 실행시킬 수 있도록 하기 위해 컴파일 타임에 모든 모듈요소를 제거한다. 또한 정의된 모듈 시스템을 적용해볼 프로그래밍 언어들의 핵심 부분을 구현한 뒤 실제로 구현된 모듈 시스템을 적용해보았다. 즉 설계한 모듈 시스템의 범용성을 테스트하기 위해 C 언어의 핵심 부분 집합, 함수형 병렬 프로그래밍 언어, 그리고 함수형 하드웨어 기술언어에 설계한 고차 모듈 시스템을 탑재해보았다.
한편 설계한 모듈 시스템의 안전성의 신뢰도를 높이기 위해서 건전성과 완전성 증명의 전 과정을 Coq 증명 보조기를 이용하여 기계화하였다. Coq으로 모듈 시스템의 안전성 및 완전성 증명을 기계화하기 위해 먼저 증명을 위한 기본 라이브러리를 구축하였다. 또한 이를 이용하여 안전성 및 완전성 정리를 Coq를 이용하여 서술하였다. 마지막으로 서술된 안전성 및 완전성 정리는 Coq을 이용하여 직접 증명하였다. 증명은 cofinite quantification, 지역 변수에 이름을 할당하지 않는 기법, 문맥 자유 타입 규칙과 같은 기법을 이용하여 진행하였다.
본 연구를 통해 개발한 범용 프로그래밍 언어를 위한 고차 모듈 시스템은 특정 기반언어에 종속되지 않는다는 점에서 학문적으로 큰 의의를 갖는다. 개발한 고차 모듈 시스템은 아직 프로토타입에 불과 하지만 향후에 다양한 언어 요소를 추가하는 등 수정 보완하여 산업계에 보급하면 모듈화 프로그래밍을 통해 소프트웨어 개발 생산성을 높이는 데 크게 일조할 수 있을 것으로 기대된다.

목차 Contents

• 일반연구자지원사업 최종(결과)보고서 ... 1
• 목차 ... 3
• I. 연구결과 요약문 ... 4
• II. 연구내용 및 결과 ... 5
• 1. 연구과제의 개요 ... 5
• 2. 국내외 기술개발 현황 ... 5
• 3. 연구수행 내용 및 결과 ... 6
• 4. 목표 달성도 및 관련 분야에의 기여도 ... 6
• 5. 연구결과의 활용 계획 ... 7
• 6. 연구과정에서 수집한 해외과학기술정보 ... 7
• III. 연구성과 ... 9