Viyana Geliştirme Yöntemi - Vienna Development Method

Viyana Geliştirme Yöntemi ( VDM ) en köklü biridir biçimsel yöntemlere bilgisayar tabanlı sistemlerin geliştirilmesi için. 1970'lerde Viyana IBM Laboratuvarı'nda yapılan çalışmalardan yola çıkarak, resmi bir belirtim diline (VDM Belirtim Dili) (VDM-SL) dayalı bir grup teknik ve aracı içerecek şekilde büyümüştür. Nesne yönelimli ve eşzamanlı sistemlerin modellenmesini destekleyen genişletilmiş bir VDM++ formuna sahiptir . VDM desteği, modellerin özelliklerini test etme ve kanıtlama ve doğrulanmış VDM modellerinden program kodu oluşturma desteği de dahil olmak üzere, modelleri analiz etmek için ticari ve akademik araçları içerir. Orada VDM ve araçlarının endüstriyel kullanım tarihidir ve biçimcilik araştırma büyüyen bir kritik sistemlerin mühendislik dikkate değer katkıları yol açmıştır derleyici , eş zamanlı sistemler ve de mantık için bilgisayar bilimi .

Felsefe

Bilgi işlem sistemleri, VDM-SL'de programlama dilleri kullanılarak elde edilebilecek olandan daha yüksek bir soyutlama düzeyinde modellenebilir, bu da sistem geliştirmenin erken bir aşamasında tasarımların analizine ve kusurlar dahil temel özelliklerin tanımlanmasına olanak tanır. Doğrulanmış modeller, bir iyileştirme süreci ile ayrıntılı sistem tasarımlarına dönüştürülebilir. Dilin, modellerin özelliklerinin yüksek düzeyde bir güvenceye sahip olduğunun kanıtlanmasını sağlayan biçimsel bir semantiği vardır. Ayrıca yürütülebilir bir alt kümesine sahiptir, böylece modeller test edilerek analiz edilebilir ve grafiksel kullanıcı arayüzleri aracılığıyla yürütülebilir, böylece modeller, modelleme diline aşina olmayan uzmanlar tarafından değerlendirilebilir.

Tarih

İçinde VDM-SL kökenleri IBM in Laboratuvarı Viyana dilinin ilk sürümü denirdi V ienna D efinition L anguage (VDL). VDL, düz anlamsal anlambilim sağlayan VDM - Meta-IV'ün aksine , temel olarak işlevsel anlambilim açıklamaları vermek için kullanıldı.

1972'nin sonlarına doğru, Viyana grubu dikkatlerini bir dil tanımından sistematik olarak bir derleyici geliştirme sorununa çevirdi. Kabul edilen genel yaklaşım "Viyana Geliştirme Yöntemi" olarak adlandırılmıştır... Fiili olarak benimsenen meta-dil ("Meta-IV"), PL/1'in (ECMA 74'te verildiği gibi - ilginç bir şekilde "resmi" bir bölümün) büyük bölümlerini tanımlamak için kullanılır. soyut tercüman olarak yazılmış standartlar belgesi") BEKIČ 74.»

Meta-IV ile Schorre'nin Meta-II dili veya onun ardılı Tree Meta arasında hiçbir bağlantı yoktur ; bunlar resmi problem tanımlamalarına uygun olmaktan ziyade derleyici-derleyici sistemleriydi.

Böylece Meta-IV, PL/I programlama dilinin "ana bölümlerini tanımlamak için kullanıldı" . Meta-IV ve VDM-SL kullanılarak geriye dönük olarak açıklanan veya kısmen açıklanan diğer programlama dilleri, BASIC programlama dili , FORTRAN , APL programlama dili , ALGOL 60, Ada programlama dili ve Pascal programlama dilini içerir . Meta-IV, genellikle Danimarka, İngiliz ve İrlanda Okulları olarak tanımlanan çeşitli varyantlara dönüştü.

Cliff Jones'un VDM'nin özellikle dil tanımı ve derleyici tasarımı ile ilgili olmayan yönleri üzerine çalışmasından türetilen "İngiliz Okulu" (Jones 1980, 1990). Zengin bir temel tür koleksiyonundan oluşturulan veri türlerinin kullanımı yoluyla kalıcı durumu modellemeyi vurgular. İşlevsellik tipik olarak durum üzerinde yan etkileri olabilen ve çoğunlukla bir ön koşul ve son koşul kullanılarak örtük olarak belirtilen işlemler aracılığıyla tanımlanır. "Danimarka Okulu" ( Bjørner ve diğerleri 1982), daha büyük ölçüde kullanılan açık operasyonel spesifikasyonlarla yapıcı bir yaklaşımı vurgulama eğiliminde olmuştur. Danimarka okulunda çalışmak, ilk Avrupa onaylı Ada derleyicisine yol açtı .

1996'da dil için bir ISO Standardı yayınlandı (ISO, 1996).

VDM özellikleri

VDM-SL ve VDM++ sözdizimi ve semantiği, VDMTools dil kılavuzlarında ve mevcut metinlerde ayrıntılı olarak açıklanmıştır. ISO Standardı, dilin anlambiliminin resmi bir tanımını içerir. Bu makalenin geri kalanında, ISO tanımlı değişim (ASCII) sözdizimi kullanılır. Bazı metinler daha özlü bir matematiksel sözdizimi tercih eder .

Bir VDM-SL modeli, veriler üzerinde gerçekleştirilen işlevsellik açısından verilen bir sistem açıklamasıdır. Bir dizi veri türü tanımından ve bunlar üzerinde gerçekleştirilen işlevlerden veya işlemlerden oluşur.

Temel türler: sayısal, karakter, belirteç ve alıntı türleri

VDM-SL, aşağıdaki gibi temel tip modelleme numaraları ve karakterleri içerir:

Temel tipler

bool	Boole veri türü	yanlış doğru
nat	doğal sayılar (sıfır dahil)	0, 1, 2, 3, 4, 5 ...
nat1	doğal sayılar (sıfır hariç)	1, 2, 3, 4, 5, ...
int	tam sayılar	..., -3, -2, -1, 0, 1, 2, 3, ...
rat	rasyonel sayılar	a/b , burada a ve b tam sayılardır, b 0 değildir
real	gerçek sayılar	...
char	karakterler	A, B, C, ...
token	yapısız belirteçler	...
<A>	değeri içeren alıntı türü <A>	...

Veri türleri, modellenen sistemin ana verilerini temsil edecek şekilde tanımlanır. Her tip tanımı, yeni bir tip ismi tanıtır ve temel tipler veya halihazırda tanıtılan tipler açısından bir temsil verir. Örneğin, bir oturum açma yönetim sistemi için bir tür modelleme kullanıcı tanımlayıcıları aşağıdaki gibi tanımlanabilir:

types
UserId = nat

Veri tiplerine ait değerlerin manipüle edilmesi için değerler üzerinde operatörler tanımlanır. Böylece eşitlik ve eşitsizlik gibi Boolean operatörleri gibi doğal sayılar toplama, çıkarma vb. Dil, gerçek sayılar için bir maksimum veya minimum temsil edilebilir sayı veya kesinlik belirlemez. Bu tür kısıtlamalar, veri türü değişmezleri aracılığıyla her modelde gerekli oldukları yerde tanımlanır - tanımlı türün tüm öğeleri tarafından uyulması gereken koşulları gösteren Boole ifadeleri. Örneğin, kullanıcı tanımlayıcılarının 9999'dan büyük olmaması gerekliliği aşağıdaki gibi ifade edilir (burada <=doğal sayılardaki "küçük veya eşittir" Boole operatörüdür):

UserId = nat
inv uid == uid <= 9999

Değişmezler keyfi olarak karmaşık mantıksal ifadeler olabileceğinden ve tanımlanmış bir türün üyeliği yalnızca değişmezi karşılayan değerlerle sınırlı olduğundan, VDM-SL'deki tür doğruluğu her durumda otomatik olarak kararlaştırılamaz.

Diğer temel türler, karakterler için char içerir. Bazı durumlarda, bir türün temsili modelin amacı ile ilgili değildir ve yalnızca karmaşıklık ekler. Bu gibi durumlarda, türün üyeleri yapısız belirteçler olarak temsil edilebilir. Belirteç türlerinin değerleri yalnızca eşitlik için karşılaştırılabilir - üzerlerinde başka operatörler tanımlanmaz. Belirli adlandırılmış değerlerin gerekli olduğu durumlarda, bunlar alıntı türleri olarak sunulur. Her alıntı türü, türün kendisiyle aynı adı taşıyan bir adlandırılmış değerden oluşur. Alıntı türlerinin değerleri (alıntı değişmezleri olarak bilinir) yalnızca eşitlik için karşılaştırılabilir.

Örneğin, bir trafik sinyali denetleyicisinin modellenmesinde, trafik sinyalinin renklerini alıntı türleri olarak temsil edecek değerlerin tanımlanması uygun olabilir:

<Red>, <Amber>, <FlashingAmber>, <Green>

Tip yapıcılar: birleşim, ürün ve kompozit türleri

Tek başına temel tipler sınırlı değere sahiptir. Yeni, daha yapılandırılmış veri türleri, tür oluşturucular kullanılarak oluşturulur.

Temel Tip Yapıcılar

T1 | T2 | ... | Tn	Türlerin birliği T1,...,Tn
T1*T2*...*Tn	Kartezyen ürün türleri T1,...,Tn
T :: f1:T1 ... fn:Tn	Kompozit (Kayıt) tipi

En temel tür oluşturucu, önceden tanımlanmış iki türün birleşimini oluşturur. Tür (A|B), A türünün tüm öğelerini ve türün tümünü içerir B. Trafik sinyali denetleyici örneğinde, bir trafik sinyalinin rengini modelleyen tip aşağıdaki gibi tanımlanabilir:

SignalColour =  <Red> | <Amber> | <FlashingAmber> | <Green>

VDM-SL'de numaralandırılmış türler , yukarıda belirtildiği gibi, teklif türlerinde birleşimler olarak tanımlanır.

Kartezyen ürün türleri de VDM-SL'de tanımlanabilir. Tür (A1*…*An), ilk öğesi türden A1, ikincisi türden A2vb. olan tüm değer gruplarından oluşan türdür . Bileşik veya kayıt türü, alanlar için etiketler içeren Kartezyen bir üründür. tip

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

etiketli alanları olan Kartezyen üründür f1,…,fn. Bir tür öğesi T, kurucu parçalarından yazılı bir kurucu tarafından oluşturulabilir mk_T. Tersine, bir tür öğesi verildiğinde T, adlandırılmış bileşeni seçmek için alan adları kullanılabilir. Örneğin, tür

Date :: day:nat1
        month:nat1
        year:nat
inv mk_Date(d,m,y) == d <=31 and m<=12

basit bir tarih türü modeller. Değer mk_Date(1,4,2001)1 Nisan 2001'e karşılık gelir. Bir tarih verildiğinde difade d.month, ayı temsil eden doğal bir sayıdır. İstenirse, ay başına gün ve artık yıl kısıtlamaları değişmeze dahil edilebilir. Bunları birleştirmek:

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

Koleksiyonlar

Koleksiyon türleri, değer gruplarını model alır. Kümeler, değerler arasındaki yinelemenin bastırıldığı sonlu sırasız koleksiyonlardır. Diziler, çoğaltmanın meydana gelebileceği ve eşlemelerin iki değer kümesi arasındaki sonlu karşılıkları temsil ettiği sonlu sıralı koleksiyonlardır (listeler).

Setler

Küme türü oluşturucusu ( önceden tanımlanmış bir tür set of Tolduğu yerde yazılır T), türünden alınan tüm sonlu değer kümelerinden oluşan türü oluşturur T. Örneğin, tür tanımı

UGroup = set of UserId

UGrouptüm sonlu değer kümelerinden oluşan bir tür tanımlar UserId. Birleşimlerini, kesişimlerini oluşturmak, uygun ve katı olmayan alt küme ilişkilerini belirlemek vb. için kümeler üzerinde çeşitli operatörler tanımlanmıştır.

Kümelerdeki ana operatörler (s, s1, s2 kümelerdir)

{a, b, c}	Set numaralandırma Unsurların kurgusu a, bvec
{x | x:T & P(x)}	Set anlama: set xtüründen TşekildeP(x)
{i, ..., j}	Aralığındaki tamsayılar kümesi iiçinj
e in set s	e kümenin bir elemanıdır s
e not in set s	e kümenin bir elemanı değildir s
s1 union s2	kümelerin birliği s1ves2
s1 inter s2	Kümelerin kesişimi s1ves2
s1 \ s2	Kümelerin farkını ayarlayın s1ves2
dunion s	küme kümelerinin dağıtılmış birliği s
s1 psubset s2	s1 (uygun) bir alt kümesidir s2
s1 subset s2	s1 bir (zayıf) alt kümesidir s2
card s	kümenin kardinalitesi s

diziler

Sonlu dizi türü yapıcısı ( önceden tanımlanmış bir tür seq of Tolduğu yerde yazılır T), türden alınan tüm sonlu değer listelerinden oluşan türü oluşturur T. Örneğin, tür tanımı

String = seq of char

StringTüm sonlu karakter dizilerinden oluşan bir tür tanımlar . Birleştirme, elemanların ve alt dizilerin seçimi vb. için diziler üzerinde çeşitli operatörler tanımlanmıştır. Bu operatörlerin çoğu, belirli uygulamalar için tanımlanmadıkları için kısmidir. Örneğin, yalnızca üç öğe içeren bir dizinin 5. öğesinin seçilmesi tanımsızdır.

Bir dizideki öğelerin sırası ve tekrarı önemlidir, bu nedenle ' [a, b]ye eşit değildir [b, a]ve ' [a]ye eşit değildir [a, a].

Dizilerdeki ana operatörler (s, s1,s2 dizilerdir)

[a, b, c]	Sekans numaralandırma: elemanları dizisi a, bvec
[f(x) | x:T & P(x)]	Sekans anlama: ifadelerin dizisi f(x)her xbir (sayısal) tip Tşekilde P(x)tutar ( xsayısal olarak alınan değerler)
hd s	Baş (ilk eleman) s
tl s	Kuyruk (kafa alındıktan sonra kalan sıra) s
len s	Uzunluğu s
elems s	öğeleri kümesi s
s(i)	iİnci unsurus
inds s	dizi için indeksler seti s
s1^s2	dizilerin birleştirilmesiyle oluşturulan dizi s1ves2

Haritalar

Sonlu bir eşleme, aralığın etki alanı indeksleme öğeleriyle etki alanı ve aralık olmak üzere iki küme arasındaki bir yazışmadır. Bu nedenle sonlu bir fonksiyona benzer. VDM-SL'deki eşleme türü yapıcısı ( map T1 to T2nerede T1ve T2önceden tanımlanmış türler olarak yazılır ), T1değer kümelerinden değer kümelerine kadar tüm sonlu eşlemelerden oluşan türü oluşturur T2. Örneğin, tür tanımı

Birthdays = map String to Date

BirthdaysKarakter dizelerini eşleyen bir tür tanımlar Date. Yine, eşlemeler üzerinde, eşlemeye indeksleme, eşlemeleri birleştirme, alt eşlemelerin üzerine yazma, çıkarma işlemleri için operatörler tanımlanır.

Eşlemelerdeki ana operatörler

{a |-> r, b |-> s}	Eşleme numaralandırması: şuna aeşlenir r, bşuna eşlenirs
{x |-> f(x) | x:T & P(x)}	Eşleme anlama: şu şekilde tür için herkes için xeşlenir :f(x)xTP(x)
dom m	etki alanı m
rng m	aralığı m
m(x)	m uygulanan x
m1 munion m2	Eşlemelerin birliği m1ve m2( m1, m2çakıştıkları yerde tutarlı olmalıdır)
m1 ++ m2	m1 üzerine yazılan m2

yapılandırma

VDM-SL ve VDM++ notasyonları arasındaki temel fark, yapılandırmanın ele alınma şeklidir. VDM-SL'de geleneksel bir modüler uzantı bulunurken VDM++, sınıflar ve kalıtım ile geleneksel nesne yönelimli bir yapılandırma mekanizmasına sahiptir.

VDM-SL'de Yapılandırma

VDM-SL için ISO standardında farklı yapılandırma ilkelerini içeren bilgilendirici bir ek bulunmaktadır. Bunların hepsi modüllerle geleneksel bilgi gizleme ilkelerini takip eder ve şu şekilde açıklanabilir:

• Modül adlandırma : Her modül sözdizimsel olarak anahtar kelime ve moduleardından modülün adı ile başlatılır . Modülün sonunda anahtar kelime ve endardından tekrar modülün adı yazılır.
• İçe Aktarma : Diğer modüllerden dışa aktarılan tanımları içe aktarmak mümkündür. Bu, anahtar kelimeyle başlayan ve ardından farklı modüllerden bir dizi içe aktarmanın izlediği bir içe aktarma bölümünde yapılır imports. Bu modül içe aktarmalarının her biri, anahtar sözcük ve fromardından modülün adı ve bir modül imzası ile başlatılır . Modül imzası ya basitçe anahtar kelime olabilir allo modülünden ihraç bütün tanımların ithalat gösteren ya da ithal imzaların bir dizisi olabilir. İçe aktarma imzaları türlere, değerlere, işlevlere ve işlemlere özeldir ve bunların her biri karşılık gelen anahtar sözcükle başlatılır. Ek olarak, bu içe aktarma imzaları, erişim arzusu olan yapıları adlandırır. Ek olarak, isteğe bağlı tip bilgisi mevcut olabilir ve son olarak, içe aktarma sırasında yapıların her birini yeniden adlandırmak mümkündür . Türler structiçin, belirli bir türün iç yapısına erişmek isteniyorsa , anahtar sözcüğün de kullanılması gerekir .
• Dışa Aktarma : Bir modülün diğer modüllerin erişmesini istediği tanımlar, anahtar kelime ve exportsardından bir dışa aktarma modülü imzası kullanılarak dışa aktarılır. İhracat modülü imza ya basitçe anahtar kelime oluşabilir allveya ihracat imzaların bir dizi olarak. Bu tür dışa aktarma imzaları türlere, değerlere, işlevlere ve işlemlere özeldir ve bunların her biri karşılık gelen anahtar sözcükle başlatılır. Bir türün iç yapısını dışa aktarmak istendiğinde, anahtar kelime structkullanılmalıdır.
• Daha egzotik özellikler : VDM-SL araçlarının önceki sürümlerinde, parametreli modüller ve bu tür modüllerin somutlaştırılması için de destek vardı. Ancak bu özellikler, endüstriyel uygulamalarda neredeyse hiç kullanılmadıkları ve bu özelliklerle ilgili önemli sayıda takım zorlukları olduğu için 2000 civarında VDMTools'dan çıkarıldı.

VDM++'da yapılandırma

VDM++'da yapılandırma, sınıflar ve çoklu kalıtım kullanılarak yapılır. Anahtar kavramlar şunlardır:

• Sınıf : Her sınıf sözdizimsel olarak anahtar kelime ve classardından sınıfın adı ile başlar. Bir sınıfın sonunda anahtar kelime endyazılır ve ardından tekrar sınıfın adı gelir.
• Kalıtım : Bir sınıfın yapıları diğer sınıflardan miras alması durumunda, sınıf başlığındaki sınıf adının ardından anahtar kelimeler ve is subclass ofardından virgülle ayrılmış bir üst sınıf adları listesi gelebilir .
• Erişim değiştiricileri : VDM++'da bilgi gizleme, erişim değiştiricileri kullanan çoğu nesne yönelimli dilde olduğu gibi yapılır. VDM++'da tanımlar varsayılan olarak özeldir, ancak tüm tanımların önünde erişim değiştirici anahtar sözcüklerinden birini kullanmak mümkündür: private, publicve protected.

Modelleme işlevselliği

fonksiyonel modelleme

VDM-SL'de fonksiyonlar bir modelde tanımlanan veri tipleri üzerinden tanımlanır. Soyutlama desteği, bir fonksiyonun nasıl hesaplanacağını söylemeden hesaplaması gereken sonucu karakterize etmenin mümkün olmasını gerektirir. Bunu yapmak için ana mekanizma , bir sonucu hesaplayan bir formül yerine, girdi ve sonuç değişkenleri üzerinde bir post-koşul olarak adlandırılan mantıksal bir yüklemin sonucun özelliklerini verdiği örtük fonksiyon tanımıdır . Örneğin, bir doğal sayının karekökünü hesaplamak için bir fonksiyon aşağıdaki gibi tanımlanabilir: SQRT

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

Burada sonkoşul, sonucu hesaplamak için bir yöntem tanımlamaz, rancak hangi özelliklerin ona sahip olduğunun varsayılabileceğini belirtir. Bunun geçerli bir karekök döndüren bir işlevi tanımladığını unutmayın; pozitif veya negatif kök olması gerekliliği yoktur. Yukarıdaki belirtim, örneğin, 4'ün negatif kökünü, ancak diğer tüm geçerli girdilerin pozitif kökünü döndüren bir işlev tarafından karşılanacaktır. VDM-SL'deki işlevlerin deterministik olması gerektiğine dikkat edin, böylece yukarıdaki örnek belirtimi karşılayan bir işlevin aynı girdi için her zaman aynı sonucu döndürmesi gerekir.

Son koşul güçlendirilerek daha kısıtlı bir işlev belirtimine ulaşılır. Örneğin, aşağıdaki tanım, pozitif kökü döndürmek için işlevi kısıtlar.

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

Tüm işlev belirtimleri, yalnızca giriş değişkenleri üzerinde mantıksal yüklemler olan ve işlev yürütüldüğünde karşılanacağı varsayılan kısıtlamaları tanımlayan ön koşullarla sınırlandırılabilir . Örneğin, yalnızca pozitif gerçek sayılar üzerinde çalışan bir karekök hesaplama işlevi aşağıdaki gibi belirtilebilir:

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

Ön koşul ve son koşul birlikte , işlevi uyguladığını iddia eden herhangi bir program tarafından yerine getirilmesi gereken bir sözleşme oluşturur. Ön koşul, işlevin son koşulu karşılayan bir sonuç döndürmeyi garanti ettiği varsayımları kaydeder. Ön koşulunu karşılamayan girdilerde bir işlev çağrılırsa, sonuç tanımsızdır (aslında, sonlandırma garanti bile edilmez).

VDM-SL, işlevsel bir programlama dili tarzında yürütülebilir işlevlerin tanımını da destekler. Bir in açık işlev tanımı, sonuç girdilerden bir ekspresyonu ile tanımlanır. Örneğin, bir sayı listesinin karelerinin bir listesini üreten bir fonksiyon aşağıdaki gibi tanımlanabilir:

SqList: seq of nat -> seq of nat
SqList(s) == if s = [] then [] else [(hd s)**2] ^ SqList(tl s)

Bu özyinelemeli tanım, girdi ve sonuç türlerini veren bir işlev imzası ve bir işlev gövdesinden oluşur. Aynı işlevin örtük bir tanımı aşağıdaki biçimi alabilir:

SqListImp(s:seq of nat)r:seq of nat
post len r = len s and
     forall i in set inds s & r(i) = s(i)**2

Açık tanım, basit bir anlamda, örtük olarak belirtilen işlevin bir uygulamasıdır. Bir örtük belirtime göre açık bir fonksiyon tanımının doğruluğu aşağıdaki gibi tanımlanabilir.

Örtük bir belirtim verildiğinde:

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

ve açık bir işlev:

f:T_p -> T_r

iff şartnamesini karşıladığını söylüyoruz :

forall p in set T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))

