Wiedeńska metoda rozwoju - Vienna Development Method

Metoda Development Wiedeń ( VDM ) jest jednym z najdłużej ustalonych metod formalnych dotyczących rozwoju systemów komputerowych. Wywodzi się z prac wykonanych w IBM Laboratory w Wiedniu w latach 70. XX wieku, a następnie rozrósł się do grupy technik i narzędzi opartych na formalnym języku specyfikacji — języku specyfikacji VDM (VDM-SL). Posiada rozszerzoną formę VDM++, która wspiera modelowanie systemów obiektowych i współbieżnych. Wsparcie dla VDM obejmuje komercyjne i akademickie narzędzia do analizy modeli, w tym wsparcie dla testowania i udowadniania właściwości modeli oraz generowania kodu programu ze zwalidowanych modeli VDM. Istnieje historia przemysłowego wykorzystania VDM i jego narzędzi, a rosnąca liczba badań nad formalizmem doprowadziła do znaczącego wkładu w inżynierię systemów krytycznych, kompilatorów , systemów współbieżnych oraz logiki dla informatyki .

Filozofia

Systemy obliczeniowe mogą być modelowane w VDM-SL na wyższym poziomie abstrakcji niż jest to osiągalne przy użyciu języków programowania, co pozwala na analizę projektów i identyfikację kluczowych cech, w tym defektów, na wczesnym etapie rozwoju systemu. Zweryfikowane modele można przekształcić w szczegółowe projekty systemu w procesie udoskonalania. Język ma semantykę formalną, umożliwiającą udowodnienie właściwości modeli na wysokim poziomie pewności. Zawiera również podzbiór wykonywalny, dzięki czemu modele mogą być analizowane przez testowanie i mogą być wykonywane za pomocą graficznych interfejsów użytkownika, dzięki czemu modele mogą być oceniane przez ekspertów, którzy niekoniecznie są zaznajomieni z samym językiem modelowania.

Historia

Początki VDM SL leżą w IBM laboratorium w Wiedeń , gdzie pierwsza wersja język zwany był V ienna D EFINICJA L anguage (VDL). VDL był zasadniczo używany do podawania operacyjnych opisów semantycznych w przeciwieństwie do VDM – Meta-IV, który zapewniał semantykę denotacyjną

„Pod koniec 1972 roku grupa wiedeńska ponownie zwróciła uwagę na problem systematycznego rozwijania kompilatora z definicji języka. Ogólne przyjęte podejście zostało nazwane „metodą rozwoju wiedeńskiego”. dokument norm napisany jako abstrakcyjny tłumacz") w BEKIČ 74.»

Nie ma żadnego związku między Meta-IV a językiem Meta-II Schorre'a lub jego następcą Tree Meta ; były to raczej systemy kompilator-kompilator niż nadające się do formalnych opisów problemów.

Tak więc Meta-IV była „używana do definiowania głównych części” języka programowania PL/I . Inne języki programowania opisane retrospektywnie lub częściowo opisane przy użyciu Meta-IV i VDM-SL obejmują język programowania BASIC , FORTRAN , język programowania APL , ALGOL 60, język programowania Ada i język programowania Pascal . Meta-IV przekształciła się w kilka wariantów, ogólnie określanych jako szkoły duńska, angielska i irlandzka.

„Szkoła języka angielskiego” wywodzi się z prac Cliffa Jonesa dotyczących aspektów VDM niezwiązanych konkretnie z definicją języka i projektowaniem kompilatorów (Jones 1980, 1990). Podkreśla modelowanie stanu trwałego poprzez wykorzystanie typów danych zbudowanych z bogatej kolekcji typów bazowych. Funkcjonalność jest zwykle opisana za pomocą operacji, które mogą mieć skutki uboczne na stanie i które są w większości określane niejawnie za pomocą warunku wstępnego i końcowego. „Szkoła Duńska” ( Bjørner et al. 1982) ma tendencję do podkreślania konstruktywnego podejścia, w którym w większym stopniu stosowana jest jawna specyfikacja operacyjna. Praca w duńskiej szkole doprowadziła do powstania pierwszego zatwierdzonego w Europie kompilatora Ady .

ISO Standard języka ukazał się w 1996 (ISO 1996).

Funkcje VDM

