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

Формальная спецификацияпрограмм. Модель свнутренним состояниемЕвгений Корныхин27 августа 2011 г.ОглавлениеЗачем нужен этот курс (вместо вступления)3Модели программ с внутренним состоянием41 RAISE Specification Language (RSL)1.1 Сигнатура модели с внутренним состоянием . .1.2 Предопределенные типы . . . .

. . . . . . . . . .1.3 Аппликативное описание операций . . . . . . . .1.4 Императивное описание операций . . . . . . . .1.5 Множества, списки, отображения . . . . . . . . .1.6 Эксплицитное и имплицитное описание функций....................................8811131427462 Контрактные спецификации2.1 Программные контракты . . . . .

. . . . . . . . . . . . . .2.2 Ситуации и ветви функциональности . . . . . . . . . . . .2.3 Программные контракты общего вида в RSL. Превыражения2.4 Финитные программные контракты . . . . . . . . . . . . .2.5 Инварианты состояния . . . . . . . . . . . . . . . .

. . . . .6162636971723 Инструмент Dafny774 Аналитическая верификация824.1 Методы Флойда . . . . . . . . . . . . . . . . . . . . . . . . 82А Приоритет операций в RSL89Литература902Оглавление3Зачем нужен этот курс (вместо вступления)Данный сборник задач написан в поддержку курса «Формальная спецификация и верификация программ», который читается студентам последних курсов факультета ВМК МГУ.Бытует точка зрения, что профессия программиста — писать код,конструировать программу на языке программирования. Чем больше качественного кода ты пишешь (в срок!), тем более ты профессионален, какпрограммист.

А те, кто код не пишут, занимаются проектированием («дизайном») программы, чтобы написание программы было удобным, самдизайн гибким и прочее, и прочее, и прочее. При всём при этом неявнопредполагается, что все предварительные действия для проектированияи кодирования очевидны и не стоят обстоятельного внимания программиста. В первую очередь в такое, неявное, может уходить тщательнаяпроработка логической части программы. Это, во-первых, задачи, которую должна решать программа, во-вторых, те термины и их взаимосвязи, которые должна обеспечивать и поддерживать программа, в-третьих,то, как программа должна себя вести в различных ситуациях, какие ситуации программа не должна допускать, какие соотношения между оперируемыми понятиями программы она должна поддерживать. Глубокойошибкой программиста будет думать, что эти вещи просты, тривиальны, очевидны, а, следовательно, не должны его сильно занимать.

Притаком отношении на финальных стадиях кодирования и отладки можетоказаться, что что-то недодумано, что-то неучтено, из-за чего приходится хорошо если просто переделать некую небольшую часть программы,а то и, возможно, придется переписывать всё с нуля. А какие-то проблемы (например, неучтенные ситуации в поведении программы) могутвыявиться только на этапе эксплуатации... (и чем выше цена ошибки,тем горше будет ее результат)В рамках курса постараемся поработать, проанализировать как постановку задачи, так и (на понятийном уровне) тот проект (дизайн) кода,который будет предлагать программист. В двух словах, проанализировать — значит, как минимум, выделить и зафиксировать, над какимипонятиями работает программа, какие действия над ними совершает, частично описать эти действия теоретически, описать решаемую программой задачу (требования), описать в виде предикатов («декларативно»)достижимые и разрешенные состояния (значения) этих понятий (в видеинвариантов), описать требуемые изменения значений при помощи дей-4Оглавлениествий на более общем уровне, чем это было бы в коде программы.

Построив такую формальную модель программы, взглянув на свою программу«по-другому» (как минимум, декларативно вместо конструктивно), естьгипотеза, что программист сможет увидеть больше особенностей в тойзадаче, которую решает программа, и в том, как она решает эту задачу.Итак, цель курса — видеть свойства программ, уметь представитьэти свойства в проверяемой форме. Под свойствами программ в первуюочередь понимаются свойства корректности.Профессионализм программиста, на самом деле, не только в том,сколько строчек качественного кода он выдает в сутки, но и в том, насколько глубоко он задумался над логикой работы программы, скольковопросов он поставил перед собой (или другими, кто участвует в написании программы) по поводу поведения и результатов работы программыи насколько он ответил на эти вопросы.Курс «Формальной спецификации и верификации программ» практически не касается формальных методов разработки программ (которые сегодня представляются в виде разработки, основанной на моделях,где программный код получается автоматически из модели, и использования утверждений специального вида для автоматизации тестированияпрограмм), поскольку это тема отдельного практического курса.Модели программ с внутренним состояниемВ рамках этого курса будут рассматриваться только программы, длякоторых можно составить модель с внутренним состоянием.Можно себе представить такую модель как черный ящик, способныйпринимать входные воздействия (название операции и ее аргументы) ивыдавать ответ (см.

рисунок 1). Например, операция — возведение вквадрат, аргумент — число 2, результат — число 4.операцияаргументысостояниерезультатоперацииРис. 1. Модель программы с внутренним состояниемОглавление5Например, для модели программы-калькулятора операцией будет выполнение некоторого арифметического действия или ввод числа.По сравнению с реальной программной системой в рассматриваемойнами модели нет таких понятий, как время выполнения операции и параллельное выполнение операций.

