비엔나 개발 방법

VDM(Vienna Development Method, VDM)은 컴퓨터 기반 시스템 개발을 위해 가장 오래 확립된 공식 방법 중 하나이다.1970년대 IBM Laboratory Vienna에서^[1] 수행된 작업에서 시작되어, 공식 사양 언어인 VDM 사양 언어(VDM-SL)에 기초한 기술과 도구 그룹을 포함하도록 성장했다.확장된 형태인 VDM++^[2]를 가지고 있어 객체 지향 및 동시 시스템 모델링을 지원한다.VDM 지원에는 모델의 테스트 및 특성 입증 지원, 검증된 VDM 모델에서 프로그램 코드 생성 등 모델 분석을 위한 상업적 및 학술적 도구가 포함된다.VDM과 그 도구의 산업적 사용의 역사가 있고 형식주의에서 연구 기구가 증가함에 따라 중요한 시스템, 컴파일러, 동시 시스템 및 컴퓨터 과학의 논리 공학에 현저한 기여를 하게 되었다.

철학

컴퓨터 시스템은 프로그래밍 언어를 사용하여 달성할 수 있는 것보다 더 높은 수준의 추상화 수준에서 VDM-SL에서 모델링될 수 있으며, 시스템 개발의 초기 단계에서 결함을 포함한 주요 기능의 설계 분석 및 식별이 가능하다.검증된 모델은 미세화 과정을 통해 세부적인 시스템 설계로 탈바꿈할 수 있다.언어는 형식적인 의미론을 가지고 있어 높은 수준의 보증으로 모델의 특성을 증명할 수 있다.또한 실행 가능한 서브셋을 가지고 있어, 시험으로 모델을 분석할 수 있고 그래픽 사용자 인터페이스를 통해 실행할 수 있어, 모델 언어 자체에 반드시 익숙하지 않은 전문가에 의해 모델을 평가할 수 있다.

역사

VDM-SL의 기원은 VDL(Vienna Definition Language, VDL)이라고 불리는 빈의 IBM 연구소에 있다.^[3]VDL은 기본적으로 VDM - Meta-IV와 대조적으로 작동 의미론 설명을 제공하는 데 사용되었으며, 이는 변위 의미론을 제공하였다^[4].

1972년 말 비엔나 집단은 다시 언어의 정의로부터 체계적으로 컴파일러를 개발하는 문제에 관심을 돌렸다.채택된 전체 접근 방식은 "비엔나 개발 방법"이라고 불렸다.실제로 채택된 메타 언어("Meta-IV")는 BEKICH 74에서 PL/1의 주요 부분(ECMA 74 - 흥미롭게도 "추상 해석기로 작성된 공식 표준 문서")을 정의하는 데 사용된다. »^[5]

Meta-IV와 Schorre의 Meta-II 언어 또는 그 후속 Tree Meta 사이에는 아무런 연관성이 없다; 이것들은 공식적인 문제 설명에 적합하기 보다는 컴파일러-컴파일러 시스템이었다.^[6]

그래서 Meta-IV는 PL/I 프로그래밍 언어의 주요 부분을 정의하는데 사용되었다.Meta-IV와 VDM-SL을 사용하여 소급하거나 부분적으로 기술된 다른 프로그래밍 언어로는 BASIC 프로그래밍 언어, FORTRAN, APL 프로그래밍 언어, ALGOL 60, Ada 프로그래밍 언어 및 Pascal 프로그래밍 언어가 있다.Meta-IV는 일반적으로 덴마크, 영어, 아일랜드 학교라고 묘사되는 여러 변종들로 진화했다.

언어 정의 및 컴파일러 설계와 특별히 관련이 없는 VDM의 측면에 대한 Cliff Jones의 연구에서 도출된 "English School"이다(Jones 1980, 1990).다양한 기본 유형 집합에서 생성된 데이터 유형의 사용을 통해 지속적인^[7] 상태 모델링을 강조한다.기능성은 일반적으로 상태에 부작용이 있을 수 있고 대부분 전제조건과 사후 조건을 사용하여 암묵적으로 지정되는 운영을 통해 설명된다."Danish School"(Bjørner et al. 1982년)은 명시적 운영 규격을 더 많이 사용한 건설적 접근방식을 강조하는 경향이 있다.덴마크 학교에서 일하면서 유럽 최초로 검증된 에이다 컴파일러로 이어졌다.

이 언어에 대한 ISO 표준은 1996년에 발표되었다(ISO, 1996).

VDM 기능

VDM-SL 및 VDM++ 구문 및 의미론은 VDMTools 언어 설명서와 사용 가능한 텍스트에 자세히 설명되어 있다.ISO 표준은 언어의 의미론에 대한 공식적인 정의를 포함하고 있다.이 글의 나머지 부분에서는 ISO 정의 교환(ASCII) 구문이 사용된다.일부 텍스트는 보다 간결한 수학적 구문을 선호한다.