Składnia i semantyka VDM-SL i VDM++ są szczegółowo opisane w podręcznikach języka VDMTools oraz w dostępnych tekstach. Norma ISO zawiera formalną definicję semantyki języka. W pozostałej części tego artykułu używana jest składnia wymiany zdefiniowanej przez ISO (ASCII). Niektóre teksty wolą bardziej zwięzłą składnię matematyczną .

Model VDM-SL to opis systemu podany pod kątem funkcjonalności wykonywanej na danych. Składa się z szeregu definicji typów danych oraz funkcji lub operacji na nich wykonywanych.

Podstawowe typy: numeryczne, znakowe, tokenowe i cudzysłowowe

VDM-SL zawiera podstawowe typy modelujące liczby i znaki w następujący sposób:

Podstawowe typy
bool Typ danych logicznych fałsz PRAWDA
nat liczby naturalne (w tym zero) 0, 1, 2, 3, 4, 5...
nat1 liczby naturalne (bez zera) 1, 2, 3, 4, 5, ...
int liczby całkowite ..., -3, -2, -1, 0, 1, 2, 3, ...
rat liczby wymierne a/b , gdzie a i b są liczbami całkowitymi, b nie jest 0
real liczby rzeczywiste ...
char postacie A, B, C, ...
token tokeny bezstrukturalne ...
<A> typ cytatu zawierający wartość <A> ...

Typy danych są zdefiniowane w celu reprezentowania głównych danych modelowanego systemu. Każda definicja typu wprowadza nową nazwę typu i przedstawia reprezentację pod względem typów podstawowych lub pod względem typów już wprowadzonych. Na przykład identyfikatory użytkownika modelujące typ dla systemu zarządzania logowaniem mogą być zdefiniowane w następujący sposób: 

types
UserId = nat

Aby manipulować wartościami należącymi do typów danych, operatory są definiowane na wartościach. W ten sposób zapewnione jest dodawanie, odejmowanie itp. liczb naturalnych, podobnie jak operatory logiczne, takie jak równość i nierówność. Język nie ustala maksymalnej lub minimalnej reprezentowanej liczby ani precyzji dla liczb rzeczywistych. Takie ograniczenia są definiowane tam, gdzie są wymagane w każdym modelu, za pomocą niezmienników typu danych — wyrażeń logicznych oznaczających warunki, które muszą być przestrzegane przez wszystkie elementy zdefiniowanego typu. Na przykład wymaganie, aby identyfikatory użytkowników nie mogły być większe niż 9999, można wyrazić w następujący sposób (gdzie <=jest operatorem logicznym „mniejszy lub równy” na liczbach naturalnych): 

UserId = nat
inv uid == uid <= 9999

Ponieważ niezmienniki mogą być dowolnie złożonymi wyrażeniami logicznymi, a członkostwo w zdefiniowanym typie jest ograniczone tylko do wartości spełniających niezmiennik, poprawność typu w VDM-SL nie jest automatycznie rozstrzygana we wszystkich sytuacjach.

Inne podstawowe typy to char dla znaków. W niektórych przypadkach reprezentacja typu nie ma znaczenia dla celu modelu i tylko zwiększa złożoność. W takich przypadkach członkowie typu mogą być reprezentowani jako tokeny bez struktury. Wartości typów tokenów można porównywać tylko pod kątem równości – nie są na nich zdefiniowane żadne inne operatory. Tam, gdzie wymagane są konkretne nazwane wartości, są one wprowadzane jako typy cytatów. Każdy typ cudzysłowu składa się z jednej nazwanej wartości o tej samej nazwie co sam typ. Wartości typów cudzysłowów (znanych jako literały cudzysłowów) mogą być porównywane tylko pod kątem równości.

Na przykład w modelowaniu sterownika sygnalizacji świetlnej może być wygodne zdefiniowanie wartości reprezentujących kolory sygnalizacji świetlnej jako typy cytatów: 

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

Konstruktory typów: typy uniowe, produktowe i złożone

Same podstawowe typy mają ograniczoną wartość. Nowe, bardziej ustrukturyzowane typy danych są budowane przy użyciu konstruktorów typów.

Konstruktorzy typu podstawowego
T1 | T2 | ... | Tn Unia typów T1,...,Tn
T1*T2*...*Tn Iloczyn kartezjański typów T1,...,Tn
T :: f1:T1 ... fn:Tn Typ kompozytowy (rekordowy)

Najbardziej podstawowy konstruktor typu tworzy unię dwóch wstępnie zdefiniowanych typów. Typ (A|B)zawiera wszystkie elementy typu A i wszystkie typu B. W przykładzie sterownika sygnalizacji świetlnej typ modelujący kolor sygnalizacji świetlnej można zdefiniować w następujący sposób: 

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

