Формальные методы
Понятие формальные методы более всего связано с математическими техниками спецификаций, верификации та доказательства правильности создаваемых программ. Эти методы содержат математическую символику, формальную нотацию, аппарат вывода и потому они трудно используются рядовыми программистами. Кроме того, постоянно развиваемые эти средства не вкладываются в стандартизованные процессы ЖЦ, в котором регламентированы все основные и дополнительные процессы (управление качеством, проектом, ресурсами и др.).
За многие годы своего существования (более 20–лет) такие известные формальные методы, как VDM, Z, RAISE [43–46] используются редко, эпизодически в реальных проектах, более всего в университетских и академических организациях и до промышленного производства фактически не дошли.
Это связано с тем, что формальные техники трудно использовать практически особенно в системах реального времени, где особенно важно применение формальных методов для создания более надежных программ, стоимость разработки которых возрастает, так как тратиться много времени на спецификацию и верификацию.
Наука формального проектирования ПС получила значительный прогресс при создании обобщенного UML, который доведен до стандарта, отодвинув на второй план такие средства спецификации, как RAISE, VDM и др.
Далее рассматриваются некоторые техники спецификации моделей программ и методы формального доказательства.
Графова модель VDM создается с помощью композиционной теоремы [5], которая определяется в виде ациклического графа, узлы которого – модули, а дуги – интерфейс между модулями.
Каждому модулю модели соответствует сервис как provider, так и потребителя (consumer) услуг. Дуга графу от модуля M к N определяет интерфейс, который может предоставлять модуль N для модуля M.
Базисом формального метода представления модели есть спецификация интерфейсов модулей для двух выше указанных пользователей сервисов.
Интерфейс удовлетворяет следующим свойствам:
– разделенность (separable) модулей с точки зрения проектирования и спецификации, интерфейс которых не требует описания среды модуля;
– композиционность (сомроsіtіоn), когда модули соединяются через композиционную теорию в систему с гарантированными связями между ними.
Данная теория базируется на модели интерфейса для взаимодействия модулей системы между собою через сетевые протоколы (TCP, UDP и др.). Каждый протокол передает разным модулям этой модели параметры для нахождения нужного сервиса.
Модель интерфейса задает связь модуля со средой в виде дискретного события (event), которое возникает только тогда, когда модуль и среда действуют вместе, и создают событие, рассматриваемое со стороны интерфейса. Иными словами, интерфейс специфицируется в виде множества последовательностей событий для наблюдения за поведением модулей модели.
Предположим, что S определяет спецификацию модуля M, которая включает в себя все возможные случаи его поведения и задает разные ситуации, которыми могут быть:
– событие интерфейса или состояние наблюдателя системы;
– анализ является конечным или представлен неопределенной последовательностью;
– формализм определения этой последовательности;
– условия выполнения события.
Эти предположения разрешают обеспечить разноуровневую систему взаимодействия модулей модели через механизм протоколов и систему наблюдения за событиями.
Формальный метод и спецификация RAISE. RAISE– метод и RSL–спецификация (RAISE Spesification Language) [45, 46] были разработаны в 1985–1998гг. как результат предварительного исследования формальных методов. Метод содержит нотации, техники и инструменты для использования формальных методов при конструировании ПС и доказательстве их правильности. Метод имеет программную поддержку в виде набора инструментов и методик, которые постоянно развиваются и используются для конструирования и доказательства правильности программ.
описанных в RSL и ЯП (С++ и Паскаль).
Язык RSL содержит абстрактные параметрические типы данных (алгебраические спецификации) и конкретные типы данных (модельно–ориентированные), подтипы, операции для задания последовательных и параллельных программ, предоставляет аппликативный и императивный стиль спецификации абстрактных программ, а также формальное конструирование программ в других ЯП и доказательства их правильности. Синтаксис этого языка близок к синтаксису языков С++ и Паскаль.
В RSL–языке имеются предопределенные абстрактные типы данных и конструкторы сложных типов данных, такие как произведение (product), множества (sets), списки (list), отображения (map), записи (record) и т.п. Далее рассмотрим, для примера, некоторые конструкторы сложных типов данных.
1. Произведение типов – это упорядоченная конечная последовательность типов Т1, Т2 , …, Тn произведения (product) Т1 ´ Т2 ´, …, ´ Тn . Представитель типа имеет вид (v1, v2 , …, vn ), где каждое vi есть значением типа Тi. Компонент произведения можно получить get и переслать set, т.е.
get component (i, d) = getvalue (i, d),
set component (d, i, val) = d ÞÑ (I ® val).
Количество компонентов произведения d находится таким образом:
size (d) = id Ñ (null (couter inc(counter))).
Конструктор произведения d1 и d2 строит произведение d1 ´ d2 вида
product (d1 , d2 ) = id Ñ (size (d1) Þ couter 1) Ñ (null (couter 2) inc couter 2))).
Для каждого конкретного типа product (Т1 ´Т2
´, …, ´ Тn) можно построить конструктор значения этого типа из отдельных компонентов произведения таким образом:
make product (value 1, …, value n) = (value i Þ 1) Ñ… Ñ (value n Þ n),
где каждое значение value i имеет тип Тi , а результирующее значение – тип произведения Т1 ´Т2 ´, …, ´ Тn .
2. Списки типов – это последовательность значений одного типа списка list Т, могут быть конечным списком типов Тk и неконечными списком типов T n . в качестве структур данных типа списку может быть бинарное дерево, в котором есть голова (head) и сын ( tail), следует за ним в списке и хвост. Операциями для списка является операция hd взятия первого элемента списка, т.е. головы и операция tl – хвоста остальные элементы.
Функция Caddr (I) = L Þ tail Þtail Þ Head выбирает из списка I –элемент. Индекс элемента помогает выбрать нужный элемент списка Index(I, idx) = L (idx) =
while (Ø is null(idx))do((L Þ tail ÞL) Ñdec(idx)) L Þ Head. Для определения количества элементов в списке выполняется функция
len (L) = (ld Ñ null (result))
while (L Þ) do (( L Þ tail Þ tail ÞL) Ñ inc (result))
result Þ
Элемент списка находится так:
elem (L) = (ld Ñ empty (result))
while (L Þ) do (( L Þ tail ÞL) Ñ
( result ( LÞ head Þ) Þ elem ) Þ result)
result Þ.
Аналогично можно представить функции конкатенации, преобразование типов данных, добавления элемента в голову и хвост списка и др.
3. Отображение – это структура (map), которая ставит в соответствие значениям одного типа значение другого типа. С другой стороны, отображение является бинарным отношением декартового произведения двух множеств, как совокупности двухкомпонентных пар, в которой первый компонент arg содержит элементы аргументов отображения, а другой компонент res соответствующие элементы значений этого отображения.
В языке представлены разные допустимые операции над отображениями: наложение, объединение, композиция, срез и др. Среди этих видов отношений рассмотрим только композицию отображений.(m1, m2).
(ld Ñ (compose (m1, m2) Þ m)) apply (m, elem)
apply to composition (m1, m2, elem) =
(ld Ñ (image (elem, m1) Þ s) restrict (m2, s) Þ map
(ld Ñ (map getname elem Þ name)) getvalue (name, map).
При этом используются функции:
Apply (m, elem) = image (elem, m) elem Þ,
Apply (m, elem) = getvalue (elem, m) elem Þ.
4. Запись – это совокупность именованных полей. Этот тип соответствует типу record в языке Паскаль и struct в языке С++. В языке RAISE определено два конструктора типа, record, shurt record, которые описываются в виде – type record id =
type mk_id (short _record id ) ::=
destr_id1 : type_expr1 « recon_id
. . .
destr_idn : type_exprn « recon_id.
Идентификатор mk_id является конструктором типа record, для которого даны деструкторы destr_idn , как функции получения значения компонентов записи.
5. Объединение – это конструктор Union, обеспечивающий объединение типов
type id = id1 , id2 ,…, idn
при котором тип id получает одно из значений в списке элементов.
Конструктор этого типа имеет вид:
type id = id_from_ id1 (id_to_ id1: id1) ½… ½ id_from_ idn (id_to_ idn: idn)/
Операции над самим типом не определены в языке RAISE.
Рассмотренные формальные структуры данных языка RAISE позволяет математически описывать и конструировать новые структуры данных в проектируемых программах. Их проще проверять на правильность методами верификации.