Bu nedenle, " fdoğru bir uygulamadır", " fbelirtimi karşılıyor " olarak yorumlanmalıdır .

Durum tabanlı modelleme

VDM-SL'de fonksiyonların kalıcı bir global değişkenin durumunu değiştirme gibi yan etkileri yoktur. Bu, birçok programlama dilinde faydalı bir yetenektir, dolayısıyla benzer bir kavram mevcuttur; Durum değişkenlerini değiştirmek için işlevler yerine işlemler kullanılır ( globals olarak da bilinir ).

Örneğin, tek bir değişkenden oluşan bir durumumuz varsa someStateRegister : nat, bunu VDM-SL'de şöyle tanımlayabiliriz:

state Register of
  someStateRegister : nat
end

VDM++'da bunun yerine şu şekilde tanımlanır:

instance variables
  someStateRegister : nat

Bu değişkene bir değer yükleme işlemi şu şekilde belirtilebilir:

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

Dış görünüş maddesinin ( ext) devlet parça işlemi ile ulaşılabilir belirtir; rdsalt okunur erişimi ve wrokuma/yazma erişimi olduğunu gösterir.

Bazen, bir durumun değiştirilmeden önceki değerine atıfta bulunmak önemlidir; örneğin, değişkene bir değer ekleme işlemi şu şekilde belirtilebilir:

ADD(i:nat)
ext wr someStateRegister : nat
post someStateRegister = someStateRegister~ + i

Son ~koşuldaki durum değişkenindeki sembolün, işlemin yürütülmesinden önceki durum değişkeninin değerini gösterdiği yerde.

Örnekler

max fonksiyonu

Bu, örtük bir işlev tanımının bir örneğidir. İşlev, bir dizi pozitif tamsayıdan en büyük öğeyi döndürür:

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

Sonkoşul, sonucu elde etmek için bir algoritma tanımlamak yerine sonucu karakterize eder. Ön koşul gereklidir, çünkü küme boşken hiçbir işlev küme s'de bir r döndüremez.

Doğal sayı çarpımı

multp(i,j:nat)r:nat
pre true
post r = i*j

Aşağıdakilerin forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))açık bir tanımına ispat yükümlülüğünün uygulanması multp:

multp(i,j) ==
 if i=0
 then 0
 else if is-even(i)
      then 2*multp(i/2,j)
      else j+multp(i-1,j)

O zaman ispat yükümlülüğü şu hale gelir:

forall i, j : nat & multp(i,j):nat and multp(i, j) = i*j

Bu doğru olarak gösterilebilir:

1. Özyinelemenin sona erdiğini kanıtlamak (bu da her adımda sayıların küçüldüğünü kanıtlamayı gerektirir)
2. matematiksel tümevarım