Typy wyliczone w VDM-SL są zdefiniowane jak pokazano powyżej jako związki w typach cytatów.

W VDM-SL można również zdefiniować kartezjańskie typy produktów. Typ (A1*…*An)to typ złożony ze wszystkich krotek wartości, z których pierwszy element pochodzi z typu, A1a drugi z typu A2i tak dalej. Typ złożony lub rekord to iloczyn kartezjański z etykietami dla pól. Typ 

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

jest iloczynem kartezjańskim z polami oznaczonymi f1,…,fn. Element typu Tmoże być złożony z części składowych przez konstruktora napisane mk_T. I odwrotnie, biorąc pod uwagę element typu T, nazwy pól mogą służyć do wybierania nazwanego komponentu. Na przykład typ 

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

modeluje prosty typ daty. Wartość mk_Date(1,4,2001)odpowiada 1 kwietnia 2001 r. W przypadku daty dwyrażenie d.monthjest liczbą naturalną reprezentującą miesiąc. W razie potrzeby do niezmiennika można włączyć ograniczenia dotyczące dni w miesiącu i lat przestępnych. Łącząc te: 

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

Kolekcje

Typy kolekcji modelują grupy wartości. Zestawy to skończone nieuporządkowane kolekcje, w których duplikowanie między wartościami jest pomijane. Sekwencje to skończone uporządkowane kolekcje (listy), w których może wystąpić duplikacja, a mapowania reprezentują skończone zależności między dwoma zestawami wartości.

Zestawy

Konstruktor typu set (zapisany set of Tgdzie Tjest typem predefiniowanym) konstruuje typ złożony ze wszystkich skończonych zestawów wartości wylosowanych z typu T. Na przykład definicja typu 

UGroup = set of UserId

definiuje typ UGroupzłożony ze wszystkich skończonych zbiorów UserIdwartości. Różne operatory są zdefiniowane na zbiorach do konstruowania ich sumy, przecięcia, określania poprawnych i nieścisłych relacji podzbiorów itp.

Główne operatory na zbiorach (s, s1, s2 są zbiorami)
{a, b, c} Wyliczenie zbioru: zbiór elementów a, borazc
{x | x:T & P(x)} Zbiór ze zrozumieniem: zbiór xod typu Ttaki, żeP(x)
{i, ..., j} Zbiór liczb całkowitych z zakresu idoj
e in set s e jest elementem zestawu s
e not in set s e nie jest elementem zestawu s
s1 union s2 Unia zbiorów s1is2
s1 inter s2 Przecięcie zbiorów s1is2
s1 \ s2 Ustaw różnicę zestawów s1is2
dunion s Rozproszony związek zbioru zestawów s
s1 psubset s2 s1 jest (właściwym) podzbiorem s2
s1 subset s2 s1 jest (słabym) podzbiorem s2
card s Kardynalność zbioru s

Sekwencje

Konstruktor typu skończonej sekwencji (zapisany seq of Tgdzie Tjest predefiniowanym typem) konstruuje typ złożony ze wszystkich skończonych list wartości wylosowanych z typu T. Na przykład definicja typu 

String = seq of char

Definiuje typ Stringzłożony ze wszystkich skończonych ciągów znaków. Różne operatory są zdefiniowane na sekwencjach do konstruowania konkatenacji, selekcji elementów i podciągów itp. Wiele z tych operatorów jest częściowych w tym sensie, że nie są zdefiniowane dla pewnych zastosowań. Na przykład wybranie piątego elementu sekwencji, która zawiera tylko trzy elementy, jest niezdefiniowane.

Kolejność i powtarzalność elementów w sekwencji jest istotna, więc [a, b]nie jest równa [b, a]i [a]nie jest równa [a, a].

Główne operatory na ciągach (s, s1,s2 są ciągami)
[a, b, c] Wyliczanie sekwencji: sekwencja elementów a, bic
[f(x) | x:T & P(x)] Zrozumienie sekwencji: sekwencja wyrażeń f(x)dla każdego xtypu (numerycznego) Ttaka, że P(x)zawiera
( xwartości brane w kolejności numerycznej)
hd s Głowa (pierwszy element) s
tl s Ogon (pozostała sekwencja po usunięciu głowy) z s
len s Długość s
elems s Zbiór elementów s
s(i) iTh elements
inds s zbiór indeksów dla ciągu s
s1^s2 ciąg utworzony przez łączenie ciągów s1is2

