Теормин-ФСВП

Формальная спецификация —это математическое описание программной или аппаратной системы, которая можетбыть реализована в соответствии с этим описанием. Специфицируется, что должнаделать система, но не то, как она должна это делать. Если существует спецификациясистемы, возможно применить методы формальной верификации, чтобыпродемонстрировать, что система удовлетворяет (или будет удовлетворять)спецификации. Таким образом, можно проверить, будет ли конкретнаяспроектированная модель удовлетворять требованиям после реализации.Если верификация ПО исследует соответствие программы спецификации,то валидация исследует соответствие программы или спецификациитребованиям пользователя.Формальная верификация — формальное доказательство соответствия илинесоответствия формального предмета верификации его формальному описанию.Предметом выступают алгоритмы, программы и другие доказательства.Тестирование программного обеспечения не может доказать, что система, алгоритмили программа не содержит никаких ошибок и дефектов и удовлетворяетопределённому свойству.

Это может сделать формальная верификация.Формальная верификация может использоваться для проверки таких систем, какпрограммное обеспечение, представленное в виде исходныхтекстов, криптографические протоколы, комбинаторные логические схемы, цифровыесхемы с внутренней памятью.Верификация представляет собой формальное доказательство на абстрактнойматематической модели системы, в предположении о том, что соответствие междуматематической моделью и природой системы считается изначально заданным.Например, по построению модели либо математического анализа и доказательстваправильности алгоритмов и программ.Примерами математических объектов, часто используемых для моделирования иформальной верификации программ и систем являются:формальная семантика языков программирования, например операционнаясемантика, денотационная семантика, аксиоматическая семантика (логика Хоара),[математическая семантика программ].конечный автоматпомеченная модель состояний и переходовсеть Петривременной автоматгибридный автоматисчисление процессовструктурированные алгоритмыструктурированные программыСуществуют следующие подходы к формальной верификации:формальная семантика языков программированияпроверка моделей (model checking)логический вывод (logical inference)cимвольное выполнение (symbolic execution)абстрактная интерпретация (abstract interpretation)систематический анализ алгоритмов и программтехнологии доказательного программированияДоказательное программирование — использовавшаяся в 1980-х годах вакадемических кругах технология разработки программ для ЭВМ с доказательствамиправильности — доказательствами отсутствия ошибок в программах (понимая, врамках данной теории, ошибки как несоответствия между программой и реализуемымею алгоритмом).Автоматическая проверка доказательстваДоказательство может быть автоматизировано полностью лишь для оченьнебольшого круга простых теорий, поэтому важное значение получает егоавтоматическая проверка и для этого преобразование к проверяемому виду.Для поддержания строгости при проверке доказательства верификатором следуетпроверить ещё и верификатор, для чего нужен ещё один верификатор и так далее.Получившуюся бесконечную цепь верификаторов можно было бы свернуть, построивверифицирующий себя верификатор, обладающий способностью развернуться доприменимого на практике.Проверка моделей (проверка на модели, англ.

model checking) — методавтоматической формальной верификации параллельных систем с конечным числомсостояний. Позволяет проверить удовлетворяет ли заданная модель системыформальным спецификациям.В качестве модели обычно используется, так называемая, модель Крипке, котораяформально задаётся следующим образом:, где S — множествосостояний, S0 — множество начальных состояний,— отношениепереходов,— функция разметки.Обычно спецификации задаются на языке формальной логики. Для спецификацииаппаратного и программного обеспечения, как правило, применяют темпоральнуюлогику — специальный язык, позволяющий описывать поведение системы во времени.Важным вопросом спецификации является полнота.

Метод проверки на моделипозволяет убедиться, что модель проектируемой системы соответствует заданнойспецификации, однако определить, охватывает ли заданная спецификация всесвойства, которым должна удовлетворять система, невозможно.Основная трудность, которую приходится преодолевать в ходе проверки на модели,связана с эффектом комбинаторного взрыва в пространстве состояний. Эта проблемавозникает в системах, состоящих из многих компонентов, взаимодействующих друг сдругом, а также в системах, обладающих структурами данных, способных приниматьбольшое число значений.Принцип подстановки Барбары Лисков ( Liskov Substitution Principle, LSP)в объектно-ориентированном программировании является специфичнымопределением подтипа.Пусть q(x) является свойством, верным относительно объектов x некотороготипа T.

