자바 모델링 언어

자바 모델링 언어(JML)는 계약 패러다임에 의한 설계를 따르는 호아레식 프리·포스 조건 및 불변제를 사용하는 자바 프로그램의 사양 언어다.사양은 소스 파일에 대한 Java 주석 설명으로 작성되며, 따라서 모든 Java 컴파일러로 컴파일할 수 있다.

런타임 어설션 체커 및 확장 정적 체커(ESC/Java)와 같은 다양한 검증 도구가 개발을 돕는다.

개요

JML은 Java 모듈의 행동 인터페이스 사양 언어다.JML은 Java 모듈의 행동을 공식적으로 기술하기 위한 의미론을 제공하며, 모듈 설계자의 의도와 관련된 모호성을 방지한다.JML은 에펠, 라치, 정제 미적분학으로부터 아이디어를 이어받는데, 어떤 자바 프로그래머도 여전히 접근할 수 있는 동시에 엄격한 공식 의미론을 제공한다는 목표를 가지고 있다.JML의 행동 규격을 활용하는 다양한 도구들이 있다.사양은 자바 프로그램 파일에 주석을 달거나 별도의 사양 파일에 저장할 수 있기 때문에 JML 사양의 자바 모듈은 어떤 자바 컴파일러로도 변경 없이 컴파일할 수 있다.

구문

JML 사양은 주석에 주석 형태로 자바 코드에 추가된다.자바 주석은 @ 기호로 시작할 때 JML 주석으로 해석된다.즉, 양식의 코멘트

//@ <JML 사양>

또는

/*@ <JML 사양> @*/

기본 JML 구문은 다음과 같은 키워드를 제공한다.

requires

다음과 같은 방법에 대한 전제조건을 규정한다.

ensures

다음 방법에 대한 사후 조건을 정의한다.

signals

다음 방법으로 지정된 예외를 발생시키는 경우에 대한 사후 조건을 정의하십시오.

signals_only

주어진 전제조건이 유지될 때 어떤 예외를 제기할 수 있는지 규정한다.

assignable

다음 방법으로 할당할 수 있는 필드를 정의하십시오.

pure