VDM-SL 모델은 데이터에 대해 수행되는 기능 측면에서 주어진 시스템 설명이다.그것은 일련의 데이터 유형과 기능에 대한 정의 또는 그것들에 대해 수행된 운영으로 구성된다.

기본 유형: 숫자, 문자, 토큰 및 견적 유형

VDM-SL은 다음과 같은 기본 형식 모델링 번호와 문자를 포함한다.

기본 유형

bool	부울 데이터 유형	거짓의
nat	자연수 (0 포함)	0, 1, 2, 3, 4, 5 ...
nat1	자연수 (0 제외)	1, 2, 3, 4, 5, ...
int	정수	..., −3, −2, −1, 0, 1, 2, 3, ...
rat	합리적인 수.	a/b, 여기서 a와 b가 정수인 경우 b는 0이 아니다.
real	실수	...
char	성격.	A, B, C, ...
token	무구조 토큰	...
<A>	값을 포함하는 인용문형<A>	...

데이터 유형은 모델링된 시스템의 주요 데이터를 나타내기 위해 정의된다.각 유형 정의는 새로운 유형 이름을 도입하고 기본 유형 또는 이미 도입된 유형 측면에서 표현을 한다.예를 들어 로그인 관리 시스템에 대한 사용자 식별자를 모델링하는 형식은 다음과 같이 정의될 수 있다.

유형 UserId = nat

데이터 유형에 속하는 값을 조작하기 위해, 연산자를 그 값에 정의한다.따라서 평등과 불평등과 같은 부울 연산자와 마찬가지로 자연수 덧셈, 뺄셈 등이 제공된다.언어는 최대 또는 최소의 표현 가능한 숫자 또는 실제 숫자에 대한 정밀도를 정하지 않는다.이러한 제약조건은 데이터 유형 불변제를 통해 각 모델에서 요구되는 경우 정의된다. 즉, 부울 식은 정의된 유형의 모든 요소에서 존중되어야 하는 조건을 나타낸다.예를 들어 사용자 식별자가 9999 이하여야 한다는 요구사항은 다음과 같이 표현된다(여기서).<=자연수에서 "보다 작거나 같은" 부울 연산자:

UserId = nat inv uid == uid <= 99999

불변성은 임의로 복잡한 논리 표현식이 될 수 있고, 정의된 유형의 멤버십은 불변성을 만족하는 값에만 한정되기 때문에 VDM-SL의 형식 정확성은 모든 상황에서 자동으로 해독될 수 있는 것은 아니다.

다른 기본 유형에는 문자 문자를 포함한다.어떤 경우에, 형식의 표현은 모델의 목적과 관련이 없고 복잡성을 가중시킬 뿐이다.이 경우 형식의 구성원은 무구조 토큰으로 나타낼 수 있다.토큰 유형의 값은 평등에 대해서만 비교할 수 있으며, 다른 운영자는 이에 대해 정의되지 않는다.특정 명명된 값이 필요한 경우 이를 인용 유형으로 도입한다.각 인용문 유형은 그 유형 자체와 동일한 이름의 하나의 명명된 값으로 구성된다.따옴표 유형(따옴표 리터럴로 알려져 있음)의 값은 동등성만을 위해 비교할 수 있다.

예를 들어, 교통 신호 제어기를 모델링할 때, 교통 신호의 색상을 인용 유형으로 나타내는 값을 정의하는 것이 편리할 수 있다.

<빨간색>, <암버>, <깜짝암버>, <녹색>.

유형 생성자: 조합, 제품 및 복합 유형

기본형만으로는 한계가 있다.보다 구조화된 새 데이터 유형은 유형 생성자를 사용하여 구축된다.

기본 유형 생성자

T1 T2 ... Tn	유형 조합T1,...,Tn
T1*T2*...*Tn	데카르트 유형의 제품T1,...,Tn
T :: f1:T1 ... fn:Tn	합성(기록) 유형

가장 기본적인 유형 생성자는 미리 정의된 두 유형의 결합을 형성한다.유형(A B)A 유형의 모든 요소 및 모든 유형 포함B. 교통신호제어기 예에서 교통신호의 색상을 모델링하는 형식은 다음과 같이 정의될 수 있다.

시그널컬러 = <빨간색> <황색> <깜짝깜짝 빛나는 앰버> <녹색>

VDM-SL에 열거된 형식은 위에서 제시한 바와 같이 견적 유형에 대한 조합으로 정의된다.

데카르트 제품 유형은 VDM-SL에도 정의될 수 있다.유형(A1*…*An)모든 값의 튜플로 구성된 유형이며, 그 중 첫 번째 요소는 유형이다.A1그리고 두 번째는 유형에서 두 번째 유형A2등등.복합 또는 레코드 유형은 필드 레이블이 있는 데카르트 제품이다.유형

