Интернет магазин китайских планшетных компьютеров

Компьютеры - Формальные методы - Использование формальных методов

Формальные методы применяются на разных этапах цикла разработки программного обеспечения:

Спецификация

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

Разработка

Если формальная спецификация использует операциональную семантику, наблюдаемое поведение конкретной системы можно сравнивать с ожидаемым, потому что такая семантика может быть выполнимой, а может даже использоваться для автоматического генерирования кода. Если используется аксиоматическая семантика, то предусловия и постусловия могут напрямую отобразиться в утверждения в выполнимом коде.

Верификация

Когда формальная спецификация подготовлена, её можно использовать для доказательства требуемых свойств. Верификация бывает дедуктивной и модельной: дедуктивная использует автоматическое доказательство теорем или специфические алгебры, а модельная основывает свои выводы не на самой системе, а на построенной по ней модели. При этом модель совершенно не обязательно строить вручную, если применимы оказываются техники вроде программного сечения .