본 논문에서는, 자바 바이트 코드 검증을 위해 설계된 중간 표현 언어인 BIRS(Bytecode Intermediate Representation with Specification)생성기 JBVF(Java Bytecode Verification Framework)를 확장한다. JBVF를 통해 생성된 BIRS는 검증 조건 생성을 위해 자바 소스 코드(하이레벨)가 공개 되었을 경우에도 프로그래머가 BIRS(로우레벨)에 직접 명세 정보를 기술해 주어야 한다. 이를 해결하기 위해, 자바 소스 코드가 공개되었을 경우 자바 소스 코드에 입력된 명세 정보를 이용하여 BIRS 코드를 생성하는 방법을 소개한다. BIRS 코드는 JML2BML도구와 JML, BML을 이용하여 생성한다. BML을 입력으로 받아 생성된 BIRS에 명세 정보가 정확히 표현되었는지 확인한다.
In this paper we extend JBVF(Java Bytecode Verification Framework). JBVF generates and verifies BIRS(Bytecode Intermediate Representation with Specification) which is an intermediate language for verifying bytecodes. When BIRS codes are genereted by JBVF, even though a programmer has java source codes(high level) annotated with specifications, he should describe specification information in BIRS codes(low level) for generation of verification conditions from BIRS codes. We present the way to generate BIRS codes from java codes annotated with specification information, when java source codes are available. We present how BIRS code is generated from BML. BML could be generated from JML by a tool JML2BML. We certify that specification information in BIRS from BML is correctly generated.