Mapy

Skończone mapowanie to zgodność między dwoma zestawami, domeną i zakresem, z elementami indeksującymi domenę z zakresu. Jest więc podobny do funkcji skończonej. Konstruktor typu mapowania w VDM-SL (zapisany map T1 to T2gdzie T1i T2są typami predefiniowanymi) konstruuje typ złożony ze wszystkich skończonych mapowań z zestawów T1wartości na zestawy T2wartości. Na przykład definicja typu 

Birthdays = map String to Date

Definiuje typ, Birthdaysktóry mapuje ciągi znaków na Date. Ponownie, operatory są definiowane w mapowaniach do indeksowania w mapowaniu, mapowania scalającego, nadpisywania wyodrębniania podmapowań.

Główni operatorzy na mapowaniach
{a |-> r, b |-> s} Wyliczenie mapowania: amaps to r, bmaps tos
{x |-> f(x) | x:T & P(x)} Zrozumienie mapowania: xmapuje do f(x)for all xdla typu Ttakiego, żeP(x)
dom m Domena m
rng m Zakres m
m(x) m stosowane do x
m1 munion m2 Unia mapowań m1i m2( m1, m2muszą być spójne tam, gdzie się nakładają)
m1 ++ m2 m1 nadpisany przez m2

Strukturyzacja

Główną różnicą między notacjami VDM-SL i VDM++ jest sposób, w jaki zajmuje się strukturacją. W VDM-SL istnieje konwencjonalne rozszerzenie modułowe, podczas gdy VDM++ ma tradycyjny mechanizm strukturyzacji obiektowej z klasami i dziedziczeniem.

Strukturyzacja w VDM-SL

W normie ISO dla VDM-SL znajduje się załącznik informacyjny, który zawiera różne zasady strukturyzowania. Wszystkie one są zgodne z tradycyjnymi zasadami ukrywania informacji za pomocą modułów i można je wyjaśnić jako:

  • Nazewnictwo modułów : każdy moduł jest uruchamiany składniowo słowem kluczowym, modulepo którym następuje nazwa modułu. Na końcu modułu endzapisywane jest słowo kluczowe, a po nim ponownie nazwa modułu.
  • Importowanie : możliwe jest importowanie definicji, które zostały wyeksportowane z innych modułów. Odbywa się to w sekcji importów, która zaczyna się od słowa kluczowego, importspo którym następuje sekwencja importów z różnych modułów. Każdy z tych importów modułów jest rozpoczynany od słowa kluczowego, frompo którym następuje nazwa modułu i sygnatura modułu. Podpis moduł może być albo po prostu słowo kluczowe allwskazaniem import wszystkich definicjach eksportowanych z tego modułu, lub może to być sekwencja podpisów importowych. Sygnatury importu są specyficzne dla typów, wartości, funkcji i operacji, a każda z nich rozpoczyna się od odpowiedniego słowa kluczowego. Ponadto te sygnatury importu określają konstrukcje, do których istnieje chęć uzyskania dostępu. Dodatkowo może być obecna opcjonalna informacja o typie i wreszcie możliwa jest zmiana nazwy każdego z konstruktów podczas importu. W przypadku typów należy również użyć słowa kluczowego, structjeśli chcemy uzyskać dostęp do wewnętrznej struktury danego typu.
  • Eksportowanie : Definicje z modułu, do którego inne moduły mają mieć dostęp, są eksportowane przy użyciu słowa kluczowego, exportspo którym następuje podpis modułu eksportu. Podpis moduł eksportu może albo po prostu składa się z słów kluczowych alllub jako sekwencję podpisów eksportowych. Takie sygnatury eksportu są specyficzne dla typów, wartości, funkcji i operacji, a każdy z nich rozpoczyna się od odpowiedniego słowa kluczowego. W przypadku chęci wyeksportowania wewnętrznej struktury typu structnależy użyć słowa kluczowego .
  • Bardziej egzotyczne funkcje : We wcześniejszych wersjach narzędzi VDM-SL istniała również obsługa modułów parametryzowanych i ich instancji. Jednak te funkcje zostały usunięte z VDMTools około 2000 r., ponieważ prawie nigdy nie były używane w zastosowaniach przemysłowych, a z tymi funkcjami istniała znaczna liczba wyzwań związanych z narzędziami.