Тогда q(y) также должно быть верным для объектов y типа S, где Sявляется подтипом типа T.Роберт С. Мартин определил[3] этот принцип так:Функции которые используют базовый тип должны иметь возможностьиспользовать подтипы базового типа не зная об этом.Таким образом, идея Лисков о «подтипе» даёт определение понятия замещения —если S является подтипом T, тогда объекты типа T в программе могут быть замещеныобъектами типа S без каких либо изменений желательных свойств этой программы(например, корректность).Этот принцип является важнейшим критерием для оценки качества принимаемыхрешений при построении иерархий наследования.Принцип подстановки (замещения) Лисков имеет близкое отношение кметодологии проектирования по контракту, и ведет к некоторым ограничениям на то,как контракты могут взаимодействовать с наследованием: Предусловия не могут быть усилены в подклассе. Постусловия не могут быть ослаблены в подклассе.Также, принцип LSP подразумевает, что методы подкласса не могут генерироватьникаких дополнительных исключений, кроме тех, которые сами являютсяподклассами исключений, генерируемых методами надкласса.Контрактное программирование (Design by Contract (DbC), или Programming byContract) — это метод проектирования программного обеспечения.

Он предполагает,что проектировщик должен определить формальные, точные и верифицируемыеспецификации интерфейсов для компонентов системы. При этом, кроме обычногоопределенияабстрактных типов данных, такжеиспользуются предусловия, постусловия и инварианты. Данные спецификацииназываются "контрактами" в соответствии с концептуальной метафорой условий иответственностей в бизнес-контрактах.Контрактное программирование выросло из формальной верификации, формальнойспецификации и логики Хоара. Условия, облегчающие применение контрактногопрограммирования:наличие наследования и возможность динамического связывания,способность обрабатывать исключения,возможность автоматической документации ПО.Основная идея контрактного программирования — это модель взаимодействияэлементов программной системы, основывающаяся на идее взаимных обязательств ипреимуществ. Как и в бизнесе, клиент и поставщик действуют в соответствии сопределённым контрактом.

Контракт некоторого метода или функции можетвключать в себя:конкретные обязательства, которые любой клиентский модуль долженвыполнить перед вызовом метода — предусловия, которые дают преимуществодля поставщика — он может не проверять выполнение предусловий;конкретные свойства, которые должны присутствовать после выполненияметода — постусловия, которые входят в обязательства поставщика;обязательства по выполнению конкретных свойств — инвариантов, которыедолжны выполняться при получении поставщиком сообщения, а также при выходеиз метода.онтрактное программирование подразумевает эти требования критическими длякорректности программ, поэтому они должны быть утверждены при проектировании.Таким образом, контрактное программирование предписывает начинать писать код снаписания формальных утверждений корректности (assertions).В объектно-ориентированном программировании контракт метода обычно включаетследующую информацию:возможные типы входных данных и их значение;типы возвращаемых данных и их значение;условия возникновения исключений, их типы и значения;присутствие побочного эффекта метода;предусловия, которые могут быть ослаблены (но не усилены) в подклассах;постусловия, которые могут быть усилены (но не ослаблены) в подклассах;инварианты, которые могут быть усилены (но не ослаблены) в подклассах;(иногда) гарантии производительности, например, временнаясложность или сложность по памяти.Контрактное программирование может повысить уровень повторного использованиякода, поскольку обязательства модуля чётко документированы.

Вообще, контрактмодуля можно рассматривать также как способ документации программногообеспечения.DafnyDafny is a language that is designed to make it easy to write correct code. This meanscorrect in the sense of not having any runtime errors, but also correct in actually doing whatthe programmer intended it to do.