Спецификация программ средствами RAISE

RAISE-метод и RSL-спецификация (RAISE Specification Language) [6.9, 6.10] были разработаны в 80-х годах как результат предварительного исследования формальных методов и их пополнения новыми возможностями. Метод содержит нотации, техники и инструменты для конструирования программ и доказательстве их правильности. Он имеет программную поддержку в виде набора инструментов и методик, которые постоянно развиваются и используются при доказательстве правильности программ, описанных в RSL и ЯП (С++ и Паскаль). Язык RSL содержит абстрактные параметрические типы данных (алгебраические спецификации) и конкретные типы данных (модельноориентированные), подтипы, операции для задания последовательных и параллельных программ. Он предоставляет аппликативный и императивный стиль спецификации абстрактных программ, а также формальное конструирование программ в других ЯП и доказательство их правильности. Синтаксис этого языка близок к синтаксису языков С++ и Паскаль.
В RSL-языке имеются предопределенные абстрактные типы данных и конструкторы сложных типов данных, такие как произведение ( ), множества ( ), списки ( ), отображения ( ), записи ( ) и т.п. Далее рассмотрим некоторые конструкторы сложных типов данных.
Произведение типов- это упорядоченная конечная последовательность типов произведения ( ) . Представитель типа имеет вид ( ), где каждое -это значение типа . Компонент произведения можно получить операцией и переслать , т.е.

Количество компонентов произведения d находится таким образом:

Конструктор произведения и строит произведение вида:

Для каждого конкретного типа можно построить конструктор значения этого типа из отдельных компонентов произведения таким образом:

где каждое значение имеет тип , а результирующее значение - тип произведения
Списки типов- это последовательность значений одного типа , могут быть конечным списком типов и неконечными списком типов . В качестве структур данных типа списка может быть бинарное дерево, в котором есть голова ( ) и сын ( ), который следует за ним в списке, и хвост. К операциям списка относится операция - взятия первого элемента списка, т.е. головы, и операция - хвоста остальных элементов (аналогично как в VDM).
Функция выбирает из списка -элемент. Индекс элемента помогает выбрать нужный элемент списка:

Для определения количества элементов в списке выполняется функция:

Элемент списка находится так:

Аналогично можно представить функции конкатенации, преобразование типов данных, добавления элемента в голову и хвост списка и др.
Отображение - это структура ( ), которая ставит в соответствие значениям одного типа значение другого типа. Вместе с тем отображение - это бинарное отношение декартова произведения двух множеств как совокупности двухкомпонентных пар, в которых первый компонент - содержит элементы аргументов отображения, а второй компонент - соответствующие элементы значений этого отображения.
В языке имеются разные допустимые операции над отображениями: наложение, объединение, композиция, срез и др. Среди этих видов отношений рассмотрим, например, композицию отображений ( , ):

При этом используются функции:

Запись - это совокупность именованных полей. Этот тип соответствует типу в языке Паскаль и в языке С++. В языке RAISE для записи определено два конструктора - , , описание которых имеет вид

Идентификатор - это конструктор типа , для которого задается деструктор как функции получения значения компонентов записи.
Объединение - это конструктор для объединения типов , при котором тип получает одно из значений в списке элементов.
Конструктор типа имеет вид

Операции над самим типом не определены в языке RAISE.
Рассмотренные формальные структуры данных языков VDM и RAISE предназначены для математического описания программ с помощью утверждений и конструирования новых структур данных, необходимых для проектируемых программ. Средства этих языков фактически - элементы спецификации программ, по которым проще проверять правильность программ методами верификации или доказательства, составляя при этом, как и в случае VDM, пред, постусловия и утверждения для проведения доказательства программы по ее спецификациям.