Е.А. Кузьменкова, А.К. Петренко - Формальная спецификация программ на языке RSL (1158800)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

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

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

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

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

Формальная спецификация программ

на языке RSL

(методическое пособие по практикуму)

1999

Введение

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

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

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

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

В качестве такого языка был выбран RSL. Этот язык является языком методологии разработки программ RAISE - Rigorous Approach to Industrial Software Engineering. RAISE является результатом работы группы европейских ученых, которые в конце 80-х годов объединилась для создания метода разработки программного обеспечения, пригодного для использования не только в исследовательских целях, но и в индустрии.

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

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

Глава 1. Основные понятия языка RSL

1. Основные типы языка RSL. RSL логика

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

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 = 4

int 4.6 = 4

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

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

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

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

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

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

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

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

 chaos  chaos

В таблицах истинности для операций = и  символы a и b обозначают выражения, значения которых отличаются друг от друга.

На основании приведенных таблиц можно заметить, например, что в отличие от классической логики в RSL операции  и  не обладают свойством коммуникативности, т.е. выражения  e₁  e₂  e₂  e₁ и e₁  e₂  e₂  e₁  уже не являются тавтологиями.

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

if value_expr then value_expr₁ else value_expr₂ end,

где value_expr является логическим выражением, а выражения value_expr₁ и value_expr₂ имеют один и тот же тип, который является и типом всего условного выражения. При вычислении значений условных выражений необходимо иметь в виду следующие свойства:

if true then expr₁ else expr₂ end  expr₁ (1)

if false then expr₁ else expr₂ end  expr₂ (2)

Характеристики

Тип файла документ

Документы такого типа открываются такими программами, как Microsoft Office Word на компьютерах Windows, Apple Pages на компьютерах Mac, Open Office - бесплатная альтернатива на различных платформах, в том числе Linux. Наиболее простым и современным решением будут Google документы, так как открываются онлайн без скачивания прямо в браузере на любой платформе. Существуют российские качественные аналоги, например от Яндекса.

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

Файлы такого типа обычно разбиты на страницы, а текст может быть форматированным (жирный, курсив, выбор шрифта, таблицы и т.п.), а также в него можно добавлять изображения. Формат идеально подходит для рефератов, докладов и РПЗ курсовых проектов, которые необходимо распечатать. Кстати перед печатью также сохраняйте файл в PDF, так как принтер может начудить со шрифтами.

Список файлов книги