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