Е.А. Кузьменкова - Формальная спецификация программ (Е.А. Кузьменкова - Формальная спецификация программ.pdf)

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТимени М.В. ЛОМОНОСОВАФакультет вычислительной математики и кибернетикиЕ.А. Кузьменкова, А.К. ПетренкоФормальная спецификация программна языке RSL(методическое пособие по практикуму)19992ВведениеДанное пособие предназначено для поддержки двухсеместрового курса«Методы формальной спецификации программ». Курс состоит из двух частей.Первая часть рассматривает вопросы разработки программного обеспечения наоснове подходов, предложенных RAISE методологий, и вопросы автоматизациитестирования на основе формальных спецификаций, где в качествеиллюстративного материала также используются RAISE спецификации.

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

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

Эта задача для своего решения требуетсистематического применения разнообразных инженерных методов, часть изкоторых может с успехом использовать и формальные методы.Одной из важнейших целей данного курса была демонстрация современныхдостижений в области использования формальных методов при созданииреального программного обеспечения. Для решения этой задачи, с однойстороны, необходимо было выбрать язык спецификаций, зарекомендовавшийсебя как инструмент практических программистов, и, с другой стороны,показать, как формальные методы могут использоваться в ходе всех фазжизненного цикла программного обеспечения: от проектирования дотестирования.В качестве такого языка был выбран RSL. Этот язык является языкомметодологии разработки программ RAISE - Rigorous Approach to IndustrialSoftware Engineering.

RAISE является результатом работы группы европейских3ученых, которые в конце 80-х годов объединилась для создания методаразработки программного обеспечения, пригодного для использования не тольков исследовательских целях, но и в индустрии.RSL, с одной стороны, вобрал в себя полезные возможности несколькихдругих широко известных языков, таких как VDM/Meta-IV, Z, LOTOS, CSP, сдругой стороны, он оказался достаточно экономным и естественным, чтоупрощает его изучение и использование в программной индустрии. Одним изпривлекательных свойств RSL является его близость к традиционным языкампрограммирования.Данное руководство не заменяет ни описания языка, ни описаниясобственно RAISE методологии.

Наиболее полным описанием языка являетсямонография [1]. Руководство содержит краткие описания тем практическихзанятий и контрольных заданий, которые студенты выполняют при изученииданного курса лекций. По форме это упражнения для закрепления навыковиспользования RSL. Вместе с тем, обратим внимание читателя на то, что заэтими упражнениями стоит целый спектр задач разработки промышленногопрограммного обеспечения. Эти задачи должны не только помочь в овладенииязыком RSL, они должны научить видеть задачи системного анализа проектныхматериалов, реализации, форвард- и реверс-инженерии и научить решать ихсистематическим образом и, если это возможно, при помощи формальныхметодов.4Глава 1.

Основные понятия языка RSL1.1.Основные типы языка RSL. RSL логикаЦель данного раздела - описать основные встроенные типы языка RSL,уделяя особое внимание специфике RSL логики. Раздел содержит упражненияпо выработке навыков вычисления и оформления выражений языка RSL на базевстроенных типов.1.1.1. Встроенные типы языка RSLВ языке RSL предусмотрены следующие встроенные типы:Bool – представляет булевские значения,Int – целые числа,Nat – натуральные числа,Real – вещественные числа,Char – символы,Text – строки символов,Unit – содержит единственное специальное значение ().Тип Bool содержит два значения true и false, над значениямиданного типа определены операции ∧, ∨, ⇒, ∼, =, ≠.Для значений типа Int определены операции +, −, ∗, /, ↑, \, abs, real,где ↑ означает возведение в степень, \ – взятие остатка от деления, abs –префиксная операция для вычисления модуля числа и real – префикснаяоперация для преобразования из типа Int в тип Real.

Кроме того значенияданного типа можно сравнивать с помощью операций <, ≤, >, ≥, =, ≠.Тип Nat является подтипом типа 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″,″″″″ –пустая строка. К значениям этого типа применимы операции =, ≠.5Тип Unit используется в описаниях сигнатур функций для изображенияотсутствующих входных или выходных параметров.1.1.2. Логика в языке RSLОстановимся более подробно на вычислении логических выражений в языкеRSL, поскольку принятая в языке логика имеет некоторую специфику посравнению с классической логикой. Суть этой специфики связана с наличием вRSL специального выражения chaos, предназначенного для обозначениянепредсказуемого (хаотичного) поведения программы во время выполнения,возникающего в результате какого-либо отказа в программе и приводящего кситуации, когда вычисление значения какого-либо выражения может незавершиться.

chaos не принадлежит ни к одному из типов RSL и ввыражениях может появляться в позициях, предусмотренных для значенийразличных типов. Например, chaos может встречаться как вместо вхождениязначений типа Bool, так и вместо типа Int. В RSL принята сокращеннаясхема вычисления логических выражений, т.е. если значение всего выраженияполностью определяется значением его первого операнда, то вычислениевторого операнда не производится.Ниже приводятся таблицы истинности (с учетом chaos ) для основныхлогических операций. Левая колонка соответствует первому операнду, верхняястрока – второму операнду.∧truefalsechaostruetruefalsechaosfalsefalsefalsechaoschaoschaosfalsechaos∨truefalsechaostruetruetruechaosfalsetruefalsechaoschaostruechaoschaos⇒truefalsechaostruetruetruechaosfalsefalsetruechaoschaoschaostruechaosОпределение операции∼ chaos ≡ chaos∼ необходимо расширить соотношением:6В таблицах истинности для операций = и ≡ символыобозначают выражения, значения которых отличаются друг от друга.≡abchaosatruefalsefalsebfalsetruefalsechaosfalsefalsetrue=abchaosatruefalsechaosbfalsetruechaoschaoschaoschaoschaosa и bНа основании приведенных таблиц можно заметить, например, что вотличие от классической логики в RSL операции ∧ и ∨ не обладаютсвойствомкоммуникативности,т.е.выраженияe1 ∧ e2 ≡ e2 ∧ e1 иe1 ∨ e2 ≡ e2 ∨ e1 уже не являются тавтологиями.Для обеспечения возможности альтернативного выбора при вычислениивыражений в RSL введены условные выражения, имеющие следующий вид:if value_expr then value_expr1 else value_expr2 end,где value_expr является логическим выражением, а выражения value_expr1и value_expr2 имеют один и тот же тип, который является и типом всегоусловного выражения.

При вычислении значений условных выраженийнеобходимо иметь в виду следующие свойства:(1)if true then expr1 else expr2 end ≡ expr1(2)if false then expr1 else expr2 end ≡ expr2if a then expr1 else expr2 end ≡(3)if a then expr1[true/a] else expr2[false/a ] end(4)if chaos then expr1 else expr2 end ≡ chaosЗапись вида expr1[true/a] обозначает подстановку в выражение expr1значения true вместо a.Квантифицированные выражения языка RSL имеют традиционную форму ииспользуются в основном для записи аксиом.