Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL (Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL.pdf)

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТимени М.В. ЛОМОНОСОВАФакультет вычислительной математики и кибернетикиЕ.А. Кузьменкова, А.К. ПетренкоПРАКТИКУМ ПО ФОРМАЛЬНОЙ СПЕЦИФИКАЦИИПРОГРАММ НА ЯЗЫКЕ 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-5ISBN 978-5-317-02422-2© Издательский отделфакультета Вычислительнойматематики и кибернетики МГУим. М.В. Ломоносова, 2008© Е.А. Кузьменкова, А.К. Петренко, 20082ВВЕДЕНИЕ«Методы формальной спецификации программ» – завершающий курс блока«Программная инженерия».

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

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

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

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

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

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

Описываются основные понятия языка, способы спецификации функций,приводятся упражнения по основным разделам языка RSL и конкретныерекомендации по их выполнению. Вторая часть пособия содержит описаниезадания практикума на ЭВМ, основной целью которого является разработкаспецификаций программной системы средней сложности на языке RSL, здесь жеприводятся конкретные варианты заданий практикума. В третьей части содержатсяпримеры вариантов письменного экзамена прошлых лет с решениями.Работа над пособием выполнена в рамках образовательной программы«Формирование системы инновационного образования в МГУ».4ГЛАВА 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 – строки символов,5Unit – содержит единственное специальное значение ().Тип 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 = 4int −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 и в выражениях его вхождения могутпоявляться в позициях, предусмотренных для значений различных типов.6Например, chaos может встречаться как вместо вхождения значений типа Bool, так и вместо типа Int. Другой специфической особенностью языка RSL является принятая в немсокращенная схема вычисления логических выражений, т.е. вычисление второгооперанда выражения не производится, если значение всего выражения полностьюопределяется значением его первого операнда.Ниже приводятся таблицы истинности (с учетом  chaos) для основныхлогических операций.