프로그래밍언어논문지 제16권 제2호 (2002년)

권두언: [.PDF 327KB]

논문

• 계층형 명세 언어의 정의 및 검사
  박사천, 권기현
• 구조비교를 위한 단백질 데이터의 XML 표현기법
  김진홍, 안건태, 이수현, 이명준
• JNI 함수 호출을 통한 C에서의 자바 배열 객체 사용
  이창환, 오세만
• G-machine과 ZG-machine의 그래프 합동
  우균

튜토리얼

• 다익스트라의 '프로그래밍의 수련(修練)': 일곱 번째,
  적절히 종료하는 구조의 설계에 대하여
  김도형

본문

계층형 명세 언어의 정의 및 검사 [.PDF 2924KB]

• 저자: 박사천, 권기현
• 요약:
  시스템 정형검증의 한 분야로 모형검사 방법이 활발히 연구되어 왔다. 왜냐하면 모형검사 방법은 사용자의 개입 없이 자동적으로 검증을 할 수 있기 때문이다. 그러나 모형검사에는 몇 가지 문제점이 있다. 그 중 가장 심각한 것이 상태폭발 문제이다. 상태폭발로 인해서 모형검사기는 큰 규모의 시스템들을 다루지 못한다. 시스템은 명세 단계에서 계층적으로 명세 되는 반면 검증 단계에서는 계층성을 잃고 평탄화 된다. 이렇게 평탄화 될 경우 전이의 수와 상태의 수가 폭발적으로 늘어나게 된다. 본 연구는 평탄화에 의해 발생하는 상태폭발의 문제를 극복하기 위하여, 계층형 크립키 구조를 정의하고 그 구조에서 CTL 속성을 검사하는 모형검사 알고리즘을 제시한다.

구조비교를 위한 단백질 데이터의 XML 표현기법 [.PDF 4416KB]

• 저자: 김진홍, 안건태, 이수현, 이명준
• 요약:
  현재의 단백질 구조비교 시스템들은 구조비교를 위하여 자신들의 알고리즘에 맞는 고유한 형식의 데이터를 이용하고 있으며, 이에 따라 호환성이나 상호작용성에 문제를 드러내게 되었다. 따라서, 이러한 문제를 해결하여 단백질 구조를 비교하는 시스템을 신속히 개발하기 위해서는 단백질 3차 구조를 표현하기 위한 데이터를 추출하여 XML과 같은 표준 형식으로 기술된 데이터를 제공하는 것이 바람직하다. 본 논문에서는 단백질 구조 및 유사성을 비교하기 위한 단백질 데이터의 XML 표현기법인 PSAML에 대하여 기술한다. PSAML은 단백질의 이차구조 구성요소와 그들 사이의 관계를 이용하여 단백질 구조를 기술하는 PSA라는 단백질 구조 모델을 이용하여 설계되었다.

JNI 함수 호출을 통한 C에서의 자바 배열 객체 사용 [.PDF 1676KB]

• 저자: 이창환, 오세만
• 요약:
  JNI는 자바와 네이티브 코드간에 상호 연동을 위해서 정의된 인터페이스이다. JNI를 이용하면 C/C++에서 자바 객체를 사용할 수 있다. 하지만 C/C++에서 자바 객체에 대한 연산을 위해서는 연산에 필요한 JNI 함수 호출을 사용자가 기술해야 한다. 사용자가 직접 기술하는 경우, 사용자는 JNI 함수의 잘못된 사용으로 오류 발생 가능성이 높아지고 JNI의 복잡한 사용 방법을 익혀야 하는 문제점이 있다. 본 논문에서는 자바에서 인덱스 연산자("[]")를 사용하여 배열 객체에 대해 연산하는 것처럼 C에서도 인덱스 연산자를 사용하여 자바 배열 객체에 대한 연산할 수 있는 방법을 제안하고 구현하였다. 제안된 방법을 통한 배열 객체 사용은 JNI를 통해 자바 배열 객체 사용할 때보다 복잡성을 줄여 오류가 발생할 가능성을 줄일 수 있다.

G-machine과 ZG-machine의 그래프 합동 [.PDF 351KB]

• 저자: 우균
• 요약:
  이 논문은 지연 함수형 언어를 위한 추상기계 G-machine과 ZG-machine의 동작이 동등함에 대하여 논한다. ZG-machine은 공간 효율을 높이기 위해 태그 옮김이라는 기법을 통해 G-machine을 변형한 추상기계이다. ZG-machine에서는 그래프 생성방법을 변경하였으므로 해석 방법도 G-machine과 다르게 되는데, 그럼에도 불구하고 G-machine과 ZG-machine은 같은 의미의 동작을 수행한다는 것을 보이고자 한다. 이를 위해 이 논문에서는 두 추상기계 수행시 메모리에 저장되는 그래프 형태를 의미 도메인상의 원소를 기술하고, 같은 프로그램에 대하여 두 추상기계에서 상태 변환 과정 중의 그래프 형태가 같은 의미라는 것을, 즉 그래프 합동이라는 것을 보인다.

다익스트라의 '프로그래밍의 수련(修練)': 일곱 번째,
적절히 종료하는 구조의 설계에 대하여 [.PDF 1661KB]

• 저자: 김도형
• 요약:
  이번 튜토리얼에서는 앞장에서 논의한 '반복 구조를 위한 기본 정리'의 결론이 되는 함축의 전제 중 일부인 wp(DO, T)에 관해 보다 깊게 논의한다. 비록 이것이 의미하는 바가 직관적으로는 단순히 '반복 구조가 종료할 최약 사전 조건'으로 간단하지만, 임의의 DO 구조가 주어졌을 때 이러한 조건을 구하는 것은 일반적으로 매우 어렵다. 따라서 반복 구조를 구성할 때 아예 처음부터 종료에 대한 조건을 염두에 두고 설계하는 것이 현실적인 방법이 된다. 기본적인 착상은 단순하다. 각각의 반복 구조에 대해 반복되는 동안 음이 아닌 값을 유지하면서 동시에 매 반복마다 1 이상 값이 감소되는 정수 함수를 하나씩 연계시키는 것이다. 이러한 함수가 관련 정리들의 전제를 모두 만족한다면, 거기에 대응되는 반복 구조는 적절히 종료하게 된다.