Иными словами, «операция» аналогична функциям, в математическом смысле (функция — как отображение входных данных к выходным, а не как подпрограмма). Но хотя нетпонятия времени выполнения операции, есть понятие последовательности операций над системой.Однако в этой модели выдача результата-значения (как в примере свозведением в квадрат числа 2) не является обязательной и однозначной.А именно,1) на входное воздействие модель может ответить тем, что она перестает выдавать ответы вообще («зацикливается»);2) на одни и те же входные воздействия модель может выдать различные ответы (модель недетерминирована);3) модель может ничего не ответить на входное воздействие в видерезультата, но при этом может оказать побочный эффект, и послеэтого продолжать выдавать ответы на следующие входные воздействия.Для нас важно, что на такой модели можно «формулировать свойства», т.е. можно дать определение правильной системы с теми же названиями операций.

Правильная система — та, что правильно выполняетоперации, поддерживает внутреннюю согласованность своих компонентов (согласованность внутреннего состояния), некоторым заданным образом изменяет состояние среды, в которой она работает.Попытка даже просто сформулировать такие свойства (т.е. проделать дополнительную работу в плюс к проектированию и кодированиюпрограммной системы) дает много преимуществ. Во-первых, это позволяет по-иному взглянуть на разрабатываемую систему, увидеть то, чтодо этого не было явно сказано, и, возможно, такой взгляд позволит увидеть ряд дефектов в проекте или даже исходном тексте (например, еслив исходном тексте был упущен какой-нибудь случай в работе системы).Во-вторых, поскольку свойства записаны на формальном языке, возможна автоматическая проверка как самих записанных свойств (на полноту,6Оглавлениена согласованность), так и проверка соответствия свойств и других артефактов разработки системы (например, соответствия свойств исходномутексту программы).Сначала надо попробовать почувствовать этот «иной взгляд», длячего вам будет предложено сделать ряд упражнений (см.

ниже). А послеэтого предлагается ознакомиться с формальным языком спецификации,на котором можно записывать свойства моделей.ЗадачиДля следующих технических средств, идей и технологий сформулируйте не определение, а область применения и эффект отприменения этого (эффект должен выражаться в некоторомкачественном изменении системы, к которой это средство применяется, или среды, где работает эта система)0.1.1 вытесняющая многозадачность (вид многозадачности, прикоторой операционная система может временно прервать текущий процесс без какой-либо помощи с его стороны)Решение:область применения: пользовательские процессы.эффект от применения: зависший процесс не завешивает всю ОС.0.1.2невытесняющая многозадачность0.1.3 пакетная обработка заданийРешение:эффект: для вычислительных задач – максимизация использованиявычислительных ресурсов.0.1.4разделение времени при обработке заданий0.1.5страничная организация виртуальной памяти0.1.6инвертированная таблица страниц0.1.7регистровые окнаОглавление70.1.8элеваторный алгоритм планирования дисковых обменов0.1.9файл, отображаемый в память0.1.10динамическая библиотека0.1.11страничный демон0.1.12монитор Хоара0.1.13буферизация ввода/вывода0.1.14дейтаграммные сокетыДля следующих программ и программных систем привести несколько примеров моделей с внутренним состоянием; какие возможны реализации этих систем, более мощные, чем конечные автоматы?0.2.1Стек.0.2.2Почтовый клиент (например, Mozilla Thunderbird или вебклиент Gmail).0.2.3Электронный будильник.0.2.4Компьютерная игра «крестики-нолики».0.2.5Подсистема работы с вкладками в веб-браузере.0.2.6Веб-сайт микроблога (например, Twitter).0.2.7Компиляторы gcc.0.2.8Игровой веб-сервер для игры в покер.Глава 1RAISE SpecificationLanguage (RSL)1.1Сигнатура модели с внутренним состояниемДля фиксации рассматриваемых в курсе моделей программ будемпользоваться языком спецификации RSL (Rigorous Approach to IndustrialSoftware Engineering Specification Language).

Сейчас рассмотрим синтаксис описания моделей в этом языке. Это описание должно содержатькак минимум список операций и список типов аргументов и типов результатов, для каждой операции должна быть указана сигнатура (имяоперации, список типов аргументов, список типов результатов операции).Описание модели без указания операций и типов:1scheme MODEL_NAME = c l a s s23endОписание операций и типов помещается между словами class и end.Описание типа очень простое:1scheme STACK = c l a s s234type Stacktype Element56end81.1.