Strukturyzacja w VDM++

W VDM++ strukturyzacja odbywa się za pomocą klas i wielokrotnego dziedziczenia. Kluczowe pojęcia to:

  • Klasa : Każda klasa jest składniowo rozpoczynana od słowa kluczowego, classpo którym następuje nazwa klasy. Na końcu klasy endzapisywane jest słowo kluczowe, a po nim ponownie nazwa klasy.
  • Dziedziczenie : W przypadku, gdy klasa dziedziczy konstrukcje z innych klas, po nazwie klasy w nagłówku klasy mogą występować słowa kluczowe, is subclass ofpo których następuje oddzielona przecinkami lista nazw nadklas.
  • Modyfikatory dostępu : ukrywanie informacji w VDM++ odbywa się w taki sam sposób, jak w większości języków obiektowych przy użyciu modyfikatorów dostępu. W VDM++ definicje są domyślnie prywatne, ale przed wszystkimi definicjami można użyć jednego ze słów kluczowych modyfikujących dostęp: private, publici protected.

Funkcjonalność modelowania

Modelowanie funkcjonalne

W VDM-SL funkcje są definiowane na podstawie typów danych zdefiniowanych w modelu. Obsługa abstrakcji wymaga, aby możliwe było scharakteryzowanie wyniku, który funkcja powinna obliczyć, bez konieczności określania, w jaki sposób powinna być obliczana. Głównym mechanizmem służącym do tego jest niejawna definicja funkcji, w której zamiast formuły obliczającej wynik, predykat logiczny nad zmiennymi wejściowymi i wynikowymi, zwany warunkiem końcowym , podaje właściwości wyniku. Na przykład funkcję SQRTobliczania pierwiastka kwadratowego z liczby naturalnej można zdefiniować w następujący sposób: 

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

W tym przypadku warunek końcowy nie definiuje metody obliczania wyniku, rale określa, jakie właściwości można założyć, że go posiadają. Zauważ, że definiuje to funkcję, która zwraca poprawny pierwiastek kwadratowy; nie ma wymogu, aby był to pierwiastek dodatni lub ujemny. Powyższa specyfikacja zostałaby spełniona na przykład przez funkcję, która zwróciła ujemny pierwiastek z 4, ale dodatni pierwiastek wszystkich innych prawidłowych danych wejściowych. Należy zauważyć, że funkcje w VDM-SL muszą być deterministyczne, aby funkcja spełniająca powyższą przykładową specyfikację zawsze zwracała ten sam wynik dla tych samych danych wejściowych.

Bardziej ograniczoną specyfikację funkcji uzyskuje się poprzez wzmocnienie warunku końcowego. Na przykład poniższa definicja ogranicza funkcję do zwracania dodatniego pierwiastka. 

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

Wszystkie specyfikacje funkcji mogą być ograniczone przez warunki wstępne, które są logicznymi predykatami tylko nad zmiennymi wejściowymi i które opisują ograniczenia, które zakłada się, że są spełnione podczas wykonywania funkcji. Na przykład funkcja obliczania pierwiastka kwadratowego, która działa tylko na dodatnich liczbach rzeczywistych, może być określona w następujący sposób: 

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

Warunek wstępny i warunek końcowy tworzą razem umowę, którą musi spełnić każdy program, który twierdzi, że realizuje funkcję. Warunek wstępny rejestruje założenia, zgodnie z którymi funkcja gwarantuje zwrócenie wyniku spełniającego warunek końcowy. Jeśli funkcja jest wywoływana na danych wejściowych, które nie spełniają jej warunku wstępnego, wynik jest niezdefiniowany (w rzeczywistości zakończenie nie jest nawet gwarantowane).

VDM-SL obsługuje również definicję funkcji wykonywalnych na sposób funkcjonalnego języka programowania. W jawnej definicji funkcji wynik jest definiowany za pomocą wyrażenia na danych wejściowych. Na przykład funkcja tworząca listę kwadratów listy liczb może być zdefiniowana w następujący sposób: 

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

Ta rekurencyjna definicja składa się z sygnatury funkcji podającej typy danych wejściowych i wyników oraz treści funkcji. Niejawna definicja tej samej funkcji może mieć następującą postać: 

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

Wyraźna definicja jest w prostym sensie implementacją niejawnie określonej funkcji. Poprawność jawnej definicji funkcji w odniesieniu do niejawnej specyfikacji można zdefiniować w następujący sposób.