T :: f1:A1 f2:A2 … fn:An

필드가 라벨로 표시된 데카르트 제품f1,…,fn. 타입의 요소T그 구성 요소로부터 건설업자에 의해 구성될 수 있다.mk_T. 반대로, 유형 요소가 주어짐T필드 이름을 사용하여 명명된 구성요소를 선택할 수 있다.예를 들어 유형

날짜 : 일 ::nat1개월:nat1년:nat inv mk_Date(d,m,y) ==d <=31 및 m<=12

간단한 날짜 유형을 모델링하십시오.값mk_Date(1,4,2001)2001년 4월 1일에 해당한다.날짜 지정d, 표현d.month월을 나타내는 자연수다.월별 일수 및 윤년 제한은 원하는 경우 불변제(invariant)에 통합될 수 있다.다음 항목을 결합하십시오.

mk_Date(1,4,2001).월 = 4

컬렉션

수집 유형 모델 그룹 값.집합은 값 사이의 중복을 억제하는 유한 비순서 집합이다.시퀀스는 중복이 발생할 수 있는 유한 순서 집합(목록)이며, 매핑은 두 값 집합 사이의 유한 대응 관계를 나타낸다.

놓다

Set type 생성자(서면됨set of T어디에T사전 정의된 형식) 형식에서 추출된 모든 유한한 값 집합으로 구성된 형식T. 예를 들어 유형 정의

UGrup = UserId 집합

활자를 규정하다.UGroup의 모든 유한한 집합으로 구성되어 있다.UserId가치다양한 운영자들이 그들의 결합, 교차점, 적절하고 엄격하지 않은 부분집합 관계 등을 결정하기 위한 세트에서 정의된다.

집합의 주 연산자(s, s1, s2는 집합)

{a, b, c}	열거형 설정: 요소 집합a,b그리고c
{x x:T & P(x)}	이해력 설정: 의 집합x활자로T그런P(x)
{i, ..., j}	범위의 정수 집합i로j
e in set s	e집합의 요소s
e not in set s	e집합의 요소가 아님s
s1 union s2	집합 조합s1그리고s2
s1 inter s2	집합 교차점s1그리고s2
s1 \ s2	세트 차이 설정s1그리고s2
dunion s	집합 집합 집합의 분산 결합s
s1 psubset s2	s1은 의 (property) 부분 집합이다.s2
s1 subset s2	s1은 의 (subset) 부분 집합이다.s2
card s	세트의 카디널리티s

시퀀스

유한 시퀀스 유형 생성자(서면)seq of T어디에T사전 정의된 유형) 형식에서 추출된 모든 유한한 값 리스트로 구성된 형식 구성T. 예를 들어 유형 정의

문자열 = 문자 집합

유형 정의String모든 유한한 문자로 구성되어 있다.접속 구성, 요소 선택 및 부속서 등을 위한 시퀀스에 대해 다양한 연산자를 정의한다.이들 사업자 중 상당수는 특정 용도에 대해 정의되지 않았다는 점에서 부분적이다.예를 들어, 세 개의 요소만 포함하는 시퀀스의 다섯 번째 요소를 선택하는 것은 정의되지 않는다.

순서에 따른 항목의 순서와 반복이 중요하기 때문에[a, b]와 같지 않다[b, a]그리고[a]와 같지 않다[a, a].

시퀀스에 대한 주 연산자(s, s1,s2는 시퀀스)

[a, b, c]	시퀀스 열거: 요소의 시퀀스a,b그리고c
[f(x) x:T & P(x)]	시퀀스 이해: 식 순서f(x)한 사람 한 사람당x타입의T그런P(x)쥔다 (x숫자 순서로 취한 값)
hd s	의 머리(첫 번째 요소)s
tl s	의 테일(헤드를 제거한 후 남은 시퀀스)s
len s	의 길이s
elems s	의 요소 집합s
s(i)	그ith 의 요소.s
inds s	순서에 대한 지수 집합s
s1^s2	염기서열 결합으로 형성된 염기서열s1그리고s2

지도

유한 매핑은 범위의 도메인 색인 요소와 도메인 및 범위 두 세트 사이의 대응이다.따라서 유한함수와 유사하다.VDM-SL의 매핑 유형 생성자(서면)map T1 to T2어디에T1그리고T2미리 정의된 유형)의 집합에서 모든 유한 매핑으로 구성된 유형 구성T1일련의 값들T2가치예를 들어 유형 정의

생일 = 날짜별 지도 문자열

유형 정의Birthdays문자열을 매핑할 대상Date. 다시, 연산자는 매핑에 대한 색인화, 매핑 병합, 하위 매핑 추출에 대한 덮어쓰기를 위한 매핑에 정의된다.

매핑의 주 연산자

