합금(사양 언어)

Alloy (specification language)

컴퓨터 과학 및 소프트웨어 공학에서 알로이(Alloy)는 소프트웨어 시스템의 복잡한 구조적 제약 및 동작을 표현하기 위한 선언적 사양 언어입니다.합금은 1차 [1]논리에 기초한 간단한 구조 모델링 도구를 제공합니다.합금은 마이크로 모델 생성을 목표로 하며, 마이크로 모델은 자동으로 정확성을 확인할 수 있습니다.합금 사양은 합금 분석기를 사용하여 확인할 수 있습니다.

합금은 자동 분석을 염두에 두고 설계되었지만 무한 모델을 정의할 수 있다는 점에서 모델 확인을 위해 설계된 많은 사양 언어와 다릅니다.합금 분석기는 무한대 모델에서도 유한 스코프 검사를 수행하도록 설계되었습니다.

알로이 언어와 분석기는 미국 매사추세츠 공과대학의 다니엘 잭슨이 이끄는 팀에 의해 개발되었습니다.

역사와 영향

알로이 언어의 첫 번째 버전은 1997년에 등장했다.그것은 다소 제한된 객체 모델링 언어였다."양자 추가, 상위 특성 관계, 다형성, 서브타이핑 및 시그니처"[2] 언어의 후속 반복.

언어의 수학적 기초는 Z 표기법의 영향을 많이 받았고, 알로이 구문은 객체 제약 언어와 같은 언어에서 기인한다.

합금 분석기

합금 분석기

합금 분석기는 소위 "경량 공식 방법"을 지원하기 위해 특별히 개발되었습니다.이와 같이 알로이(Alloy)와 유사한 사양 언어에 일반적으로 사용되는 인터랙티브 정리 증명 기법과 대조적으로 완전 자동 분석을 제공하기 위한 것입니다.Analyzer의 개발은 원래 모델 체커가 제공하는 자동 분석에서 영감을 받았습니다.그러나 모델 체크는 일반적으로 알로이에서 개발된 모델에는 적합하지 않으며, 결과적으로 분석기의 핵심이 부울 SAT [1]솔버 위에 구축된 모델 파인더로 구현되었습니다.

버전 3.0을 통해 알로이 분석기는 기성 SAT 솔버를 기반으로 하는 일체형 SAT 기반 모델 파인더를 통합했습니다.그러나 4.0 버전부터는 분석기가 프런트 엔드 역할을 하는 Kodkod 모델 파인더를 사용합니다.두 모델 파인더는 기본적으로 관계형 논리로 표현된 모델을 대응하는 부울 논리식으로 변환한 다음 부울 공식에서 기성 SAT 솔버를 호출합니다.해결사가 해결책을 찾으면 결과는 관계 논리 모델에서 변수에 [3]대응하는 상수의 결합으로 다시 변환됩니다.

모델 검색 문제를 확실하게 해결하기 위해 합금 분석기는 사용자 정의 유한 개수의 개체로 구성된 제한된 범위에 대해 모델 검색을 수행합니다.이는 분석기가 생성하는 결과의 일반성을 제한하는 효과가 있습니다.그러나 합금 분석기 설계자들은 일부 소규모 [4]범위 내에서 모든 테스트 입력을 테스트함으로써 많은 수의 버그를 발견할 수 있다는 소범위 가설에 호소하여 제한된 범위 내에서 작업하기로 결정한 것을 정당화합니다.

모델 구조

합금 모델은 본질적으로 관계형이며 다음과 같은 여러 가지 다른 [1]문장으로 구성됩니다.

  • 시그니처는 새로운 세트를 생성하여 모델의 어휘를 정의합니다.
sig Object{}시그니처 오브젝트를 정의합니다.
sig List{ head : lone Node }는 노드 및 다중성 론 유형의 필드 헤드를 포함하는 시그니처 목록을 정의합니다.이것에 의해, 리스트와 노드간의 관계가 확립되어 모든 리스트가 1개 이상의 헤드노드와 관련지을 수 없게 됩니다.
  • 사실은 항상 유지된다고 가정되는 제약 조건이다.
  • 술어는 매개 변수화된 제약 조건이며 연산을 나타내는 데 사용할 수 있습니다.
  • 함수는 결과를 반환하는 식입니다.
  • 주장은 모형에 대한 가정입니다.

합금은 선언적 언어이기 때문에 모형의 의미는 문장의 순서에 영향을 받지 않습니다.

레퍼런스

  1. ^ a b c Jackson, Daniel (2006). Software Abstractions: Logic, Language, and Analysis. MIT Press. ISBN 978-0-262-10114-1.
  2. ^ "Alloy FAQ". Archived from the original on 7 June 2007. Retrieved 7 March 2013.
  3. ^ Torlak, E.; Dennis, G. (April 2008). "Kodkod for Alloy Users" (PDF). First ACM Alloy Workshop. Portland, Oregon. Archived from the original (PDF) on 22 June 2010. Retrieved 19 April 2009.
  4. ^ Andoni, Alexandr; Daniliuc, Dumitru; Khurshid, Sarfraz; Marinov, Darko (2002). "Evaluating the small scope hypothesis". CiteSeerX 10.1.1.8.7702. {{cite journal}}:Cite 저널 요구 사항 journal=(도움말)

외부 링크