Biorąc pod uwagę niejawną specyfikację: 

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

oraz funkcja jawna: 

f:T_p -> T_r

mówimy, że spełnia specyfikację iff : 

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

Tak więc " fjest poprawną implementacją" należy interpretować jako " fspełnia specyfikację".

Modelowanie oparte na stanach

W VDM-SL funkcje nie mają skutków ubocznych, takich jak zmiana stanu trwałej zmiennej globalnej. Jest to przydatna umiejętność w wielu językach programowania, więc istnieje podobna koncepcja; zamiast funkcji do zmiany zmiennych stanu używane są operacje (znane również jako globals ).

Na przykład, jeśli mamy stan składający się z jednej zmiennej someStateRegister : nat, możemy to zdefiniować w VDM-SL jako: 

state Register of
  someStateRegister : nat
end

W VDM++ byłoby to zamiast tego zdefiniowane jako: 

instance variables
  someStateRegister : nat

Operacja ładowania wartości do tej zmiennej może być określona jako: 

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

Pozory punkt ( ext) określa, które elementy stanu mogą być dostępne przez działanie; rdwskazujący dostęp tylko do wrodczytu i będący dostępem do odczytu/zapisu.

Czasami ważne jest, aby odwołać się do wartości stanu przed jego modyfikacją; na przykład operacja dodania wartości do zmiennej może być określona jako: 

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

Gdzie ~symbol na zmiennej stanu w warunku końcowym wskazuje wartość zmiennej stanu przed wykonaniem operacji.

Przykłady

Maks funkcja

To jest przykład niejawnej definicji funkcji. Funkcja zwraca największy element ze zbioru dodatnich liczb całkowitych: 

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

Warunek końcowy charakteryzuje wynik, a nie definiuje algorytm jego uzyskania. Warunek wstępny jest potrzebny, ponieważ żadna funkcja nie może zwrócić r w zbiorze s, gdy zbiór jest pusty.

Mnożenie liczb naturalnych

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

Stosowanie obowiązku dowodu forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))do wyraźnej definicji 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)

Wówczas obowiązek dowodu staje się: 

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

Można to wykazać prawidłowo przez:

  1. Udowodnienie, że rekurencja się kończy (to z kolei wymaga udowodnienia, że ​​liczby zmniejszają się z każdym krokiem)
  2. Indukcja matematyczna

Abstrakcyjny typ danych kolejki

Jest to klasyczny przykład ilustrujący zastosowanie niejawnej specyfikacji operacji w modelu stanowym znanej struktury danych. Kolejka modelowana jest jako sekwencja złożona z elementów typu Qelt. Reprezentacja jest Qeltnieistotna i dlatego jest definiowana jako typ tokenu. 

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)

Przykład systemu bankowego

Jako bardzo prosty przykład modelu VDM-SL rozważ system do utrzymywania szczegółów konta bankowego klienta. Klienci są modelowani według numerów klientów ( CustNum ), konta są modelowane według numerów kont ( AccNum ). Przedstawienia numerów klientów są uważane za nieistotne i dlatego są modelowane przez typ tokena. Salda i kredyty w rachunku bieżącym są modelowane według typów liczbowych. 

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)

Z operacjami: NEWC przydziela nowy numer klienta: 

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 przydziela nowy numer rachunku i ustawia saldo na zero: 

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 zwraca wszystkie salda wszystkich rachunków klienta w postaci mapy numeru rachunku do salda: 

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}

Wsparcie narzędziowe

Wiele różnych narzędzi obsługuje VDM:

  • VDMTools to wiodące komercyjne narzędzia dla VDM i VDM++, będące własnością, sprzedawane, utrzymywane i rozwijane przez CSK Systems , oparte na wcześniejszych wersjach opracowanych przez duńską firmę IFAD. Dostępne są podręczniki i praktyczny samouczek . Wszystkie licencje są dostępne bezpłatnie dla pełnej wersji narzędzia. Pełna wersja zawiera automatyczne generowanie kodu dla Javy i C++, bibliotekę dołączaną dynamicznie oraz obsługę CORBA.
  • Overture to oparta na społeczności inicjatywa open source, której celem jest zapewnienie bezpłatnie dostępnego wsparcia narzędziowego dla VDM++ na platformie Eclipse. Jego celem jest opracowanie ram dla interoperacyjnych narzędzi, które będą przydatne do zastosowań przemysłowych, badań i edukacji.
  • vdm-mode to zbiór pakietów Emacsa do pisania specyfikacji VDM przy użyciu VDM-SL, VDM++ i VDM-RT. Obsługuje podświetlanie i edycję składni, sprawdzanie składni w locie, uzupełnianie szablonów i obsługę interpretera.
  • SpecBox : firmy Adelard zapewnia sprawdzanie składni, proste sprawdzanie semantyczne oraz generowanie pliku LaTeX umożliwiającego drukowanie specyfikacji w notacji matematycznej. To narzędzie jest dostępne bezpłatnie, ale nie jest dalej utrzymywane.
  • Makra LaTeX i LaTeX2e są dostępne do obsługi prezentacji modeli VDM w składni matematycznej języka standardowego ISO. Zostały opracowane i są utrzymywane przez National Physical Laboratory w Wielkiej Brytanii. Dokumentacja i makra są dostępne online.