Kuyruk soyut veri türü

Bu, iyi bilinen bir veri yapısının durum tabanlı bir modelinde örtük işlem belirtiminin kullanımını gösteren klasik bir örnektir. Kuyruk, bir türdeki öğelerden oluşan bir dizi olarak modellenmiştir Qelt. Temsil Qeltönemsizdir ve bu nedenle bir belirteç türü olarak tanımlanır.

types

Qelt = token;
Queue = seq of Qelt;

state TheQueue of
  q : Queue
end

operations

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

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

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

Banka sistemi örneği

Bir VDM-SL modelinin çok basit bir örneği olarak, müşteri banka hesabının ayrıntılarını korumak için bir sistem düşünün. Müşteriler müşteri numaralarına göre modellenir ( CustNum ), hesaplar hesap numaralarına göre modellenir ( AccNum ). Müşteri numaralarının temsilleri önemsiz olarak tutulur ve bu nedenle bir belirteç türüyle modellenir. Bakiyeler ve kredili mevduat hesapları sayısal türlere göre modellenir.

AccNum = token;
CustNum = token;
Balance = int;
Overdraft = nat;

AccData :: owner : CustNum
           balance : Balance

state Bank of
  accountMap : map AccNum to AccData
  overdraftMap : map CustNum to Overdraft
inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and
                                        a.balance >= -overdraftMap(a.owner)

İşlemlerle: NEWC yeni bir müşteri numarası tahsis eder:

operations
NEWC(od : Overdraft)r : CustNum
ext wr overdraftMap : map CustNum to Overdraft
post r not in set dom ~overdraftMap and overdraftMap = ~overdraftMap ++ { r |-> od};

NEWAC yeni bir hesap numarası tahsis eder ve bakiyeyi sıfıra ayarlar:

NEWAC(cu : CustNum)r : AccNum
ext wr accountMap : map AccNum to AccData
    rd overdraftMap map CustNum to Overdraft
pre cu in set dom overdraftMap
post r not in set dom accountMap~ and accountMap = accountMap~ ++ {r|-> mk_AccData(cu,0)}

ACINF , bir müşterinin tüm hesaplarının tüm bakiyelerini, dengelenecek hesap numarası haritası olarak döndürür:

ACINF(cu : CustNum)r : map AccNum to Balance
ext rd accountMap : map AccNum to AccData
post r = {an |-> accountMap(an).balance | an in set dom accountMap & accountMap(an).owner = cu}

Araç desteği

Bir dizi farklı araç VDM'yi destekler:

• VDMTools , Danimarka Şirketi IFAD tarafından geliştirilen önceki sürümleri temel alan, CSK Systems tarafından sahip olunan, pazarlanan, bakımı yapılan ve geliştirilen VDM ve VDM++ için önde gelen ticari araçlardır . Kılavuzları ve pratik bir öğretici mevcuttur. Aracın tam sürümü için tüm lisanslar ücretsiz olarak mevcuttur. Tam sürüm, Java ve C++ için otomatik kod oluşturma, dinamik bağlantı kitaplığı ve CORBA desteği içerir.
• Overture , Eclipse platformunun üstünde VDM++ için ücretsiz olarak kullanılabilen araç desteği sağlamayı amaçlayan topluluk tabanlı bir açık kaynak girişimidir. Amacı, endüstriyel uygulama, araştırma ve eğitim için faydalı olacak birlikte çalışabilir araçlar için bir çerçeve geliştirmektir.
• vdm-mode , VDM-SL, VDM++ ve VDM-RT kullanarak VDM belirtimlerini yazmaya yönelik bir Emacs paketleri koleksiyonudur. Sözdizimi vurgulama ve düzenlemeyi, anında sözdizimi denetimi, şablon tamamlama ve yorumlayıcı desteğini destekler.
• SpecBox : Adelard'dan, sözdizimi denetimi, bazı basit anlamsal denetimler ve özelliklerin matematiksel gösterimde yazdırılmasını sağlayan bir LaTeX dosyasının oluşturulmasını sağlar. Bu araç serbestçe kullanılabilir, ancak daha fazla bakımı yapılmamaktadır.
• LaTeX ve LaTeX2e makroları, ISO Standart Dilinin matematiksel sözdiziminde VDM modellerinin sunumunu desteklemek için mevcuttur. Birleşik Krallık'taki Ulusal Fizik Laboratuvarı tarafından geliştirilmiş ve sürdürülmektedir. Belgeler ve makrolar çevrimiçi olarak mevcuttur.

