В информатике формальные спецификации — это математически обоснованные методы, целью которых является помощь в реализации систем и программного обеспечения. Они используются для описания системы, анализа ее поведения и помощи в ее проектировании путем проверки ключевых свойств, представляющих интерес, с помощью строгих и эффективных инструментов рассуждения. [1] [2] Эти спецификации формальны в том смысле, что они имеют синтаксис, их семантика находится в пределах одной области, и их можно использовать для получения полезной информации. [3]
С каждым десятилетием компьютерные системы становятся все более мощными и, как следствие, оказывают все большее влияние на общество. По этой причине необходимы более совершенные методы, помогающие в разработке и внедрении надежного программного обеспечения. Признанные инженерные дисциплины используют математический анализ в качестве основы для создания и проверки конструкции продукта. Формальные спецификации являются одним из способов достижения этой надежности в разработке программного обеспечения, как когда-то предсказывалось. Другие методы, такие как тестирование , чаще используются для повышения качества кода. [1]
Учитывая такую спецификацию , можно использовать формальные методы проверки, чтобы продемонстрировать, что проект системы верен с точки зрения его спецификации. Это позволяет пересмотреть неправильные конструкции системы до того, как будут сделаны какие-либо крупные инвестиции в фактическую реализацию. Другой подход заключается в использовании вероятно правильных шагов уточнения для преобразования спецификации в проект, который в конечном итоге преобразуется в правильную по конструкции реализацию .
Важно отметить, что формальная спецификация не является реализацией, а скорее может использоваться для разработки реализации . Формальные спецификации описывают , что должна делать система, а не то, как она должна это делать.
Хорошая спецификация должна обладать некоторыми из следующих атрибутов: адекватная, внутренне непротиворечивая, однозначная, полная, удовлетворяющая, минимальная [3].
Хорошая спецификация будет иметь: [3]
Одна из основных причин интереса к формальным спецификациям заключается в том, что они обеспечивают возможность проверки реализаций программного обеспечения. [2] Эти доказательства могут использоваться для проверки спецификации, проверки правильности проекта или для доказательства того, что программа удовлетворяет спецификации. [2]
Проект (или реализация) никогда не может быть объявлен «правильным» сам по себе. Оно может быть только «правильным по отношению к заданной спецификации». Правильно ли формальная спецификация описывает решаемую задачу – это отдельный вопрос. Это также трудный вопрос для решения, поскольку в конечном итоге он касается проблемы построения абстрактных формальных представлений неформальной конкретной проблемной области , и такой шаг абстракции не поддается формальному доказательству. Однако можно подтвердить достоверность спецификации, доказав «проблемные» теоремы , касающиеся свойств, которые, как ожидается, будет демонстрировать спецификация. Если они верны, эти теоремы укрепляют понимание спецификатором спецификации и ее связи с базовой проблемной областью. Если нет, то спецификацию, вероятно, необходимо изменить, чтобы лучше отражать понимание предметной области теми, кто участвует в разработке (и реализации) спецификации.
Формальные методы разработки программного обеспечения не получили широкого распространения в промышленности. Большинство компаний не считают экономически эффективным применять их в процессах разработки программного обеспечения. [4] Это может происходить по разным причинам, вот некоторые из них:
Другие ограничения: [3]
Методы формальной спецификации уже довольно давно существуют в различных областях и в различных масштабах. [6] Реализации формальных спецификаций будут различаться в зависимости от того, какую систему они пытаются моделировать, как они применяются и на каком этапе жизненного цикла программного обеспечения они были введены. [2] Эти типы моделей можно разделить на следующие парадигмы спецификации:
В дополнение к вышеперечисленным парадигмам существуют способы применения определенных эвристик, которые помогут улучшить создание этих спецификаций. В упомянутой здесь статье лучше всего обсуждаются эвристики, которые следует использовать при разработке спецификации. [6] Они делают это, применяя подход «разделяй и властвуй» .
Нотация Z является примером ведущего языка формальных спецификаций . Другие включают язык спецификации (VDM-SL) Венского метода разработки и абстрактную машинную нотацию (AMN) B-метода . В области веб-сервисов формальная спецификация часто используется для описания нефункциональных свойств [7] ( качество обслуживания веб-сервисов ).
Вот некоторые инструменты: [4]