Doświadczenie przemysłowe

VDM jest szeroko stosowany w różnych dziedzinach aplikacji. Najbardziej znane z tych aplikacji to:

  • Kompilatory Ada i CHILL : Pierwszy kompilator Ada zwalidowany w Europie został opracowany przez Dansk Datamatik Center przy użyciu VDM. Podobnie semantyka CHILL i Modula-2 została opisana w ich standardach przy użyciu VDM.
  • ConForm: Eksperyment w British Aerospace porównujący konwencjonalny rozwój zaufanej bramy z rozwojem przy użyciu VDM.
  • Dust-Expert: Projekt realizowany przez Adelard w Wielkiej Brytanii dla aplikacji związanej z bezpieczeństwem, określający, czy bezpieczeństwo jest odpowiednie w rozplanowaniu zakładów przemysłowych.
  • Rozwój VDMTools: Większość komponentów pakietu narzędzi VDMTools jest sama opracowywana przy użyciu VDM. Ten rozwój został dokonany w IFAD w Danii i CSK w Japonii .
  • TradeOne: Niektóre kluczowe elementy systemu back-office TradeOne opracowanego przez systemy CSK dla japońskiej giełdy zostały opracowane przy użyciu VDM. Istnieją pomiary porównawcze wydajności programistów i gęstości defektów komponentów opracowanych w VDM w porównaniu z konwencjonalnie opracowanym kodem.
  • Firma FeliCa Networks poinformowała o opracowaniu systemu operacyjnego dla układu scalonego do zastosowań telefonii komórkowej .

Udoskonalenie

Korzystanie z VDM zaczyna się od bardzo abstrakcyjnego modelu i rozwija go w implementację. Każdy krok obejmuje rewizję danych , a następnie dekompozycję operacji .

Reifikacja danych rozwija abstrakcyjne typy danych w bardziej konkretne struktury danych , podczas gdy dekompozycja operacji rozwija (abstrakcyjną) niejawną specyfikację operacji i funkcji w algorytmy, które mogą być bezpośrednio zaimplementowane w wybranym języku komputerowym.

Reifikacja danych

Reifikacja danych (udokładnianie krokowe) polega na znalezieniu bardziej konkretnej reprezentacji abstrakcyjnych typów danych używanych w specyfikacji. Może być kilka kroków przed osiągnięciem implementacji. Każdy krok reifikacji abstrakcyjnej reprezentacji danych ABS_REPwiąże się z zaproponowaniem nowej reprezentacji NEW_REP. Aby pokazać, że nowa reprezentacja jest dokładna, zdefiniowana jest funkcja wyszukiwania, która odnosi się NEW_REPdo ABS_REP, tj retr : NEW_REP -> ABS_REP. . Poprawność reifikacji danych zależy od wykazania adekwatności , tj 

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

Ponieważ reprezentacja danych uległa zmianie, konieczne jest zaktualizowanie operacji i funkcji tak, aby działały na NEW_REP. Należy pokazać nowe operacje i funkcje, aby zachować wszelkie niezmienniki typu danych w nowej reprezentacji. Aby udowodnić, że nowe operacje i funkcje modelują te, które znalazły się w pierwotnej specyfikacji, konieczne jest spełnienie dwóch obowiązków dowodowych:

  • Reguła domeny:
forall r: NEW_REP & pre-OPA(retr(r)) => pre-OPR(r)
  • Zasada modelowania:
forall ~r,r:NEW_REP & pre-OPA(retr(~r)) and post-OPR(~r,r) => post-OPA(retr(~r,), retr(r))

