Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL, страница 11
Описание файла
PDF-файл из архива "Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 11 страницы из PDF
Терминаторы переходов6.5.8.1. Символ перехода в состояниеСимвол перехода в новое состояние определяет, в каком состоянии процессбудет ожидать следующего сигнала. <dash nextstate> означает, что изменениясостояния не происходит. Конструкция <dash nextstate> оказывается особенноценной при организации помеченных участков графа.Графический синтаксис:<nextstate area><nextstate body><dash nextstate><state name> ::=::= <state symbol> contains <nextstate body>::= { <state name> | <dash nextstate> }::= <name>6.5.8.2.
Символ перехода на меткуСимвол перехода на метку осуществляет передачу управления на новыйучасток перехода. Заметим, что явная передача управления на текущий переходявляется единственным средством организации циклов.Графический синтаксис:<merge area> ::= <merge symbol> is connected to<flow line symbol><merge symbol> ::= <flow line symbol><flow line symbol> ::=<out-connector area> ::= <out-connector symbol> contains<connector name><out-connector symbol> ::= <in-connector symbol>6.5.8.3. Символ остановкиВыполнение остановки процесса приводит к уничтожению всех переменныхпроцесса и всех необработанных сигналов из входного порта процесса.Графический синтаксис:<stop symbol> ::=636.5.8.4.
Символ возврата из процедурыВозврат из процедуры означаеткотором произошел вызов процедуры.продолжение того перехода, наГрафический синтаксис:<return area> ::= <return symbol>[ is associated with <expression> ]<return symbol> ::=6.5.9. Действия6.5.9.1.
ПрисваиваниеГрафический синтаксис:<task area> ::= <task symbol> contains <assignment statement><task symbol> ::=6.5.9.2. Создание процессаГрафический синтаксис:<create request area> ::= <create request symbol>contains <create body><create request body> ::= <name> [ <actual parameters> ]<actual parameters> ::= ( <expression> { , <expression> }* )<create request symbol> ::=Динамическое поведение SDL системы описывается внутри процессов.Процессы могут создаваться при запуске системы, а также могут создаватьсяи уничтожаться динамически во время выполнения системы. Можетсуществовать более одного экземпляра одного и того же процесса. Каждыйэкземпляр процесса имеет уникальный идентификатор PId.
Это делаетвозможным посылку сигнала конкретному экземпляру процесса.Формальные параметры процесса получают свои значения при егосоздании. У экземпляров процессов, которые создаются статически, значенияформальных параметров неопределены.64У каждого процесса есть четыре стандартные переменные типа PId:- Собственный идентификатор процесса (переменная self);- Идентификатор родительского процесса (переменная parent);- Идентификатор последнего процесса, порожденного данным процессом(переменная child);- Идентификатор процесса, от которого был получен последнийполученный сигнал (переменная sender).При попытке создания лишних экземпляров процесса (т.е. больше чем<maximum number>, новый экземпляр не создается, переменная offspringполучает значение Null, а выполнение перехода продолжается.6.5.9.3.
Вызов процедурыГрафический синтаксис:<procedure call area> ::= <procedure call symbol> contains<procedure call body><procedure call body> ::= <name> [ <actual parameters> ]<procedure call symbol> ::=6.5.9.4. Посылка сигналаПри посылке сигнала можно явно указать маршрут, по которому долженбыть направлен сигнал (конструкция via), либо процесс-получатель(конструкция to) в одной из двух форм: либо имя процесса-получателя, либоуникальный PId процесса-получателя. Если при посылке сигнала указаноимя процесса-получателя, то сигнал попадет к произвольному экземплярупроцесса с данным именем (если таковые вообще существуют).Графический синтаксис:<output area> ::= <output symbol> contains <output body><output body> ::= <signal name> [ <actual parameters> ][ to <destination> ] [ via <via path> ]<destination> ::= <Pid expression> | <name><via path> ::= <channel name>| <signal route name><signal name> ::= <name><channel name> ::= <name><signal route name> ::= <name><output symbol> ::=656.5.10.
УсловияГрафический синтаксис:<decision area> ::= <decision symbol> contains <question>is followed by{ { <graphical answer part><graphical else part> }*| { <graphical answer part> {<graphical answer part>}+[ <graphical else part> ] }*<decision symbol> ::=<graphical answer part> ::= <flow line symbol>is associated with <graphical answer>is followed by <transition area><graphical else part> ::= <flow line symbol> is associated with<else answer>is followed by <transition area><graphical answer> ::= <range condition><else answer> ::= else6.5.11.
ТаймерыГрафический синтаксис:<timer definition> ::= timer <timer name> [ <sort list> ][ := <Duration ground expression> ]<set area> ::= <task symbol> contains <set><reset area> ::= <task symbol> contains <reset><set> ::= set <set statement><set statement> ::= ( [ <Time expression> ,] <timer name>[ ( <expression list>) ] )<reset> ::= reset ( <reset statement> )<reset statement> ::= <timer name> [ ( <expression list> ) ]<timer name> ::= <name><Time expression> ::= <expression><Duration expression> ::= <expression>66Рис.
14. Пример диаграммы процесса6.6. ДанныеОсновным механизмом описания данных в языке SDL являютсяалгебраические спецификации абстрактных типов данных. Абстрактный типданных – это тип данных, внутреннее устройство которого не определено.Вместо этого, для абстрактного типа данных задаются набор литералов,набор операторов и набор аксиом, которым эти операторы должныудовлетворять. Подробное рассмотрение алгебраических спецификацийабстрактных типов данных в данном пособии не предусмотрено.В языке SDL имеется набор предопределенных типов данных:Integer, Real, Natural, Boolean, Character, Duration, Time, Charstring, PId.Ниже приводится упрощенный синтаксис выражений в языке SDL.Графический синтаксис:<range condition> ::= { <closed range> | <open range> }{ , { <closed range> | <open range> } }*<closed range> ::= <constant> : <constant>67<open range> ::= <constant>| { = | /= | < | > | <= | >= } <constant><expression> ::= <sub expression><sub expression> ::= <operand0> | <sub expression> => <operand0><operand0> ::= <operand1> | <operand0> {or | xor } <operand1><operand1> ::= <operand2> | <operand1> and <operand2><operand2> ::= <operand3>| <operand2> {= | /= | > |>= | < | <= | in } <operand3><operand3> ::= <operand4> | <operand3> { + | - | // } <operand4><operand4> ::= <operand5> |<operand4>{*|/|mod|rem } <operand5><operand5> ::= [ - | not ] <primary><primary> ::= <name>| ( <expression> )6.7.
ЗаключениеВ данном разделе мы подробно рассмотрели основные возможности языкаспецификаций и описаний SDL.Мы рассмотрели основные структурные единицы языка SDL: систему,блок, процесс и процедуру. Мы также рассмотрели организациювзаимодействия процессов через посылки сигналов по статическиммаршрутам, состоящих из межблочных и межпроцессных каналов, связанныхсоединениями. Мы рассмотрели средства описания поведения процесса какрасширенного конечного автомата.Отметим, что некоторые возможности языка остались за рамками нашегорассмотрения:• Структурные типы- Определение структурных типов- Использование типизированных объектов- Наследование структурных типов- Специализация структурных типов- Специализация поведения процессов- Определения пакетов• Алгебраические спецификации абстрактных типов данных• Процедурные определения операторов абстрактных типов данных68Глава 7. Организатор системы SDTДанная часть пособия представляет собой практическое руководство поредактору SDL диаграмм системы SDT.
Предполагается, что все упражнения,описанные в данном разделе, будут проделаны на компьютере. В следующихглавах мы будем разрабатывать MSC и SDL спецификации примера"Игральный автомат".7.1. Пример "Игральный автомат"Внешнее поведение системы выглядит следующим образом. Системавоспринимает четыре типа входных сигналов: Newgame (новая игра),Endgame (конец игры), Probe (ход) и Result (счет).
Первые два сигналаиспользуются для начала и окончание игры. Одновременно может вестисьтолько одна игра, т.е. сигналы Newgame игнорируются в течение игры, асигналы Endgame игнорируются, если игра не началась.Сама игра очень простая. Состояние системы время от временименяется от выигрышного к проигрышному и обратно. Игрок долженугадать, в какой момент состояние выигрышное. Если игрок делает ход(посылает сигнал Probe) в тот момент, когда состояние системывыигрышное, он получает одно очко. Если игрок делает ход в момент, когдасостояние системы проигрышное, он теряет одно очко. Игрок может узнатьтекущий счет, послав сигнал Result.7.2.