{a -> r, b -> s}	매핑 열거:a에 매핑하다.r,b에 매핑하다.s
{x -> f(x) x:T & P(x)}	매핑 이해:x에 매핑하다.f(x)대체적으로x활자로T그런P(x)
dom m	의 도메인m
rng m	의 범위m
m(x)	m에 적용했다.x
m1 munion m2	매핑 연합m1그리고m2(m1,m2겹치는 부분이 일치해야 함)
m1 ++ m2	m1에 의해 덮어쓰다.m2

구조화

VDM-SL과 VDM++ 표기 사이의 주요 차이점은 구조를 처리하는 방식이다.VDM-SL에는 전통적인 모듈형 확장이 있는 반면, VDM+++는 클래스와 상속을 포함하는 전통적인 객체 지향 구조 메커니즘을 가지고 있다.

VDM-SL 구조화

VDM-SL에 대한 ISO 표준에는 서로 다른 구조 원리를 포함하는 유익한 부록이 있다.이들 모두는 모듈로 전통적인 정보 숨기기 원칙을 따르고 있으며, 다음과 같이 설명될 수 있다.

• 모듈 이름:각 모듈은 키워드를 사용하여 구문식으로 시작됨module그 다음에 모듈 이름이 나온다.모듈의 끝에서 키워드end모듈 이름 뒤에 다시 쓰여진다.
• 가져오는 중:다른 모듈에서 내보낸 정의를 가져올 수 있다.키워드로 시작하는 가져오기 섹션에서 이 작업을 수행하십시오.imports그리고 다른 모듈로부터 일련의 수입품들이 뒤따른다.이러한 각 모듈 가져오기는 키워드로 시작됨from모듈 이름 및 모듈 서명 뒤에 오십시오.모듈 서명은 단순히 키워드가 될 수 있다.all해당 모듈에서 내보낸 모든 정의 가져오기를 표시하거나, 또는 가져오기 서명의 시퀀스가 될 수 있다.가져오기 서명은 유형, 값, 기능 및 작업에 한정되며, 각각의 서명은 해당 키워드로 시작한다.또한 이러한 가져오기 서명은 액세스하고자 하는 구문을 명명한다.또한 선택적 형식 정보가 있을 수 있으며 마지막으로 가져올 때 각 구조물의 이름을 바꿀 수 있다.유형에는 키워드도 사용해야 한다.struct특정 유형의 내부 구조에 접근하려면
• 내보내기:다른 모듈에서 액세스하기를 원하는 모듈의 정의는 키워드를 사용하여 내보내진다.exports수출 모듈 서명이 뒤따른다.내보내기 모듈 서명은 단순히 키워드로 구성될 수 있다.all또는 수출 서명의 순서로서.이러한 수출 서명은 유형, 값, 기능 및 운영에 한정되며 각각 해당 키워드로 시작한다.내부 구조를 내보내려는 경우 키워드를 입력하십시오.struct반드시 사용되어야 한다.
• 이국적인 기능:이전 버전의 VDM-SL 도구에서는 매개 변수화된 모듈과 그러한 모듈의 인스턴스화에 대한 지원도 있었다.그러나 이러한 기능은 산업용 애플리케이션에서 거의 사용되지 않았고 이러한 기능에서 상당한 도구 문제가 발생했기 때문에 2000년경에 VDMTools에서 제외되었다.

VDM++의 구조화

VDM++ 구조는 클래스와 다중 상속을 사용하여 이루어진다.주요 개념은 다음과 같다.

• 클래스: 각 클래스는 키워드로 구문적으로 시작됨class그 뒤에 반의 이름이 붙었다.수업이 끝날 때 키워드는end그 다음에 또 그 반의 이름이 쓰여진다.
• 상속:클래스가 다른 클래스의 구성을 상속하는 경우 클래스 제목에 클래스 이름이 뒤에 있을 수 있음is subclass of그 다음에 쉼표로 구분된 슈퍼클래스 이름 목록이 나온다.
• 액세스 한정자:VDM++에 숨어 있는 정보는 액세스 한정자를 사용하는 대부분의 객체 지향 언어와 동일한 방식으로 이루어진다.VDM++ 정의는 기본적으로 비공개지만 모든 정의 앞에서 다음 액세스 한정자 키워드 중 하나를 사용할 수 있다.private,public그리고protected.

모델링 기능

기능 모델링

VDM-SL에서는 모델에 정의된 데이터 유형에 걸쳐 함수가 정의된다.추상화에 대한 지원은 함수가 어떻게 계산되어야 하는지를 말하지 않아도 함수가 계산해야 하는 결과를 특성화할 수 있어야 한다고 요구한다.이를 위한 주요 메커니즘은 결과를 계산하는 공식 대신에 포스트 조건이라고 불리는 입력과 결과 변수에 대한 논리 술어가 결과의 속성을 제공하는 암묵적 함수 정의다.예를 들어, 함수SQRT자연수의 제곱근을 계산하기 위해 다음과 같이 정의할 수 있다.

