ESC/자바
ESC/Java |
ESC/Java(그리고 최근에는 ESC/Java2)인 "Extended Static Checker for Java"는 컴파일 시간에 자바 프로그램에서 일반적인 런타임 오류를 찾으려고 시도하는 프로그래밍 툴이다.[1]ESC/Java에서 사용되는 기본 접근방식을 확장 정적 점검이라고 하며, 이는 다양한 프로그램 제약조건의 정확성을 정적으로 점검하기 위한 다양한 기법을 지칭하는 집합적 명칭이다.예를 들어 정수 변수가 0보다 크거나 배열의 경계 사이에 있는 경우.이 기법은 ESC/Java(및 그 전신인 ESC/Modula-3)에서 개척되었으며, 형식 확인의 확장된 형태라고 생각할 수 있다.확장된 정적 점검은 대개 자동화된 정리 프로베론의 사용을 포함하며, ESC/Java에서는 Simplified 정리 프로베러를 사용하였다.
ESC/Java는 소리가 나지도 않고 완전하지도 않다.이는 의도적이었으며, 실제로 도구를 보다 유용하게 만들기 위해 프로그래머에게 보고된 오류 및/또는 경고의 수를 줄이는 것을 목적으로 한다.그러나 이는 다음과 같은 것을 의미한다: 첫째, ESC/Java가 잘못된 것으로 잘못 간주하는 프로그램(허위 긍정 프로그램이라고 함)이 있고, 둘째, 정확하다고 간주할 잘못된 프로그램(허위 부정 프로그램이라고 함)이 있다.후자 범주의 예로는 모듈식 산술 및/또는 멀티스레딩에서 발생하는 오류를 들 수 있다.
ESC/Java는 원래 Compaq Systems Research Center(SRC)에서 개발되었으며, SRC는 원래 확장 정적 체커인 ESC/Modula-3에 대한 작업이 1996년에 종료된 후 1997년에 이 프로젝트를 시작했다.2002년에 SRC는 ESC/Java 및 관련 도구에 대한 소스 코드를 발표했다.ESC/Java의 최근 버전은 JML(Java Modeling Language)을 기반으로 한다.사용자들은 특별하게 포맷된 주석이나 실용주의로 프로그램에 주석을 달아서 체크의 양과 종류를 조절할 수 있다.
Nijmegen 대학의 시스템 보안 그룹은 2004년까지 JML 사양 언어를 처리하는 ESC/Java의 확장 버전인 ESC/Java2의 알파 버전을 발표했다.2004년부터 2009년까지 ESC/Java2 개발은 2009년 코펜하겐의 IT대학으로, 2012년에는 덴마크 공과대학으로 이전한 University College Dublin의 KindSoftware Research Group에 의해 관리되었다.세월이 흐르면서 ESC/Java2는 다중 정리 프로버로 추론하는 능력, Eclipse와의 통합 등 많은 새로운 특징을 얻었다.
자바 1.8에서는 ESC/Java2의 후속 제품인 OpenJML을 이용할 수 있다.[2]출처는 https://github.com/OpenJML에서 확인할 수 있다.
참고 항목
참조
- ^ Flanagan, C.; Leino, K.R.M.; Lillibridge, M.; Nelson, G.; Saxe, J. B.; Stata, R. (2002). Extended static checking for Java. Proceedings of the Conference on Programming Language Design and Implementation. pp. 234–245. doi:10.1145/512529.512558. ISBN 1-58113-463-0.
- ^ "OpenJML download site on sourceforge".
- ^ "Java Modeling Language (JML) / Code / [r9606] /OpenJML/Trunk/OpenJML".
- 메모들
- Flanagan, C.; Kiniry, K. R. M. (2001). Houdini, an Annotation Assistant for ESC/Java. FME 2001: Formal Methods for Increasing Software Productivity. pp. 500–517. doi:10.1007/3-540-45251-6_29. ISBN 3-540-41791-5.
- Cataño, N.; Huisman, M. (2002). Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java. FME 2002:Formal Methods—Getting IT Right. pp. 272–289. doi:10.1007/3-540-45614-7_16. ISBN 3-540-43928-5.
- Cok, D. R.; Kiniry, J. R. (2005). ESC/Java2: uniting ESC/Java and JML. Proceedings of the 2004 international conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. pp. 108–128. doi:10.1007/978-3-540-30569-9_6. ISBN 3-540-24287-2.
- Chalin, P.; Kiniry, J. R.; Leavens, G. T.; Poll, E. (2006). Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. Formal Methods for Components and Objects. pp. 342–363. doi:10.1007/3-540-45614-7_16. ISBN 3-540-36749-7.
- Cok, D. R. (2006). Specifying java iterators with JML and Esc/Java2. Proceedings of the 2006 conference on Specification and verification of component-based systems. pp. 71–74. doi:10.1145/1181195.1181210. ISBN 1-59593-586-X.
- Chalin, P. (2006). Early detection of JML specification errors using ESC/Java2. Proceedings of the 2006 conference on Specification and verification of component-based systems. pp. 25–32. doi:10.1145/1181195.1181201. ISBN 1-59593-586-X.
- Ishikawa, H. (2009). An Approach for Refactoring using ESC/Java2: A Simple Case Study. Proceedings of the 2009 conference on New Trends in Software Methodologies, Tools and Techniques. pp. 61–72. ISBN 978-1-60750-049-0.
- Poll, E. (2009). Teaching Program Specification and Verification Using JML and ESC/Java2 (PDF). Proceedings of the 2nd International Conference on Teaching Formal Methods. pp. 92–104. doi:10.1007/978-3-642-04912-5_7. ISBN 978-3-642-04911-8.
- James, P. R.; Chalin, P. (2009). ESC4: a modern caching ESC for Java. Proceedings of the 8th international workshop on Specification and verification of component-based systems. pp. 19–26. doi:10.1145/1596486.1596491. ISBN 978-1-60558-680-9.
외부 링크
- Java Programming Toolkit 소스 릴리즈
- 웨이백 머신에서 Java에 대한 확장 정적 검사(2005년 12월 8일 보관)
- 킨드소프트웨어의 ESC/Java2
- SRC-RR-159 확장 정적 점검 - David L.데틀프스, K. 러스탄 M.레이노, 그렉 넬슨, 제임스 B색스
- Wayback Machine의 확장 정적 점검 모듈라-3(2001년 2월 28일 보관)
- 확장된 정적 체크 컴퓨터 과학 및 엔지니어링 콜로키아.워싱턴 대학교.1999.
