Alloy 시작

Alloy란
Alloy는 "소프트웨어 모델링에 사용되는 개방된 소스 언어와 분석기"이며 "안전의 빈틈을 발견하는 것부터 전화 교환 네트워크까지 광범위하게 응용된다"고 말했다.
Alloy is an open source language and analyzer for software modeling. It has been used in a wide range of applications, from finding holes in security mechanisms to designing telephone switching networks. - Alloy - Website
Alloy는 어떤 구속을 가정하는 대신 표현력과 자동 검증 능력을 겸비한'경량 형식 방법'의 일종이다.
일반적으로 형식 기법으로서의 언어의 표현력과 자동 검증 능력은 균형적인 관계이다.한 마디로 하면 편리한 문법을 준비한 언어일수록 복잡할수록 자동 검증의 계산 비용이 커진다(이런 것 같다)
Alloy가 가정하는 "어떤 구속"을 소범위 가정이라고 합니다.
소범위 가설은'대부분의 실수에 작은 반례가 있다'는 것을 가리킨다.한 마디로 하면 동치분할·경계치 분석적인 생각으로'대략 0 또는null을 포함하는 동치류 오류죠?'이런 말투.감각적으로 자유롭게 지배할 수 있다.
이 소범위 가설을 가정하고 적당한 소범위를 설정하여 반례가 있는지 없는지를 검증하는 것이지 모델에 대해 전면적인 검증을 하는 것이 아니다.
'적당한 작은 범위', 예를 들어 '모든 배열의length가 0, 1, 2에 오류가 있는지 검색하기'.length가 임의의 값일 때 구린내 나는 벌레를 검색하는 것은 매우 어려우며, 0, 1, 2라면 쉽게 계산할 수 있다.
또한 Alloy의 개발 환경은 특히 Alloy Analyzer라고 합니다.
환경 구조
웹 페이지 정보에서 실행 파일을 다운로드합니다.Windows 및 Linux의 경우 alloy.4.2.OS X의 경우 jar을 alloy4로 설정합니다.2. dmg 를 선택합니다.(또한, 현재(2017/4/30) 다운로드 가능한 최신 버전은 4.2%)

alloy4.2.jar Alloy 4.2 (platform independent). Requires Java 6.

alloy4.2.dmg Alloy 4.2 (for OS X). Requires Java 6.

다운로드한 파일을 디렉토리에 저장하면 설치가 완료됩니다.
Hello World!
Alloy 시작
다운로드한 alloy4.2. jar을 두 번 클릭하면 Alloy가 시작됩니다.자바와 확장자jar 사이의 관계를 설정하지 않으면 명령 알림 (또는 셸) 입력 java -jar alloy4.2.jar 을 통해 시작할 수 있습니다.

파일 만들기
Alloy 편집기에서 다음 코드를 설명합니다.
이번 예는'한 모니터에 표시된 것은 단지 하나의 컨트롤러에 있는'Hello World'일 뿐이다."입니다.
또 알로이의 문법은 EBNF 형태로 정의돼 웹 페이지 정보에서 열람할 수 있다.

/**
 * 
 * Hello World のモジュール
 * 
 */
module sample/HelloWorld

//=====================================================
//
// シグニチャ
//
//=====================================================

/** ディスプレイ */
one sig Display {
    console : one Console
}
one sig Console {
    message : some Message
}

/** メッセージ */
abstract sig Message {}

/** Hello World */
sig HelloWorld extends Message {}

//=====================================================
//
// 事実
//
//=====================================================

/** 全てのメッセージはコンソールに表示される */
fact {
    all m : Message | m in Console.message
}

//=====================================================
//
// 実行
//
//=====================================================
pred show{}
run show

모듈 선언

첫 줄의 module sample/HelloWorld는 모듈의 성명이다.모듈은 Alloy를 구성하는 최대 단위이며 여러 모듈을 연결하여 모델을 구성합니다.

이 예에서 sample는 자바로 포장명이고, HelloWorld는 자바로 분류명에 해당한다.

참고 사항

의견을 Java와 동일하게 씁니다.

서명

서명은 Java에서 클래스에 해당하는 개념이다.

그러나 Alloy에서는 한 모듈에 여러 서명을 포함합니다.

서명 성명은 간단하게 <sigQual> sig <name> {<decl>}로 묘사되었다.

<sigQual>는 서명의 수량과 방문을 나타내는 수식자입니다.

one는 한 개의 서명(즉 자바로 말하자면 단식)을 나타내는 수식부호이고, abstract는 실체가 없는 추상적인 서명을 나타내는 수식부호이다.

<name>는 서명한 이름을 가리킨다.<decl>는 서명의 정의로 자바로 구성원 변수를 정의합니다.

한 서명Display만 한 서명Console으로 정의됩니다.즉, 하나의 모니터에 하나의 콘솔만 표시되는 상태를 모델링합니다.

한 개Console의 서명만 0 개 또는 여러 개Message의 서명으로 정의된다.즉, 하나의 콘솔에 하나 이상의 메시지가 표시되는 상태를 모델링합니다.

Message 서명은 추상적인 서명이다.각종 소식을 추상화하는 추상적인 서명이다.

HelloWorld 서명은 상속Message 서명extends의 구체적인 서명이다.즉, 콘솔에 표시된 Hello World!에 대한 모델링 서명입니다.

사실

사실은 서명이 만족해야 할 조건을 열거했다.

"모든 메시지가 콘솔에 표시됩니다"는 사실은 모든 메시지all m : Message가 콘솔에 포함되어야 함을 나타냅니다in.

실행

는 실행 함수m in Console.message를 정의하고 실행pred show{}을 통해 모델을 검증한다.

실행
모형 표시run show 아이콘을 클릭하여 모형을 표시합니다.메타 모델은 Alloy 모델의 정적 구조를 나타내는 클래스입니다.서명의 포함 관계와 계승 관계를 나타낸다.

메타모델을 통해 모니터, 콘솔, 메시지 및 Show 서명의 포함 관계와 계승 관계를 확인합니다.
실행 결과 표시Hello World! 아이콘을 클릭하여 검증합니다.검증 결과는 Alloy에 정의된 모델의 인스턴스를 충족하는 것으로 표시됩니다.
이번 예에서는 Hello World 1개와 디스플레이 2개만 표시되는 경우를 출력했다.콘솔에 모델에 표시되는 Hello World의 수를 정의하지 않았기 때문입니다.
모니터 하나에 콘솔 하나에 Hello World 하나만 표시되면

모니터 하나에 Hello World 2개

이렇게 하면 Alloy는 검증 방법을 특별히 지정하지 않아도 오류가 발생하기 쉬운 경계 조건이나 같은 값 범주를 우선적으로 검증하고 표시합니다.
링크

다니엘 잭슨(저), 중도진(역), 이마이 겐남(역), 사카이 마사유(역), 히로시마 유개(역), 히로시마 신프(역), 추상적인 소프트웨어 디자인-올로이로 시작하는 형식 기법-옴사, 2011

Alloy - Website

alloy-4-eclipse