endüstriyel deneyim

VDM, çeşitli uygulama alanlarında yaygın olarak uygulanmıştır. Bu uygulamalardan en bilinenleri şunlardır:

• Ada ve CHILL derleyicileri : İlk Avrupa onaylı Ada derleyicisi, VDM kullanılarak Dansk Datamatik Center tarafından geliştirilmiştir . Aynı şekilde CHILL ve Modula-2'nin semantiği, standartlarında VDM kullanılarak açıklanmıştır.
• ConForm: British Aerospace'de, güvenilir bir ağ geçidinin geleneksel gelişimini VDM kullanan bir geliştirme ile karşılaştıran bir deney.
• Toz-Uzman: Bir proje içinde Adelard tarafından yürütülen İngiltere'de emniyet endüstriyel tesislerin düzeninde uygun olduğunu belirleyen bir emniyet ile ilgili uygulama için.
• VDMTools'un geliştirilmesi: VDMTools araç takımının çoğu bileşeni, VDM kullanılarak geliştirilmiştir. Bu gelişme de yapılmıştır IFAD içinde Danimarka ve CSK içinde Japonya .
• TradeOne: Japon borsası için CSK sistemleri tarafından geliştirilen TradeOne arka ofis sisteminin belirli temel bileşenleri VDM kullanılarak geliştirildi. VDM tarafından geliştirilen bileşenlerin, geleneksel olarak geliştirilen koda karşı geliştirici üretkenliği ve kusur yoğunluğu için karşılaştırmalı ölçümler mevcuttur.
• FeliCa Networks, cep telefonu uygulamaları için bir entegre devre için bir işletim sistemi geliştirdiğini bildirdi .

arıtma

VDM kullanımı çok soyut bir modelle başlar ve bunu bir uygulamaya dönüştürür. Her adım, verinin somutlaştırılmasını ve ardından işlem ayrıştırmasını içerir .

Veri somutlaştırma, soyut veri türlerini daha somut veri yapılarına dönüştürürken , işlem ayrıştırma, operasyonların (soyut) örtük özelliklerini ve fonksiyonları doğrudan tercih edilen bir bilgisayar dilinde uygulanabilen algoritmalara dönüştürür .

${\displaystyle {\begin{array}{|rcl|}{\textbf {Spesifikasyon}}&&{\textbf {Uygulama}}\\\hline {\text{Soyut veri türü}}&\xrightarrow {\text{Veri reification}} &{\text{Veri yapısı}}\\{\text{İşlemler}}&{\xrightarrow[{\text{İşlem ayrıştırma}}]{}}&{\text{Algoritmalar}}\end{dizi }}}$

Veri somutlaştırma

Veri somutlaştırma (adım adım iyileştirme), bir belirtimde kullanılan soyut veri türlerinin daha somut bir temsilini bulmayı içerir. Bir uygulamaya ulaşılmadan önce birkaç adım olabilir. Soyut bir veri temsili için her şeyleştirme adımı, ABS_REPyeni bir temsil önermeyi içerir NEW_REP. Yeni gösterimin doğru olduğunu göstermek için , örneğin ile ilgili bir geri alma işlevi tanımlanır . Bir veri somutlaştırmasının doğruluğu, yeterliliğin kanıtlanmasına bağlıdır , yani NEW_REPABS_REPretr : NEW_REP -> ABS_REP

forall a:ABS_REP & exists r:NEW_REP & a = retr(r)

Veri gösterimi değiştiğinden, işlem ve fonksiyonların üzerinde çalışacak şekilde güncellenmesi gerekmektedir NEW_REP. Yeni gösterimde herhangi bir veri türü değişmezini korumak için yeni işlemler ve işlevler gösterilmelidir . Yeni işlemlerin ve işlevlerin orijinal şartnamede bulunanları modellediğini kanıtlamak için iki ispat yükümlülüğünü yerine getirmek gerekir:

• Alan kuralı:

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

• Modelleme kuralı:

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

Örnek veri somutlaştırma

Bir iş güvenliği sisteminde çalışanlara kimlik kartları verilir; bunlar fabrikaya giriş ve çıkışta kart okuyuculara beslenir. Gerekli işlemler:

• INIT() sistemi başlatır, fabrikanın boş olduğunu varsayar
• ENTER(p : Person)bir işçinin fabrikaya girdiğini kaydeder; işçi bilgileri kimlik kartından okunur)
• EXIT(p : Person) bir işçinin fabrikadan çıktığını kaydeder
• IS-PRESENT(p : Person) r : bool belirli bir işçinin fabrikada olup olmadığını kontrol eder