SQRT(x:nat)r:real post r*r = x

여기서 사후 조건은 결과를 계산하는 방법을 정의하지 않는다.r그러나 어떤 성질을 가지고 있다고 가정할 수 있는지 명시한다.이것은 유효한 제곱근을 반환하는 함수를 정의한다는 점에 유의하십시오. 양수 또는 음수근이어야 한다는 요구사항은 없다.예를 들어, 위의 규격은 4의 음의 루트를 반환했지만 다른 모든 유효한 입력의 양의 루트를 반환한 함수에 의해 충족될 것이다.VDM-SL의 기능은 위의 예시 규격을 만족하는 함수가 항상 동일한 입력에 대해 동일한 결과를 반환하도록 결정론적이어야 한다는 점에 유의하십시오.

사후 조건을 강화하여 보다 제약적인 기능 규격을 달성한다.예를 들어, 다음의 정의는 함수를 제약하여 양의 근을 반환한다.

SQRT(x:nat)r:real post r*r = x 및 r>=0

모든 기능 사양은 입력 변수에 대한 논리적 술어이며 기능이 실행될 때 충족된다고 가정되는 제약 조건을 설명하는 전제조건에 의해 제한될 수 있다.예를 들어, 양의 실수에서만 작동하는 제곱근 계산 함수는 다음과 같이 지정될 수 있다.

SQRTP(x:real)r:real pre x >=0 post r*r = x 및 r>=0

전제조건과 사후조건이 함께 기능 구현을 주장하는 어떤 프로그램이든 만족하는 계약을 맺는다.전제조건은 기능이 사후 조건을 만족하는 결과를 반환하도록 보장하는 가정을 기록한다.함수가 그 전제조건을 충족하지 않는 입력에 대해 호출되는 경우, 결과는 정의되지 않는다(사실, 종료는 보장되지도 않는다).

VDM-SL은 또한 기능 프로그래밍 언어의 방식으로 실행 가능한 기능의 정의를 지원한다.명시적 함수 정의에서 결과는 입력에 대한 표현에 의해 정의된다.예를 들어, 숫자 목록의 제곱 목록을 생성하는 함수는 다음과 같이 정의될 수 있다.

SqList: s = []이면 sqList ==의 nat -> seq가 다른 [(hd s)**2] ^SqList(tl s)

이 재귀적 정의는 입력과 결과의 유형을 제공하는 함수 서명과 함수 본체로 구성된다.동일한 함수의 암묵적 정의는 다음과 같은 형식을 취할 수 있다.

SqListImp(s:seq of nat)r:secq post len r = len s, set inds &r(i) = s(i)**2

명시적 정의는 단순한 의미에서 암묵적으로 지정된 함수의 구현이다.암묵적 명세에 관한 명시적 함수 정의의 정확성은 다음과 같이 정의될 수 있다.

암묵적 사양 지정:

f(p:T_p)r:T_r pre-f(p) post-f(p, r)

및 명시적 함수:

f:T_p -> T_r

iff: 규격에 부합한다고 말한다.

설정 T_p & pre-f(p) => f(p):T_r 및 post-f(p, f(p))

그래서 "f올바른 구현 여부"는 다음과 같이 해석되어야 한다.f규격에 부합한다."

국가 기반 모델링

VDM-SL에서 함수는 지속적 글로벌 변수의 상태를 변경하는 등의 부작용이 없다.이것은 많은 프로그래밍 언어에서 유용한 능력이기 때문에 유사한 개념이 존재한다. 기능 대신에 운영은 상태 변수(글로벌이라고도 함)를 변경하기 위해 사용된다.

예를 들어 단일 변수로 구성된 상태가 있는 경우someStateRegister : natVDM-SL에서 이를 다음과 같이 정의할 수 있다.

someStateRegister: nat end

VDM++에서 이는 대신 다음과 같이 정의된다.

인스턴스 변수 someStateRegister : nat

이 변수에 값을 로드하는 작업은 다음과 같이 지정될 수 있다.

LOAD(i:nat) ext wr someStateRegister:nat post someStateRegister = i

외부 절(Externals 절)ext)은 연산에 의해 접속할 수 있는 주의 부분을 지정한다.rd읽기 전용 액세스 표시 및wr읽기/쓰기 액세스 권한.

때로는 수정되기 전의 상태 값을 참조하는 것이 중요하다. 예를 들어 변수에 값을 추가하는 연산을 다음과 같이 지정할 수 있다.

ADD(i:nat) extraStateRegister: someStateRegister = someStateRegister~ + i

어디?~사후 조건의 상태 변수에 있는 기호는 작업을 실행하기 전의 상태 변수의 값을 나타낸다.

예

최대함수

이것은 암묵적 함수 정의의 예다.함수는 양의 정수 집합에서 가장 큰 원소를 반환한다.

