Кіріспе
Компьютерлік жүйелерді әзірлеудің ресми әдісі
Веналық даму әдісі (VDM) – компьютерлік жүйелерді әзірлеуге арналған ең көне және беделді ресми әдістердің бірі. 1970-ші жылдары Венадағы IBM зертханасында жүргізілген жұмыстардың нәтижесінде пайда болған VDM, ресми спецификация тілі – VDM Specification Language (VDM SL) негізінде құрылған әдістер мен құралдар жиынтығын қамтиды. Оның кеңейтілген нұсқасы VDM++ объектіге бағытталған және параллель жүйелерді модельдеуге мүмкіндік береді. VDM қолдауына модельдерді талдауға арналған коммерциялық және академиялық құралдар, соның ішінде модельдердің қасиеттерін тестілеу және растау, сондай-ақ VDM модельдерінен бағдарламалық кодты автоматты түрде жасау кіреді. VDM және оның құралдары өнеркәсіпте кеңінен қолданылып келеді, ал формализм саласындағы зерттеулер маңызды жүйелерді жобалау, компиляторлар жасау, параллель жүйелерді құру және компьютерлік ғылымның логикасын дамыту салаларына үлкен үлес қосты.
Философия
Компьютерлік жүйелерді VDM SL-де бағдарламалау тілдерінде мүмкін болатыннан гөрі жоғары деңгейде абстракциялап модельдеуге болады, бұл жүйе әзірлеудің бастапқы кезеңінде жобаларды талдауға және негізгі мүмкіндіктерді, соның ішінде кемшіліктерді анықтауға мүмкіндік береді. Расталган модельдерді жетілдіру процесі арқылы егжей-тегжейлі жүйе жобаларына түрлендіруге болады. Тілдің формальды семантикасы бар, ол модельдердің қасиеттерін жоғары дәрежеде сеніммен дәлелдеуге мүмкіндік береді. Сонымен қатар, модельдерді тестілеу арқылы талдауға және графикалық интерфейстер арқылы іске қосуға болатын орындалатын кіші жиынтығы бар, сондықтан модельдеу тілімен таныс емес сарапшылар да модельдерді бағалай алады.
Тарих
VDM SL-нің бастамасы Венадағы IBM зертханасында жатыр, онда тілдің алғашқы нұсқасы Вена анықтама тілі (VDL) деп аталды. VDL негізінен VDM-ге қарама-қарсы операциялық семантика сипаттамаларын беру үшін пайдаланылды, ал VDM – Meta IV денотациялық семантиканы ұсынды. 1972 жылдың соңында Вена тобы тіл анықтамасынан компиляторды жүйелі түрде әзірлеу мәселесіне қайта назар аударды. Қолданылған жалпы тәсіл «Веналық даму әдісі» деп аталды. Нақты қолданылған мета тіл («Meta IV») PL/1 тілінің негізгі бөліктерін анықтау үшін пайдаланылды (ECMA 74-де көрсетілгендей – қызықтысы, бұл «абстракт аудармашы ретінде жазылған ресми стандарттар құжаты»). BEKIČ 74 осыны айтады. Meta IV пен Schorre-дің META II тілі немесе оның мұрагері Tree Meta арасында ешқандай байланыс жоқ; бұл формалды проблемаларды сипаттауға жарамды емес, компилятор құрастыру жүйелері болды. Сондықтан Meta IV PL/I бағдарламалау тілінің «негізгі бөліктерін анықтау үшін» қолданылды. Meta IV және VDM SL арқылы ретроспективті немесе ішінара сипатталған басқа бағдарламалау тілдеріне BASIC, FORTRAN, APL, ALGOL 60, Ada және Pascal кіреді. Meta IV бірнеше нұсқаға эволюциялады, олар әдетте Дания, ағылшын және ирланд мектептері деп сипатталады. «Ағылшын мектебі» Клифф Джонстың VDM-нің тілдік анықтамаға және компиляторды жобалауға тікелей қатысы жоқ аспектілері бойынша жұмысына негізделген (Jones 1980, 1990). Ол базалық типтердің бай жиынтығынан құрылған дерек типтерін пайдалану арқылы тұрақты күйді модельдеуге баса назар аударады. Функционалдық мүмкіндіктер әдетте күйге жанама әсер ететін және көбінесе алғышарттар мен кейінгі шарттарды пайдалану арқылы жасырын түрде көрсетілген операциялар арқылы сипатталады. «Дания мектебі» (Bjørner және басқалар, 1982) конструктивті тәсілге, нақты операциялық сипаттамаларға көбірек мән береді. Дания мектебіндегі жұмыс алғашқы еуропалық Ada компиляторының жасалуына әкелді. 1996 жылы тіл үшін ISO стандарты жарияланды (ISO, 1996).
«Towards the end of 1972 the Vienna group again turned their attention to the problem of systematically developing a compiler from a language definition. The overall approach adopted has been termed the "Vienna Development Method" The meta language actually adopted ("Meta IV") is used to define major portions of PL/1 (as given in ECMA 74 – interestingly a "formal standards document written as an abstract interpreter") in BEKIČ 74.»
There is no connection between Meta IV, and Schorre's META II language, or its successor Tree Meta; these were compiler compiler systems rather than being suitable for formal problem descriptions. So Meta IV was "used to define major portions of" the PL/I programming language. Other programming languages retrospectively described, or partially described, using Meta IV and VDM SL include the BASIC programming language, FORTRAN, the APL programming language, ALGOL 60, the Ada programming language and the Pascal programming language. Meta IV evolved into several variants, generally described as the Danish, English and Irish Schools. The "English School" derived from work by Cliff Jones on the aspects of VDM not specifically related to language definition and compiler design (Jones 1980, 1990). It stresses modelling persistent state through the use of data types constructed from a rich collection of base types. Functionality is typically described through operations which may have side effects on the state and which are mostly specified implicitly using a precondition and postcondition. The "Danish School" (Bjørner et al. 1982) has tended to stress a constructive approach with explicit operational specification used to a greater extent. Work in the Danish school led to the first European validated Ada compiler. An ISO Standard for the language was released in 1996 (ISO, 1996).
VDM ерекшеліктері
VDM SL және VDM++ синтаксисі мен семантикасы VDMTools тілдік нұсқаулықтарында және қолжетімді мәтіндерде толыққанды сипатталған. ISO стандарты тілдің семантикасының формалды анықтамасын қамтиды. Осы мақаланың қалған бөлігінде ISO стандартымен белгіленген алмасу (ASCII) синтаксисі қолданылады. Кейбір мәтіндер математикалық синтаксисті ықшамдау етіп қолдануды ұсынады. VDM SL моделі – деректермен жұмыс істеу арқылы жүзеге асырылатын функционалдық мүмкіндіктермен сипатталған жүйе туралы ақпарат. Ол дерек түрлерінің анықтамаларынан және оларға қатысты орындалатын функциялар немесе амалдар тізбегінен тұрады.
Жинақтар
Жинақ түрлері мәндердің топтарын модельдейді. Жинақтар – мәндердің қайталануына жол бермейтін, шекті ретсіз жиынтықтар. Тізбелер – дубликаттарға рұқсат етілген, шекті реттелген жиынтықтар (тізімдер), ал сәйкестендірулер екі мән жиынтығы арасындағы шекті сәйкестіктерді көрсетеді.
Құрылымдық
VDM SL және VDM++ белгілерінің негізгі айырмашылығы – құрылымдау тәсілінде. VDM SL-де әдеттегі модульдік кеңейту қолданылады, ал VDM++ сыныптар мен мұрагерлікпен қатар дәстүрлі объектіге бағытталған құрылымдау механизмін ұсынады.
VDM-SL-дегі құрылымдау
VDM SL үшін ISO стандартында әртүрлі құрылымдау принциптерін қамтитын ақпараттық қосымша бар. Бұлардың барлығы модульдермен ақпаратты жасырудың дәстүрлі принциптерін ұстанады және оларды былай түсіндіруге болады:
Модульді атау: Әрбір модуль синтаксистік тұрғыдан модуль кілт сөзімен басталады, одан соң модульдің аты келеді. Модульдің соңында «end» кілт сөзі, содан кейін тағы да модульдің аты жазылады.
Импорттау: Басқа модульдерден экспортталған анықтамаларды импорттау мүмкін. Бұл импорт бөлімінде жүзеге асырылады, ол «imports» кілт сөзімен басталады, содан кейін әртүрлі модульдерден импорттар тізбегі келеді. Әрбір модульдік импорт «from» кілт сөзімен басталады, одан соң модульдің аты және модульдің қолтаңбасы жазылады. Модульдің қолтаңбасы, осы модульден экспортталған барлық анықтамаларды импорттауды білдіретін «all» кілт сөзі болуы мүмкін, немесе импорт қолтаңбаларының тізбегі болуы мүмкін. Импорттық қолтаңбалар типтерге, мәндерге, функцияларға және операцияларға арналған, және олардың әрқайсысы сәйкес кілт сөзбен басталады. Сонымен қатар, осы импорттық қолтаңбалар қол жеткізілгісі келетін құрылымдарды атайды. Қосымша, типтік ақпарат опциялы түрде болуы мүмкін, және соңында импорт кезінде құрылымдардың әрқайсысының атын өзгертуге болады. Типтер үшін, егер сіз нақты типтің ішкі құрылымына қол жеткізігіңіз келсе, «struct» кілт сөзін пайдалану қажет.
Экспорттау: Басқа модульдерге қол жеткізуді қалаған модульдің анықтамалары «exports» кілт сөзін және экспорт модульінің қолтаңбасын пайдаланып экспортталады. Экспорт модульінің қолтаңбасы тек «all» кілт сөзінен немесе экспорттық қолтаңбалар тізбегінен тұруы мүмкін. Мұндай экспорттық қолтаңбалар типтерге, мәндерге, функцияларға және операцияларға арналған, және олардың әрқайсысы сәйкес кілт сөзбен басталады. Егер сіз типтің ішкі құрылымын экспорттағыңыз келсе, «struct» кілт сөзін пайдалану керек.
Экзотикалық мүмкіндіктер: VDM SL-нің бұрынғы нұсқаларында құралдар параметрленген модульдерді және мұндай модульдердің инстанцияларын қолдаған. Алайда, бұл мүмкіндіктер 2000 жыл шамасында VDMTools-тан алынып тасталды, өйткені олар өнеркәсіптік қолданбаларда көбінесе қолданылмады және осы мүмкіндіктермен байланысты құралдарда көптеген қиындықтар туды.
Module naming: Each module is syntactically started with the keyword module followed by the name of the module. At the end of a module the keyword end is written followed again by the name of the module. Importing: It is possible to import definitions that has been exported from other modules. This is done in an imports section that is started off with the keyword imports and followed by a sequence of imports from different modules. Each of these module imports are started with the keyword from followed by the name of the module and a module signature. The module signature can either simply be the keyword all indicating the import of all definitions exported from that module, or it can be a sequence of import signatures. The import signatures are specific for types, values, functions and operations and each of these are started with the corresponding keyword. In addition these import signatures name the constructs that there is a desire to get access to. In addition optional type information can be present and finally it is possible to rename each of the constructs upon import. For types one needs also to use the keyword struct if one wish to get access to the internal structure of a particular type. Exporting: The definitions from a module that one wish other modules to have access to are exported using the keyword exports followed by an exports module signature. The exports module signature can either simply consist of the keyword all or as a sequence of export signatures. Such export signatures are specific for types, values, functions and operations and each of these are started with the corresponding keyword. In case one wish to export the internal structure of a type the keyword struct must be used. More exotic features: In earlier versions of the VDM SL, tools there was also support for parameterized modules and instantiations of such modules. However, these features were taken out of VDMTools around 2000 because they were hardly ever used in industrial applications and there was a substantial number of tool challenges with these features.
VDM++-да құрылымдау
VDM++ құрылымдау сыныптар және көптеген мұрагерлік арқылы жасалады. Негізгі түсініктер: Сынып: Әр сынып синтаксистік тұрғыдан "сынып" кілт сөзімен басталады, одан кейін сыныптың атауы келеді. Сыныптың соңында "end" кілт сөзі жазылады, содан кейін қайтадан сыныптың атауы жазылады. Мұрагерлік: Егер сынып басқа сыныптардан құрылымдарды мұрагерлік алса, сынып тақырыбында сынып атына "ішкі сынып" кілт сөздері ілеседі, одан кейін үтірмен бөлінген жоғары сыныптардың тізімі келеді. Кіру модификаторлары: VDM++-да ақпаратты жасыру көптеген объектіге бағытталған тілдердегідей кіру модификаторларын пайдалану арқылы жүзеге асырылады. VDM++ анықтамалары әдепкі бойынша жеке болып табылады, бірақ барлық анықтамалардың алдында кіруді өзгертуші кілт сөздердің бірін қолдануға болады: жеке, қоғамдық және қорғалған.
Class: Each class is syntactically started with the keyword class followed by the name of the class. At the end of a class the keyword end is written followed again by the name of the class. Inheritance: In case a class inherits constructs from other classes the class name in the class heading can be followed by the keywords is subclass of followed by a comma separated list of names of superclasses. Access modifiers: Information hiding in VDM++ is done in the same way as in most object oriented languages using access modifiers. In VDM++ definitions are per default private but in front of all definitions it is possible to use one of the access modifier keywords: private, public and protected.
Өнеркәсіптік тәжірибе
VDM әр түрлі қолдану салаларында кеңінен қолданылған. Осы қолданыстардың ең танымалдары: Ada және CHILL компиляторлары: Еуропалық алғашқы расталган Ada компиляторы Dansk Datamatik Center-де VDM қолданылып жасалды. Сол сияқты, CHILL және Modula 2 семантикасы олардың стандарттарында VDM арқылы сипатталған. ConForm: British Aerospace жүргізген тәжірибе, сенімді шлюздің дәстүрлі әзірлемесін VDM қолданып әзірлеумен салыстыру. Dust Expert: Ұлыбританиядағы Adelard компаниясы жүргізген жоба, өнеркәсіптік объектілердің орналасуындағы қауіпсіздіктің дұрыстығын анықтауға қатысты қауіпсіздікке байланысты қолданыс. VDMTools құралын әзірлеу: VDMTools құралдары жиынтығының көп бөлігі VDM қолданылып әзірленген. Бұл әзірлеме Даниядағы IFAD және Жапониядағы CSK-да жүзеге асырылды. TradeOne: Жапон қор биржасы үшін CSK systems әзірлеген TradeOne бэк-офис жүйесінің бірнеше маңызды компоненттері VDM қолданылып жасалды. VDM-де әзірленген компоненттердің әзірлеушілердің өнімділігі мен ақаулар тығыздығын дәстүрлі кодпен салыстыратын өлшемдер бар. FeliCa Networks ұялы телефондарға арналған интегралды схема үшін операциялық жүйенің әзірленгенін хабарлады.
Ada and CHILL compilers: The first European validated Ada compiler was developed by Dansk Datamatik Center using VDM. Likewise the semantics of CHILL and Modula 2 were described in their standards using VDM. ConForm: An experiment at British Aerospace comparing the conventional development of a trusted gateway with a development using VDM. Dust Expert: A project carried out by Adelard in the UK for a safety related application determining that the safety is appropriate in the layout of industrial plants. The development of VDMTools: Most components of the VDMTools tool suite are themselves developed using VDM. This development has been made at IFAD in Denmark and CSK in Japan. TradeOne: Certain key components of the TradeOne back office system developed by CSK systems for the Japanese stock exchange were developed using VDM. Comparative measurements exist for developer productivity and defect density of the VDM developed components versus the conventionally developed code. FeliCa Networks have reported the development of an operating system for an integrated circuit for cellular telephone applications.
Тазарту
VDM-ді қолдану өте абстрактілі модельден басталып, оны іске асыруға қарай дамытады. Әр қадамда деректерді нақтылау, содан кейін операцияларды жіктеу жүзеге асырылады. Деректерді нақтылау абстрактілі дерек түрлерін нақтырақ дерек құрылымдарына айналдырады, ал операцияларды жіктеу операциялар мен функциялардың (абстрактілі) жасырын сипаттамаларын таңдаған компьютер тілінде тікелей іске асырылатын алгоритмдерге дамытады.