Resmi olarak, bu olurdu:

types

Person = token;
Workers = set of Person;

state AWCCS of
  pres: Workers
end

operations

INIT()
ext wr pres: Workers
post pres = {};

ENTER(p : Person)
ext wr pres : Workers
pre p not in set pres
post pres = pres~ union {p};

EXIT(p : Person)
ext wr pres : Workers
pre p in set pres
post pres = pres~\{p};

IS-PRESENT(p : Person) r : bool
ext rd pres : Workers
post r <=> p in set pres~

Çoğu programlama dili, bir kümeyle (genellikle bir dizi biçiminde) karşılaştırılabilir bir konsepte sahip olduğundan, belirtimdeki ilk adım, verileri bir dizi açısından temsil etmektir. Aynı işçinin iki kez görünmesini istemediğimiz için bu diziler tekrara izin vermemelidir, bu nedenle yeni veri türüne bir değişmez eklemeliyiz . Bu durumda, sıralama önemli değildir [a,b], aynı önemlidir [b,a].

Viyana Geliştirme Metodu, model tabanlı sistemler için değerlidir. Sistemin zamana dayalı olması uygun değildir. Bu gibi durumlarda, iletişim sistemleri (CCS) hesabı daha kullanışlıdır.

Ayrıca bakınız

• resmi yöntemler
• Resmi şartname
• Pidgin kodu
• Yüklem mantığı
• önermeler hesabı
• Z belirtim dili , VDM-SL'nin ana alternatifi (karşılaştır)
• VDM-SL ile CSP'nin bir kombinasyonu olan COMPASS Modelleme Dili (CML), Sistem Sistemlerini (SoS) modellemek için geliştirilmiş , Programlamanın Birleştirici Teorilerine dayalıdır.

daha fazla okuma

• Bjørner, Dines; Cliff B. Jones (1978). Viyana Geliştirme Yöntemi: Meta-Dil, Bilgisayar Bilimlerinde Ders Notları 61 . Berlin, Heidelberg, New York: Springer. ISBN'si 978-0-387-08766-5.
• O'Regan, Gerard (2006). Yazılım Kalitesine Matematiksel Yaklaşımlar . Londra: Springer. ISBN'si 978-1-84628-242-3.
• Cliff B. Jones, ed. (1984). Programlama Dilleri ve Tanımları — H. Bekič (1936-1982) . Bilgisayar Bilimleri Ders Notları . 177 . Berlin, Heidelberg, New York, Tokyo: Springer-Verlag. doi : 10.1007/BFb0048933 . ISBN'si 978-3-540-13378-0.
• Fitzgerald, JS ve Larsen, PG, Modelleme Sistemleri: Yazılım Mühendisliğinde Pratik Araçlar ve Teknikler . Cambridge University Press , 1998 ISBN  0-521-62348-0 (Japonca Baskı yayın. Iwanami Shoten 2003 ISBN  4-00-005609-3 ).
• Fitzgerald, JS , Larsen, PG, Mukherjee, P., Plat, N. and Verhoef,M., Validated Designs for Object-Oriented Systems . Springer Verlag 2005. ISBN  1-85233-881-4 . Destekleyen web sitesi [1] , örnekler ve ücretsiz araç desteği içerir.
• Jones, CB , VDM Kullanarak Sistematik Yazılım Geliştirme , Prentice Hall 1990. ISBN  0-13-880733-7 . Ayrıca çevrimiçi ve ücretsiz olarak da mevcuttur: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip
• Bjørner, D. ve Jones, CB , Resmi Spesifikasyon ve Yazılım Geliştirme Prentice Hall International, 1982. ISBN  0-13-880733-7
• J. Dawes, The VDM-SL Reference Guide , Pitman 1991. ISBN  0-273-03151-1
• Uluslararası Standardizasyon Örgütü , Bilgi teknolojisi - Programlama dilleri, ortamları ve sistem yazılımı arayüzleri - Viyana Geliştirme Yöntemi - Belirtim Dili - Bölüm 1: Temel dil Uluslararası Standart ISO/IEC 13817-1, Aralık 1996.
• Jones, CB , Yazılım Geliştirme: Titiz Bir Yaklaşım , Prentice Hall International, 1980. ISBN  0-13-821884-6
• Jones, CB ve Shaw, RC (ed.), Sistematik Yazılım Geliştirmede Vaka Çalışmaları , Prentice Hall International, 1990. ISBN  0-13-880733-7
• Bicarregui, JC, Fitzgerald, JS , Lindsay, PA, Moore, R. ve Ritchie, B., Proof in VDM: a Practitioner's Guide . Springer Verlag Bilgisayar ve Bilgi Teknolojisine Resmi Yaklaşımlar (FACIT), 1994. ISBN  3-540-19813-X .

Referanslar

Dış bağlantılar

• VDM ve VDM++ hakkında bilgiler (archive.org adresinde arşivlenmiş kopyası)
• Viyana Tanımlama Dili (VDL)