max(s:s:set of nat)r:nat pre card s > 0 post r in s(set s), forall r(set s & r' <= r)

포스트 조건은 결과를 얻기 위한 알고리즘을 정의하기보다는 결과를 특징짓는다.세트가 비어 있을 때 어떤 함수도 세트 s에서 r을 반환할 수 없기 때문에 전제 조건이 필요하다.

자연수 곱하기

multp(i,j:nat)r:rnat 이전 true post r = i*j

증명 의무 적용forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))의 명백한 정의로multp:

multp(i,j) == i=0이면 0이고 짝수인 경우 2*multp(i/2,j) 다른 j+multp(i-1,j)

그러면 증명 의무는 다음과 같은 것이 된다.

all i, j : nat & multp(i,j):nat 및 multp(i, j) = i*j

이는 다음을 통해 올바르게 나타날 수 있다.

1. 재귀가 종료됨을 증명하는 것(이것은 각 단계에서 숫자가 작아진다는 것을 증명해야 함)
2. 수학적 유도

대기열 추상 데이터 유형

이것은 잘 알려진 데이터 구조의 상태 기반 모델에서 암묵적 운용 명세서의 사용을 예시하는 고전적인 사례다.큐는 유형의 요소로 구성된 시퀀스로 모델링됨Qelt대표자는Qelt중요하지 않고 토큰 유형으로 정의된다.

종류들

Qelt = 토큰, 큐 = Qelt의 seq;

Q의 Queue 상태: 대기열 끝

작전

ENQUE(e:Qelt) ext wr q:Queue post q = q~^ [e];

디큐()e:Qelt ext q:Queue pre q <> [] post q~ = [e]^q;

IS-REMY()r:bool ext rd q:Queue post r <=>(len q = 0)

은행 시스템 예

VDM-SL 모델의 매우 간단한 예로서 고객 은행 계좌의 세부 정보를 유지하기 위한 시스템을 고려하십시오.고객은 고객 번호(CustNum)로 모델링되며, 계정은 고객 번호(AcNum)로 모델링된다.고객 번호의 표현은 중요하지 않은 것으로 유지되므로 토큰 유형에 의해 모델링된다.잔액과 당좌대월액은 숫자형식으로 모델링한다.

AccNum = 토큰, CustNum = 토큰, 잔고 = int, 초과 인출 = nat;

AccData : 소유자 : CustNum 잔액 : 잔액

State Bank of accountMap : map AccNum to AccData overdraftMap : 설정된 모든 rng accountMap & a.balance >= -overdraftMap(a. 소유자)에 대해 CustNum to Charfused Map.

운영의 경우: NEWC는 새로운 고객 번호를 할당한다.

작업 NEC(od : 당좌대월)r : 커스터Num extrawdMap : 설정된 dom ~overdraftMap 및 당좌대월Map = ~overdraftMap ++ {r -> od};

NEWAC는 새로운 계좌 번호를 할당하고 잔액을 0으로 설정한다.

NEWAC(cu : CustNum)r : AccNum ext wr accountMap : adap AcData rd overwardMap CustNum to CharchwardMap pre cu in set dom adcountMap~ and accountMap = accountMap~ ++{r_AccData(cu,0)}

ACINF는 고객의 모든 계정 잔액을 잔액에 맞는 계좌 번호 맵으로 반환한다.

