МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

имени М.В. ЛОМОНОСОВА

Факультет вычислительной математики и кибернетики

Е.А. Кузьменкова, А.К. Петренко

Практикум по формальной спецификации программ на языке RSL

МОСКВА

2008

УДК 378(075.8):004.43

ББК 32.973-018.1я73

К89

Пособие содержит справочные и методические материалы по практическому освоению основных разделов курса лекций «Формальная спецификация и верификация программ», касающихся использования языка спецификаций RSL. В пособии приводятся упражнения по основным разделам языка RSL и рекомендации по их выполнению, а также предлагаются варианты задания практикума и примеры экзаменационных билетов.

Работа над пособием выполнена в рамках образовательной программы «Формирование системы инновационного образования в МГУ».

Для студентов программистских кафедр факультета ВМиК в поддержку лекционного курса «Формальная спецификация и верификация программ» и для преподавателей, ведущих практические занятия по этому курсу.

Рецензенты:

Кузнецов С.Д., д.т.н., профессор

Соловьев С.Ю., д.ф.-м.н., профессор

Е.А. Кузьменкова, А.К. Петренко «Практикум по формальной спецификации программ на языке RSL» — М. Издательский отдел факультета ВМК МГУ (лицензия ИД № 05899 от 24.09.01), 2008. — 88 с.

Печатается по решению Редакционно- издательского Совета факультета Вычислительной математики и кибернетики МГУ ми. М.В. Ломоносова.

ISBN 978-5-89407-338-5 © Издательский отдел

ISBN 978-5-317-02422-2 факультета Вычислительной

математики и кибернетики МГУ

им. М.В. Ломоносова, 2008

© Е.А. Кузьменкова, А.К. Петренко, 2008

ВВЕДЕНИЕ

«Методы формальной спецификации программ» – завершающий курс блока «Программная инженерия». В настоящее время он состоит из трех курсов:

• Объектно-ориентированный анализ и проектирование

• Верификация программ на моделях

• Методы формальной спецификации программ

За рамками блока пока находятся вопросы организации производства программных средств (ПС), управление требованиями, верификация и валидация, оценка стоимости ПС и сроков разработки и другие. Сейчас блок представляет некоторое сужение предмета программной инженерии. В таком виде его можно было бы назвать как «Конструирование программных систем». При рассмотрении проблем конструирования программных систем необходимо не забывать о двух аспектах программной системы:

• структурном (архитектурном)

• функциональном (поведенческом)

Программисты часто увлекаются первым, тогда как для пользователя или заказчика скорее более важным представляется второй. Однако искусство разработчика программной системы состоит в том, чтобы постоянно держать в поле зрения оба ракурса рассмотрения. Поэтому для профессионального разработчика важно умение рассматривать и структурные, и функциональные аспекты системы/проекта и находить компромиссы там, где функциональные требования приходят в противоречие с архитектурными решениями.

Сопоставляя проблемы архитектурного и функционального анализа систем можно сделать вывод, что структурный аспект на практике превалирует над функциональным. Это, в частности, объясняется тем, что он опирается на достаточно хорошо известные нотации (языки программирования) и инструменты, и тем что задачи конструирования изучаются в многих учебных курсах, соответственно, специалистов в области конструирования/программирования программных систем много. Методы описания и исследования систем в функциональном аспекте не так развиты. Задачей курса «Методы формальной спецификации программ» является, хотя бы частичное, восполнение этого пробела.

Многие исследователи-специалисты по формальным методам разработки программ акцентируют свое внимание на собственно формальном аппарате, используемом для анализа спецификаций, на инструментах, которые упрощают работу с формальными спецификациями. Эти работы, конечно, важны. Но чрезмерное увлечение математической стороной дела не только не помогает в решении практических задач, но часто и строит дополнительные трудности. Здесь, как и в любой инженерной задаче, важно находить компромисс в сочетании строгих, формальных методов и инженерных, эмпирических подходов. В практике использования формальных спецификаций главной инженерной задачей является выбор метода абстракции реальной целевой системы, который позволяет построить модель поведения, которая представляет, с одной стороны, необходимое приближение поведению реальной системы, и, с другой стороны, достаточно простой, чтобы обеспечивать возможность использования выбранного формального аппарата, имеющихся инструментов для работы со спецификациями.

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

В рамках одного курса, конечно, невозможно обхватить все методы и используемые формальные аппараты. Задача курса – показать, как формальные спецификации могут предоставить некоторую строгую концептуальную основу, позволяющую там, где это необходимо, обеспечить корректность реализации за счет доказательной демонстрации корректности самих спецификаций и соответствия реализации требованиям, заданными данными спецификациями. Авторы пособия пытались подобрать материал таким образом, чтобы студенты и преподаватели на учебных задачах смогли познакомиться с различными видами и методами использования формальных спецификаций.

Пособие состоит из трех частей. Первая часть содержит методические указания для проведения занятий практикума по освоению языка спецификаций RSL. Описываются основные понятия языка, способы спецификации функций, приводятся упражнения по основным разделам языка RSL и конкретные рекомендации по их выполнению. Вторая часть пособия содержит описание задания практикума на ЭВМ, основной целью которого является разработка спецификаций программной системы средней сложности на языке RSL, здесь же приводятся конкретные варианты заданий практикума. В третьей части содержатся примеры вариантов письменного экзамена прошлых лет с решениями.

