Конструкция и символы SDL

Конструкция start. Стартовое состояние процесса конвертируется в БП, у

которого в качестве предусловия записано (начальное) состояние init. В постусловии БП записывается состояние, заданное конструкцией start. Заметим, что все агенты инициируются состоянием init как в исходном состоянии, так и для случая динамически созданных экземпляров агентов.

Состояние процесса. Конструкция state <имя состояния> транслируется в

соответствующую проверку специального атрибута state в предусловии:

Так как конструкция state * означает «все состояния», то она просто игнорируется при трансляции.

Конструкция state *(x) означает «все состояния кроме х» и записывается в

предусловии в виде соответствующих неравенств:

Чтение сигнала из очереди (input). Функциональность приема/посылки

сигналов реализуется с помощью структуры данных типа «очередь» и набором операторов над ней: is_in_list, add_elem, remove_elem, и др. Так же определена функция First(<имя списка>, <условие>), которая находит первый элемент из списка <имя списка>, удовлетворяющий условию <условие>. Для полной реализации работы с входящими сообщениями необходимо описать обработку конструкции SAVE <имя сигнала>. Для этого организуем дополнительный список save_list, в который будут записываться сохраняемые сигналы в постусловии:

Тогда конструкция input запишется с использованием функции First:

В постусловии сигнал удаляется из очереди посредством выполнения операции remove_elem(<элемент>, <имя очереди>) и выполняется присваивание атрибута SENDER:

<имя типа процесса> <процесс>.SENDER:= pid

Посылка сигнала (output). Посылка сигнала транслируется в оператор

add_tail(<имя сигнала>,<имя очереди входящих сигналов адресата>) в постусловии.

Оператор task и вызовы процедур. Этот оператор выполняет присваивания,

в т.ч. вызовы процедур (с присвоением возвращаемого значения). Присваивания транслируются тривиально, для правильной же симуляции вызова процедур организуем специальную структуру данных типа стек. Используется классическая семантика стека для вызова процедур – в него попадают как локальные переменные, так и точка возврата.

Символы SDL

SDL/GR	SDL/PR	Значение символов
	STATE NEXTSTATE	Состояние Следующее состояние
	TASK	Задача
	INPUT	Ввод
	OUTPUT	Вывод
	SAVE	Сохранение
	DECISION	Решение
	CALL	Вызов процедуры
	MACRO	Вызов макро
	CREATE	Запрос создания процесса
	ALTERNATIVE	Опции
	STOP	Останов
	RETURN	Возврат из процедуры
	ENDMACRO	Выход из макро
	START	Старт процесса
	PROCEDURE	Начало процедуры
	MACRO EXPANSION	Вход в макро
		Расширение текста
	COMMENT	Kомментарии
	X: JOIN X	Входной соединитель Выходной соединитель
		Все
		Все, кроме
	PROVIDED	Непрерывный сигнал

40) Методы формальной спецификации программ; 41) Объектно – ориентированные методы

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

Можно выделить три уровня применения формальных методов:

Нулевой уровень

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

Первый уровень

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

Второй уровень

Автоматические доказатели теорем используются для выведения полностью формализованных доказательств, проверяемых автоматически. Подход требует объёмных вложений и исследований, но оправдывает себя в самых критичных частях сложных систем, где ошибки непозволительны (например, в проектировании интегральных схем).

«Методы формальной спецификации программ». Курс состоит из двух частей.

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

Языки формальных спецификаций были разработаны для того, чтобы

упростить и там, где это возможно, автоматизировать процессы создания и

анализа программного обеспечения.

Дата добавления: 2015-08-13