Введение
Формальный метод разработки компьютерных систем
Венский метод разработки (VDM) – один из наиболее устоявшихся формальных методов разработки компьютерных систем. Зародившись в 1970-х годах в лаборатории IBM в Вене, он развился в совокупность техник и инструментов, основанных на формальном языке спецификаций – языке спецификаций VDM (VDM SL). Существует расширенная версия VDM++, поддерживающая моделирование объектно-ориентированных и параллельных систем. Поддержка VDM включает в себя коммерческие и академические инструменты для анализа моделей, в том числе для тестирования и доказательства свойств моделей, а также для генерации программного кода из валидированных моделей VDM. VDM и его инструменты имеют историю промышленного применения, а растущий объем исследований в области этого формализма привел к значительным достижениям в разработке критически важных систем, компиляторов, параллельных систем и логики для информатики.
Философия
Вычислительные системы могут быть смоделированы в VDM SL на более высоком уровне абстракции, чем это возможно при использовании языков программирования, что позволяет анализировать проекты и выявлять ключевые характеристики, включая дефекты, на ранней стадии разработки системы. Валидированные модели могут быть преобразованы в детальные проекты систем посредством процесса уточнения. Язык обладает формальной семантикой, что позволяет доказывать свойства моделей с высокой степенью достоверности. Он также имеет исполняемое подмножество, благодаря которому модели можно анализировать путем тестирования и выполнять через графические пользовательские интерфейсы, что позволяет экспертам, не обязательно знакомым с самим языком моделирования, оценивать модели.
История
Истоки VDM SL лежат в лаборатории IBM в Вене, где первая версия языка была названа Венским языком определения (VDL). VDL использовался главным образом для описания операционной семантики, в отличие от VDM – Meta IV, который предоставлял денотационную семантику.
К концу 1972 года Венская группа вновь обратила внимание на проблему систематической разработки компилятора на основе определения языка. Общий принятый подход получил название «Венский метод разработки». Фактически принятый мета-язык («Meta IV») использовался для определения основных частей PL/1 (как указано в ECMA 74 – примечательно, что это «формальный стандартный документ, написанный в виде абстрактного интерпретатора») в BEKIČ 74. Связи между Meta IV и языком 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 et al. 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 содержит формальное определение семантики языка. В остальной части данной статьи используется синтаксис обмена данными ASCII, определенный стандартом ISO. Некоторые публикации предпочитают более лаконичный математический синтаксис. Модель VDM SL – это описание системы, представленное с точки зрения функциональности, выполняемой над данными. Она состоит из ряда определений типов данных и функций или операций, применяемых к ним.
Коллекции
Типы коллекций моделируют группы значений. Множества — это конечные неупорядоченные коллекции, в которых исключаются повторяющиеся значения. Последовательности — это конечные упорядоченные коллекции (списки), в которых могут быть повторяющиеся значения, а отображения представляют собой конечные соответствия между двумя множествами значений.
Структурирование
Основное различие между нотациями VDM SL и VDM++ заключается в способе организации структуры. В VDM SL используется традиционное модульное расширение, а в VDM++ – традиционный объектно-ориентированный механизм структурирования с классами и наследованием.
Структурирование в VDM-SL
В стандарте ISO для VDM SL имеется информационное приложение, содержащее различные принципы структурирования. Все они основаны на традиционных принципах сокрытия информации посредством модулей и могут быть описаны следующим образом:
Именование модуля: Каждый модуль синтаксически начинается с ключевого слова `module`, за которым следует имя модуля. В конце модуля записывается ключевое слово `end`, за которым снова следует имя модуля.
Импорт: Возможно импортировать определения, экспортированные из других модулей. Это осуществляется в секции импорта, начинающейся с ключевого слова `imports` и далее следующей последовательностью импортов из различных модулей. Каждый из этих импортов модуля начинается с ключевого слова `from`, за которым следует имя модуля и сигнатура модуля. Сигнатура модуля может быть либо просто ключевым словом `all`, указывающим на импорт всех определений, экспортированных из этого модуля, либо последовательностью сигнатур импорта. Сигнатуры импорта специфичны для типов, значений, функций и операций, и каждая из них начинается с соответствующего ключевого слова. Кроме того, эти сигнатуры импорта указывают на конструкции, к которым требуется получить доступ. Дополнительно может присутствовать необязательная информация о типе, и, наконец, возможно переименование каждой из конструкций при импорте. Для типов также необходимо использовать ключевое слово `struct`, если требуется получить доступ к внутренней структуре конкретного типа.
Экспорт: Определения из модуля, к которым необходимо предоставить доступ другим модулям, экспортируются с использованием ключевого слова `exports`, за которым следует сигнатура модуля экспорта. Сигнатура модуля экспорта может состоять либо просто из ключевого слова `all`, либо из последовательности сигнатур экспорта. Такие сигнатуры экспорта специфичны для типов, значений, функций и операций, и каждая из них начинается с соответствующего ключевого слова. В случае, если требуется экспортировать внутреннюю структуру типа, необходимо использовать ключевое слово `struct`.
Более экзотические возможности: В ранних версиях VDM SL инструменты также поддерживали параметризованные модули и инстанцирование таких модулей. Однако эти возможности были исключены из VDMTools примерно в 2000 году, поскольку они практически не использовались в промышленных приложениях и создавали значительные проблемы для инструментов.
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++ структурирование выполняется с использованием классов и множественного наследования. Ключевые понятия:
Класс: Каждый класс синтаксически начинается с ключевого слова `class`, за которым следует имя класса. В конце класса указывается ключевое слово `end`, за которым снова следует имя класса.
Наследование: Если класс наследует конструкты от других классов, то после имени класса в заголовке класса могут следовать ключевые слова `is subclass of`, за которыми следует список имен суперклассов, разделенных запятыми.
Модификаторы доступа: Сокрытие информации в VDM++ осуществляется тем же способом, что и в большинстве объектно-ориентированных языков, с использованием модификаторов доступа. В VDM++ определения по умолчанию являются приватными, но перед всеми определениями можно использовать одно из ключевых слов модификатора доступа: `private`, `public` и `protected`.
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: Некоторые ключевые компоненты серверной части системы TradeOne, разработанной CSK systems для японской фондовой биржи, были разработаны с использованием 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 начинается с очень абстрактной модели и переходит к реализации. Каждый этап включает в себя материализацию данных, а затем декомпозицию операций. Материализация данных развивает абстрактные типы данных в более конкретные структуры данных, в то время как декомпозиция операций развивает (абстрактные) неявные спецификации операций и функций в алгоритмы, которые могут быть непосредственно реализованы на выбранном языке программирования.