Работа над пособием выполнена в рамках образовательной программы «Формирование системы инновационного образования в МГУ».

ГЛАВА 1. ОСНОВНЫЕ ТИПЫ ЯЗЫКА RSL. СПЕЦИФИКА RSL-ЛОГИКИ

Концепция типов в языке RSL (встроенные, абстрактные, составные). Описание подтипов. Встроенные типы языка RSL. Логика в языке RSL. Квантифицированные и условные выражения RSL. Упражнения.

Концепция типов в языке RSL

В языке RSL имеется три вида типов:

• встроенные (предопределенные),

• абстрактные,

• составные (производные).

Встроенный тип определяется набором предопределенных литералов и операций над значениями данного типа.

Абстрактный тип представлен только идентификатором соответствующего типа. Значения такого типа не уточняются, в типе отсутствуют предопределенные операции генерации значений данного типа и манипулирования с ними (кроме операций = и ~=). С помощью абстрактного типа осуществляется декларация типа, про значения которого ничего не известно, кроме возможности сравнивать их посредством операций = и ~=.

Составной тип строится из других типов посредством применения типовых операций.

Над всеми типами определены операции = и ~=.

Описание подтипов

На основе любого типа можно построить подтип. Для задания подтипа необходимо определить с помощью предиката некоторое ограничение на исходный (базисный) тип. В общем случае описание подтипа имеет вид:

ST1 = {| t : T1:- p(t) |},

где ST1 обозначает определяемый подтип, T1 - исходный (базисный) тип, p(t) – предикат, задающий ограничение на значения базисного типа. Значениями подтипа являются все возможные значения исходного (базисного) типа, на которых предикат-ограничение принимает значение  true.

Встроенные типы языка RSL

В языке RSL предусмотрены следующие встроенные типы:

Bool – представляет булевские значения,

Int – целые числа,

Nat – натуральные числа,

Real – вещественные числа,

Char – символы,

Text – строки символов,

Unit – содержит единственное специальное значение ().

Тип Bool содержит два значения true и false, над значениями данного типа определены операции /\, \/, =>, , is (эквивалентность), , ~=.

Тип Int представляет все целые числа. Над значениями этого типа определены операции , , , /, \, , abs, real, где / означает целочисленное деление,  \ – взятие остатка от деления,  - возведение в степень, abs – префиксная операция для вычисления модуля числа и real – префиксная операция для преобразования из типа Int в тип Real. Заметим, что автоматического преобразования из типа Int в тип Real в RSL нет. Кроме того значения данного типа можно сравнивать с помощью операций , <=, , >=, , ~=.

Тип Nat содержит все натуральные числа 0, 1, 2, …, он является подтипом типа Int и задается соотношением:

Nat = { i : Int :- i >= 0 }.

К значениям этого типа применимы все операции, определенные для типа Int.

Тип Real представляет все действительные числа, к значениям этого типа применимы операции , , , /, , <, <=, , >=, , ~=, abs, int, где int – префиксная операция для преобразования из типа Real в тип Int, возвращающая ближайшее по направлению к 0 целое число. Например:

int 4.6 = 4

int 4.6 = 4

Наличие десятичной точки в записи вещественных констант обязательно (1.0, 12.35 и т.д.).

Тип Char содержит символы, к значениям этого типа применимы операции  и ~, константы типа Char заключаются в апострофы (например: f, Z и т.д.).

Тип Text предназначен для описания строк символов, причем каждая строка должна начинаться и заканчиваться символом . Например, ABC,  –пустая строка. К значениям этого типа применимы операции , ~=.

Тип Unit является аналогом типа void в языках C, C++, Java, C#, он используется в описаниях сигнатур функций для изображения отсутствия входных или выходных параметров.

Логика в языке RSL

Остановимся более подробно на вычислении логических выражений в языке RSL, поскольку принятая в языке логика имеет некоторую специфику по сравнению с классической логикой. Суть этой специфики связана с наличием в RSL специального выражения chaos, которое предназначено для обозначения непредсказуемого (хаотичного) поведения программы во время ее выполнения. Такое поведение может возникать в результате какого-либо отказа в программе и приводит к ситуации, когда вычисление значения какого-либо выражения может не завершиться (например, при вычислении выражения 1/x в точке x=0.0). chaos не принадлежит ни к одному из типов RSL и в выражениях его вхождения могут появляться в позициях, предусмотренных для значений различных типов. Например, chaos может встречаться как вместо вхождения значений типа Bool, так и вместо типа Int. 

Другой специфической особенностью языка RSL является принятая в нем сокращенная схема вычисления логических выражений, т.е. вычисление второго операнда выражения не производится, если значение всего выражения полностью определяется значением его первого операнда.

Ниже приводятся таблицы истинности (с учетом chaos) для основных логических операций. Левая колонка соответствует первому операнду, верхняя строка – второму операнду.

/\	true	false	chaos
true	true	false	chaos
false	false	false	false
chaos	chaos	chaos	chaos

\/	true	false	chaos
true	true	true	true
false	true	false	chaos
chaos	chaos	chaos	chaos

=>	true	false	chaos
true	true	false	chaos
false	true	true	true
chaos	chaos	chaos	chaos

Определение операции  необходимо расширить соотношением: