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