Przykładowa reifikacja danych

W firmowym systemie bezpieczeństwa pracownicy otrzymują identyfikatory; są one podawane do czytników kart przy wejściu i wyjściu z fabryki. Wymagane operacje:

  • INIT() inicjuje system, zakłada, że ​​fabryka jest pusta
  • ENTER(p : Person)rejestruje, że pracownik wchodzi do fabryki; dane pracowników są odczytywane z dowodu osobistego)
  • EXIT(p : Person) odnotowuje, że pracownik opuszcza fabrykę
  • IS-PRESENT(p : Person) r : bool sprawdza, czy określony pracownik jest w fabryce, czy nie

Formalnie byłoby to: 

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~

Ponieważ większość języków programowania ma koncepcję porównywalną do zestawu (często w postaci tablicy), pierwszym krokiem od specyfikacji jest przedstawienie danych w postaci sekwencji. Te sekwencje nie mogą umożliwiać powtórzeń, ponieważ nie chcemy, aby ten sam pracownik pojawiał się dwa razy, więc musimy dodać niezmiennik do nowego typu danych. W tym przypadku kolejność nie jest ważna, więc [a,b]jest taka sama jak [b,a].

Vienna Development Method jest cenna dla systemów opartych na modelach. Nie jest właściwe, jeśli system jest oparty na czasie. W takich przypadkach bardziej przydatny jest rachunek systemów komunikacji (CCS).

Zobacz też

Dalsza lektura

  • Bjørner, Dines; Cliff B. Jones (1978). Wiedeńska metoda rozwoju: metajęzyk, notatki do wykładów z informatyki 61 . Berlin, Heidelberg, Nowy Jork: Springer. Numer ISBN 978-0-387-08766-5.
  • O'Regan, Gerard (2006). Matematyczne podejścia do jakości oprogramowania . Londyn: Springer. Numer ISBN 978-1-84628-242-3.
  • Cliff B. Jones, wyd. (1984). Języki programowania i ich definicja — H. Bekič (1936-1982) . Notatki z wykładów z informatyki . 177 . Berlin, Heidelberg, Nowy Jork, Tokio: Springer-Verlag. doi : 10.1007/BFb0048933 . Numer ISBN 978-3-540-13378-0.
  • Fitzgerald, JS i Larsen, PG, Systemy modelowania: praktyczne narzędzia i techniki w inżynierii oprogramowania . Cambridge University Press , 1998 ISBN  0-521-62348-0 (wydanie japońskie, Iwanami Shoten 2003 ISBN  4-00-005609-3 ).
  • Fitzgerald, JS , Larsen, PG, Mukherjee, P., Plat, N. i Verhoef, M., Zatwierdzone projekty systemów zorientowanych obiektowo . Springer Verlag 2005. ISBN  1-85233-881-4 . Pomocnicza strona internetowa [1] zawiera przykłady i bezpłatne wsparcie narzędzi.
  • Jones, CB , Systematyczne tworzenie oprogramowania przy użyciu VDM , Prentice Hall 1990. ISBN  0-13-880733-7 . Dostępne również online i bezpłatnie: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip
  • Bjørner, D. i Jones, CB , Specyfikacja formalna i rozwój oprogramowania Prentice Hall International, 1982. ISBN  0-13-880733-7
  • J. Dawes, The VDM-SL Reference Guide , Pitman 1991. ISBN  0-273-03151-1
  • Międzynarodowa Organizacja Normalizacyjna , Technologia informacyjna – Języki programowania, ich środowiska i interfejsy oprogramowania systemowego – Wiedeńska metoda rozwoju – Język specyfikacji – Część 1: Język podstawowy Norma międzynarodowa ISO/IEC 13817-1, grudzień 1996.
  • Jones, CB , Rozwój oprogramowania: rygorystyczne podejście , Prentice Hall International, 1980. ISBN  0-13-821884-6
  • Jones, CB and Shaw, RC (red.), Studia przypadków w systematycznym rozwoju oprogramowania , Prentice Hall International, 1990. ISBN  0-13-880733-7
  • Bicarregui, JC, Fitzgerald, JS , Lindsay, PA, Moore, R. i Ritchie, B., Proof in VDM: a Practitioner's Guide . Springer Verlag Formalne podejścia do informatyki i technologii informacyjnej (FACIT), 1994. ISBN  3-540-19813-X .

Bibliografia

Zewnętrzne linki