ACINF(cu : CustNum)r : Adap AccNum to Balance ext rd 계정맵 : r = {an -> accData post r = {an -> accountMap(an).balance in set dom 계정Map & an.소유자 = cu}

툴 지원

VDM을 지원하는 다양한 툴:

• VDMTools는 CSK Systems에서 소유, 마케팅, 유지보수 및 개발한 VDM 및 VDM++를 위한 선도적인 상용 도구로, 덴마크 회사 IFAD에서 개발한 이전 버전을 기반으로 구축된다.설명서와 실제 자습서를 이용할 수 있다.모든 라이센스는 툴의 전체 버전에 대해 무료로 이용할 수 있다.풀버전은 자바와 C++에 대한 자동 코드 생성, 동적 링크 라이브러리 및 CORBA 지원을 포함한다.
• 서곡은 Eclipse 플랫폼 위에 VDM++를 자유롭게 이용할 수 있는 툴 지원을 제공하는 것을 목적으로 하는 커뮤니티 기반의 오픈 소스 이니셔티브다.그것의 목적은 산업 응용, 연구 및 교육에 유용한 상호운용 가능한 도구의 프레임워크를 개발하는 것이다.
• VDM-Mode는 VDM-SL, VDM++ 및 VDM-RT를 사용하여 VDM 사양을 작성하기 위한 Emacs 패키지 모음입니다.구문 강조 및 편집, 즉석 구문 확인, 템플릿 완성 및 통역 지원을 지원한다.
• SpecBox: Adelard에서 제공하는 구문 검사, 간단한 의미 검사, LaTeX 파일 생성 등을 통해 사양을 수학적 표기법으로 인쇄할 수 있다.이 도구는 자유롭게 사용할 수 있지만 더 이상 유지되지 않고 있다.
• LaTeX와 LaTeX2e 매크로는 ISO 표준 언어의 수학적 구문에 VDM 모델의 발표를 지원하기 위해 이용 가능하다.그것들은 영국의 국립물리연구소에 의해 개발되었고 유지되고 있다.문서와 매크로는 온라인에서 이용할 수 있다.

산업 경험

VDM은 다양한 애플리케이션 도메인에 광범위하게 적용되어 왔다.이러한 애플리케이션 중 가장 잘 알려진 애플리케이션은 다음과 같다.

• Ada와 CHIL 컴파일러:유럽 최초로 검증된 에이다 컴파일러는 VDM을 사용하여 Dansk Datamatik Center에 의해 개발되었다.^[8] 마찬가지로 CHIL과 Modula-2의 의미론도 VDM을 사용한 표준에 설명되었다.
• ConForm: 영국 항공우주국의 실험은 기존의 신뢰할 수 있는 게이트웨이의 개발과 VDM을 이용한 개발을 비교한 것이다.
• 먼지-전문가 : 영국의 아델라드가 산업용 플랜트 배치에서 안전성이 적절하다고 판단하는 안전 관련 적용을 위해 실시하는 프로젝트.
• VDMTools 개발: VDMTools 제품군의 대부분의 구성요소는 VDM을 사용하여 자체 개발된다.이러한 개발은 덴마크의 IFAD와 일본의 CSK에서 이루어졌다.^[9]
• TradeOne: 일본 증권거래소를 위해 CSK 시스템이 개발한 TradeOne 백오피스 시스템의 특정 핵심 구성 요소는 VDM을 사용하여 개발되었다. VDM이 개발한 구성 요소의 개발자 생산성과 결함 밀도에 대한 비교 측정은 기존의 코드와 비교된다.
• FeliCa Networks는 휴대폰 어플리케이션용 집적회로를 위한 운영체제의 개발을 보고했다.

정제

VDM 사용은 매우 추상적인 모델에서 시작하여 이를 구현으로 발전시킨다.각 단계에는 데이터 재조립 후 작업 분해가 포함된다.

데이터 재조정은 추상 데이터 유형을 보다 구체적인 데이터 구조로 발전시키는 반면, 운용 분해는 운용과 기능의 암묵적 사양(추상)을 선택한 컴퓨터 언어로 직접 구현할 수 있는 알고리즘으로 발전시킨다.

${\displaystyle {\begin{array}{ rcl }{\textbf {Specification}}&&{\textbf {Implementation}}\\\hline {\text{Abstract data type}}&\xrightarrow {\text{Data reification}} &{\text{Data structure}}\\{\text{Operations}}&{\xrightarrow[{\text{Operation decomposition}}]{}}&{\text{Algorithms}}\end{array}}}$

데이터 재조정

데이터 재조정(단계적 세분화)에는 규격에 사용된 추상적 데이터 유형의 보다 구체적인 표현을 찾는 것이 포함된다.구현에 도달하기 전에 몇 가지 단계가 있을 수 있다.추상 데이터 표현을 위한 각 재조정 단계ABS_REP새로운 대표직을 제안하는 것을 포함한다.NEW_REP. 새로운 표현이 정확하다는 것을 보여주기 위해, 관련된 검색 함수를 정의한다.NEW_REP로ABS_REP, 즉.retr : NEW_REP -> ABS_REP데이터 재화의 정확성은 적절성 입증에 달려 있다.

모두 A:ABS_REP & existance r:NEW_REP & a = ret(r)

데이터 표현이 변경되었으므로, 작동과 기능이 작동하도록 갱신할 필요가 있다.NEW_REP새로운 운영과 기능은 새로운 표현에 대한 모든 데이터 유형의 불변성을 보존하도록 보여져야 한다.새로운 운용과 기능이 원래 규격에서 발견된 것을 모델링한다는 것을 증명하기 위해서는 다음 두 가지 입증 의무를 이행할 필요가 있다.

• 도메인 규칙:

forall r: NEW_REP & pre-OPA(r) => pre-OPR(r)

• 모델링 규칙:

~r,r:NEW_REP&pre-OPA(~r) 및 post-OPR(~r,r) =>post-OPA(retr(~r,), retri(r)

데이터 재조정 예

사업 보안 시스템에서는 근로자에게 신분증을 주고, 공장 출입 시 신분증을 카드 판독기에 넣어 준다.필요한 작업:

• INIT()시스템을 초기화하고, 공장이 비어 있다고 가정한다.
• ENTER(p : Person)작업자가 공장에 들어가고 있다는 것을 기록한다. 작업자의 세부사항은 신분증에서 읽는다.)
• EXIT(p : Person)노동자가 공장을 빠져나간다는 것을 기록하다.
• IS-PRESENT(p : Person) r : bool지정된 작업자가 공장에 있는지 여부를 검사한다.

공식적으로, 이것은 다음과 같다.

종류들

Person = 토큰, Workers = Person 집합;

사전 AWCCS 상태:일꾼의 끝

작전

INIT() ext wr pres:사전 작업 후 작업자 = {};

ENTER(p : Person) ext wr pres : 사전 설정된 사전 p p에 없는 작업자 사전 p = 사전 ~ 사전 조합 {p};

EXIT(p : Person) ext wr p: 사전 설정된 사전 p의 작업자 사전 p = 사전 p~\{p};

IS-PRESS(p : Person) r : bool ext rd pres : 작업자는 r <=> p를 set pres에 게시한다.

대부분의 프로그래밍 언어는 집합에 필적하는 개념을 가지고 있기 때문에(흔히 배열의 형태로 나타나기 때문에, 명세서의 첫 번째 단계는 시퀀스의 관점에서 데이터를 표현하는 것이다.동일한 작업자가 두 번 나타나는 것을 원치 않기 때문에, 우리는 새로운 데이터 유형에 불변성을 추가해야 하기 때문에 이러한 시퀀스는 반복을 허용하지 않아야 한다.이 경우 순서는 중요하지 않기 때문에[a,b]와 같다[b,a].

비엔나 개발 방법은 모델 기반 시스템에 유용하다.그 시스템이 시간 기반이라면 적절하지 않다.그러한 경우, 통신 시스템의 미적분학(CCS)이 더 유용하다.

참고 항목

• 형식 방법
• 형식 사양
• 피진 코드
• 술어 논리학
• 명제 미적분학
• Z 사양 언어, VDM-SL의 주요 대안(비교)
• 프로그래밍의 통일 이론에 근거한 VDM-SL과 CSP의 조합으로, 시스템 모델링 시스템(SoS)을 위해 개발된 COMBACH 모델링 언어

추가 읽기

• Bjørner, Dines; Cliff B. Jones (1978). The Vienna Development Method: The Meta-Language, Lecture Notes in Computer Science 61. Berlin, Heidelberg, New York: Springer. ISBN 978-0-387-08766-5.
• O'Regan, Gerard (2006). Mathematical Approaches to Software Quality. London: Springer. ISBN 978-1-84628-242-3.
• Cliff B. Jones, ed. (1984). Programming Languages and Their Definition — H. Bekič (1936-1982). Lecture Notes in Computer Science. Vol. 177. Berlin, Heidelberg, New York, Tokyo: Springer-Verlag. doi:10.1007/BFb0048933. ISBN 978-3-540-13378-0.
• Fitzgerald, J.S.와 Larsen, P.G. 모델링 시스템: 소프트웨어 엔지니어링의 실용적인 도구와 기술케임브리지 대학 출판부, 1998 ISBN 0-521-62348-0 (일본판 펍).이와나미 쇼텐 2003 ISBN 4-005609-3).^[10]
• Fitzgerald, J.S., Larsen, P.G, Mukherjee, P, Plat, N. 및 Verhoef, M. Validated Designs for Object-orient Systems.Springer Verlag 2005.ISBN 1-85233-881-4.지원 웹 사이트[1]에는 예시와 무료 도구 지원이 포함된다.^[11]
• 존스, C.B. VDM을 이용한 체계적 소프트웨어 개발, 프렌티스 홀 1990.ISBN 0-13-880733-7.온라인에서 무료로 이용 가능: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip
• Bjørner, D. 및 Jones, C.B., 공식 사양 및 소프트웨어 개발 프렌티스 홀 인터내셔널, 1982.ISBN 0-13-880733-7
• J. Dawes, Pitman 1991 VDM-SL 참조 가이드.ISBN 0-273-03151-1
• 국제 표준화 기구, 정보 기술 – 프로그래밍 언어, 그 환경 및 시스템 소프트웨어 인터페이스 – Vienna 개발 방법 – 사양 언어 – Part 1: 기본 언어 ISO/IEC 13817-1, 1996년 12월.
• 존스, C.B., 소프트웨어 개발: 프렌티스 홀 인터내셔널, 1980.ISBN 0-13-821884-6
• Jones, C.B. 및 Shaw, R.C.(에드), Fratice Hall International, 1990년 체계적 소프트웨어 개발 사례 연구.ISBN 0-13-880733-7
• Bicargui, J.C., Fitzgerald, J.S., Lindsay, P.A., Moore, R. and Ritchie, B. Proof in VDM: 실무자 가이드.Springer Verlag Computing and Information Technology(FACIT), 1994.ISBN 3-540-19813-X.

참조

외부 링크

• VDM 및 VDM++에 대한 정보(archive.org 참조)
• VDL(Vienna Definition Language)