| 1 |
1
자바 프로그램 검증 조건 생성 시스템에 있어서,자바 프로그램 중간 표현 언어를 저장하는 자바 중간 표현 언어 저장소;상기 자바 중간 표현 언어로부터 제어 흐름 그래프를 생성하는 제어 흐름 그래프 생성부;상기 제어 흐름 그래프로부터 기본 경로를 추출하는 기본 경로 추출부; 및상기 기본 경로로부터 검증 조건을 생성하는 검증 조건 생성부;를 포함하는 자바 프로그램 검증 조건 생성 시스템
|
| 2 |
2
제 1 항에 있어서,상기 자바 프로그램 중간 표현 언어는 프로그램 검증을 위한 전조건, 후조건, 및 루프불변자를 포함하는 명세 정보를 입력한 자바 프로그램 소스 파일을 변환하여 생성되는 것이며상기 명세 정보 입력에는 JML(Java Modeling Language) 문법이 사용되는 자바 프로그램 검증 조건 생성 시스템
|
| 3 |
3
제 1 항에 있어서,상기 자바 프로그램 중간 표현 언어는 자바 프로그램 바이트코드 파일을 변환하여 생성되는 것인 자바 프로그램 검증 조건 생성 시스템
|
| 4 |
4
제 1 항에 있어서,상기 제어 흐름 그래프는 상기 자바 프로그램 중간 표현 언어의 각 블록을 노드(node)로 하고, 분기를 간선(edge)으로 하는 순서가 있는 그래프이며,상기 간선에는 상기 분기시 만족해야 하는 조건이 포함되는 자바 프로그램 검증 조건 생성 시스템
|
| 5 |
5
제 2 항에 있어서,상기 제어 흐름 그래프의 시작 노드는 상기 전조건을 나타내고, 종료 노드는 상기 후조건을 나타내도록 구성되는 자바 프로그램 검증 조건 생성 시스템
|
| 6 |
6
제 1 항에 있어서,상기 기본 경로는 상기 제어 흐름 그래프의 시작 노드 또는 루프불변자 블록을 나타내는 노드로부터 시작되고,상기 제어 흐름 그래프의 종료 노드, 단언(assert) 블록을 나타내는 노드 또는 루프불변자 블록을 나타내는 노드에서 끝나며,상기 제어 흐름 그래프를 깊이 우선 탐색하여 추출되는 자바 프로그램 검증 조건 생성 시스템
|
| 7 |
7
제 1 항에 있어서,상기 제어 흐름 그래프의 간선에 포함되어 있는 조건은 상기 기본 경로에서 가정(assume) 표현식으로 변환되는 자바 프로그램 검증 조건 생성 시스템
|
| 8 |
8
제 1 항에 있어서,상기 검증 조건 생성부는 최약 전조건(weakest precondition) 계산 함수를 사용하여 상기 검증 조건을 생성하며,상기 최약 전조건 계산 함수는 상기 기본 경로에 포함되어 있는 각 표현식을 인수로 하여 순환 호출되는 자바 프로그램 검증 조건 생성 시스템
|
| 9 |
9
제 8 항에 있어서,상기 최약 전조건 계산 함수는 상기 순환 호출시 상기 기본 경로의 끝에 있는 표현식을 초기 후조건 인수로 받는 자바 프로그램 검증 조건 생성 시스템
|
| 10 |
10
자바 프로그램 검증 조건 생성 시스템을 이용한 자바 프로그램 검증 조건 생성 방법에 있어서,자바 중간 표현 언어로부터 제어 흐름 그래프를 생성하는 단계;상기 제어 흐름 그래프로부터 기본 경로를 추출하는 단계; 및상기 기본 경로로부터 검증 조건을 생성하는 단계;를 포함하는 자바 프로그램 검증 조건 생성 방법
|
| 11 |
11
제 10 항에 있어서,상기 제어 흐름 그래프는 상기 자바 프로그램 중간 표현 언어의 각 블록을 노드(node)로 하고, 분기를 간선(edge)으로 하는 순서가 있는 그래프이며,상기 간선에는 상기 분기시 만족해야 하는 조건이 포함되는 자바 프로그램 검증 조건 생성 방법
|
| 12 |
12
제 10 항에 있어서,상기 기본 경로는 상기 제어 흐름 그래프의 시작 노드 또는 루프불변자 블록을 나타내는 노드로부터 시작되고,상기 제어 흐름 그래프의 종료 노드, 단언(assert) 블록을 나타내는 노드 또는 루프불변자 블록을 나타내는 노드에서 끝나며,상기 제어 흐름 그래프를 깊이 우선 탐색하여 추출되는 자바 프로그램 검증 조건 생성 방법
|
| 13 |
13
제 10 항에 있어서,상기 검증 조건 생성에는 최약 전조건(weakest precondition) 계산 함수가 사용되며,상기 최약 전조건 계산 함수는 상기 기본 경로에 포함되어 있는 각 표현식을 인수로 하여 순환 호출되는 자바 프로그램 검증 조건 생성 방법
|