메서드를 부작용 없음(예:assignable \nothing예외를 둘 수도 있다.더욱이 순수한 방법은 항상 정상적으로 종료하거나 예외를 두어야 한다.

invariant

클래스의 불변 속성을 규정한다.

loop_invariant

루프에 대해 루프를 불변으로 정의한다.

also

명세 사례를 결합하고, 어떤 방법이 그 슈퍼타입으로부터 명세를 계승하고 있다고 선언할 수도 있다.

assert

JML 어설션을 정의하십시오.

spec_public

규격 목적을 위해 보호 변수 또는 비공개 변수를 공개로 선언한다.

기본 JML은 또한 다음과 같은 식을 제공한다.

\result

다음 메서드의 반환 값에 대한 식별자.

\old(<expression>)

값을 나타내는 한정자<expression>어떤 방법에 착수할 때

(\forall <decl>; <range-exp>; <body-exp>)

범용 계량기.

(\exists <decl>; <range-exp>; <body-exp>)

실존적 계량기.

a ==> b

a함축적으로 말하다b

a <== b

a은연중에 있다b

a <==> b

a만약의 경우에 한해서만b

논리적 및 또는 그렇지 않은 표준 Java 구문뿐만 아니라JML 주석은 또한 주석을 달 수 있는 방법의 범위 내에 있고 적절한 가시성을 가진 Java 객체, 객체 방법 및 연산자에 대한 액세스 권한을 가지고 있다.이것들은 클래스, 필드 및 방법의 속성에 대한 공식적인 사양을 제공하기 위해 결합된다.예를 들어, 주석을 단 간단한 은행 클래스의 예는 다음과 같이 보일 수 있다.

공중의 계급 BankingExample {       공중의 정태의 최종의 인트로 맥스_밸런스 = 1000;      사유의 /*@spec_public@*/ 인트로 균형을 잡다;     사유의 /*@spec_public@*/ 부울 잠금 해제됨 = 거짓의;        //@ 공공 불변균형 >= 0 &&balance <= MAX_BANCE;       //@ 할당 가능한 균형;     //@잔액 == 0;     공중의 BankingExample()     {         이.균형을 잡다 = 0;     }       //@는 0 < 금액 &&& 금액 + 잔액 < MAX_BANCE;     //@ 할당 가능한 균형;     //@잔액 == \old(균형) + 금액 보장;     공중의 공허하게 하다 대변을 보다(최종의 인트로 분량)     {         이.균형을 잡다 += 분량;     }       //@는 0 < 금액 &&& 금액 <= 잔액;     //@ 할당 가능한 균형;     //@ 잔액 == \old(균형) - 양 보장;     공중의 공허하게 하다 차변(최종의 인트로 분량)     {         이.균형을 잡다 -= 분량;     }       //@ isLocked == true;     공중의 공허하게 하다 lockAccount()     {         이.잠금 해제됨 = 진실의;     }       //@ 필요 !is잠금;     //@가 \cHB == 균형을 보장;     //@도     //@ isLocked 필요;     //@ signals_Only BankingException;     공중의 /*@ 순수 @*/ 인트로 게트밸런스() 던지다 뱅킹익스셉션     {         만일 (!이.잠금 해제됨)         {                 돌아오다 이.균형을 잡다;         }         다른         {                 던지다 새로운 뱅킹익스셉션();         }     } } 

JML 구문에 대한 전체 설명서는 JML 참조 매뉴얼에서 확인할 수 있다.

툴 지원

다양한 도구가 JML 주석을 기반으로 한 기능을 제공한다.아이오와 주 JML 도구는 어설션 체크 컴파일러를 제공한다. jmlcJML 주석을 문서 생성기인 런타임 주장으로 변환한다.jmldocJML 주석 및 장치 테스트 생성기의 추가 정보와 함께 Javadoc 문서를 생성함jmlunitJML 주석으로부터 JUnit 테스트 코드를 생성한다.

독립된 그룹들은 JML 주석을 사용하는 도구를 연구하고 있다.여기에는 다음이 포함된다.

• 다른 방법보다 더 엄격한 정적 검사를 수행하기 위해 JML 주석을 사용하는 확장 정적 검사기 ESC/Java2 [1].
• 오픈JML은 스스로를 ESC/Java2의 후계자로 선언한다.
• 다이콘, 동적 불변 발전기.
• JML의 구문 강조표시를 지원하는 오픈소스 정리 프로베이어와 Eclipse 플러그인(JML Editing)을 제공하는 KeY.
• Krakatoa는 Why 검증 플랫폼에 기반하고 Coq 증명 도우미를 사용하는 정적 검증 툴이다.
• JML 구문 및 JML 주석을 사용하는 다양한 도구와의 인터페이스를 지원하는 Eclipse 통합 개발 환경의 플러그인 JML클립스.
• 시름/키아산, JML을 계약 언어로 지원하는 상징적인 실행 기반 정적 분석기.
• JML에 주석을 단 Java 파일에서 JUnit 테스트를 실행하기 위한 파일을 생성하는 도구인 JMLUnit.
• TACO는 Java 프로그램의 Java Modeling Language 사양과 정적으로 Java 프로그램의 준수를 검사하는 오픈 소스 프로그램 분석 툴이다.
• VerCors 검증기

참조

• 개리 티 레븐스와 천윤식.JML과의 계약에 의한 설계; 초안 자습서.
• 게리 T. 레븐스, 앨버트 L. 베이커, 클라이드 루비.JML: 상세설계를 위한 표기법; Haim Kilov, Bernhard Rumpe 및 Ian Simmonds(편집자), Business and Systems의 행동규격, Kluwer, 1999, 12장 175-188.
• 게리 티 레븐스, 에릭 폴, 커티스 클리프턴, 윤식천, 클라이드 루비, 데이비드 콕, 피터 뮐러, 조셉 키니리, 패트리스 샬린, 다니엘 M. 짐머만.JML 참조 설명서(Draft), 2009년 9월.HTML
• 마리크 후이스만, 볼프강 아렌트, 다니엘 브런스, 마틴 헨첼.JML로 정식 사양 2014. 다운로드(CC-BY-NC-ND)

외부 링크

• JML 웹사이트