В компьютерных науках формальные спецификации — это математически обоснованные методы, цель которых — помочь в реализации систем и программного обеспечения. Они используются для описания системы, анализа ее поведения и помощи в ее разработке путем проверки ключевых свойств, представляющих интерес, с помощью строгих и эффективных инструментов рассуждений. [1] [2] Эти спецификации являются формальными в том смысле, что они имеют синтаксис, их семантика относится к одной области, и их можно использовать для получения полезной информации. [3]
С каждым прошедшим десятилетием компьютерные системы становятся все более мощными и, как следствие, все более влиятельными для общества. Из-за этого необходимы более совершенные методы, помогающие в разработке и внедрении надежного программного обеспечения. Устоявшиеся инженерные дисциплины используют математический анализ в качестве основы для создания и проверки дизайна продукта. Формальные спецификации являются одним из способов достижения такой надежности разработки программного обеспечения, как это когда-то предсказывалось. Другие методы, такие как тестирование , чаще используются для повышения качества кода. [1]
Имея такую спецификацию , можно использовать методы формальной проверки , чтобы продемонстрировать, что проект системы является правильным по отношению к ее спецификации. Это позволяет пересматривать неправильные конструкции системы до того, как будут сделаны какие-либо крупные инвестиции в фактическую реализацию. Другой подход заключается в использовании, вероятно, правильных шагов уточнения для преобразования спецификации в проект, который в конечном итоге преобразуется в правильную по построению реализацию .
Важно отметить, что формальная спецификация не является реализацией, а скорее может использоваться для разработки реализации . Формальные спецификации описывают , что должна делать система, а не то, как она должна это делать.
Хорошая спецификация должна иметь некоторые из следующих атрибутов: адекватная, внутренне непротиворечивая, недвусмысленная, полная, удовлетворительная, минимальная [3] .
Одна из основных причин интереса к формальным спецификациям заключается в том, что они дают возможность выполнять доказательства программных реализаций. [2] Эти доказательства могут использоваться для проверки спецификации, проверки правильности дизайна или для доказательства того, что программа удовлетворяет спецификации. [2]