Сегодня поговорим о том, зачем нужна формальная верификация, как ей пользоваться и чем это лучше тестов. Начнем с определения, формальная верификация - это процесс доказательства того, что программа или система удовлетворяет заданным требованиям. Иногда еще добавляют, что с помощью мат методов. Уже исходя из этого определения, можно легко заметить главное преимущество перед тестами. А именно то, что формальная верификация ставит своей задачей доказать, а не проверить работоспособность. Тесты же именно проверяют работоспособность. К примеру, имеется функция trim, которая обрезает пробелы(или переданные символы) в начале и конце строки(это фактически описание из документации), только вот проблема, пробелы она обрезает не все. По факту есть просто набор из 6 символом, которые передаются вторым параметром по умолчанию, и в них отсутствуют некоторые пробельные символы, что уже отчасти противоречит спецификации. И если мы начнем писать для нее тесты, то данную ошибку тупо не обнаружим, пока не обратимся к таблице всех возможных проблемных символов. Потому что здесь имеет место проблема тех самых крайних случаев, о существовании которых мы просто не подозреваем. А не подозреваем мы о них из-за формулировки, ведь есть огромная разница в восприятии «удалить пробелы» и «удалить все символы принадлежащие множеству пробельных символов кодировки X». Уже на этапе формулировки задачи приходится думать по другому. А что входит в это множество, а как мне его выразить в программе, а что потенциально делать с другими кодировками? Про один из вариантов, как перейти к такому образу постановки, я как раз рассказывал в рамках доклада на LivePHP. И вот в этом есть одна из прелестей формальной верификации, пока мы думаем, как нам это доказать, мы параллельно думаем о том, а что мы вообще доказываем. Что фраза «удаление пробелов» означает на самом деле. И это уточнение невероятно полезно в текущей реальности, где код уже по большей часи генерируется, а не пишется руками. Когда же все уточнено, определено и выражено, тогда и только тогда можно переходить к доказательству. Доказывать можно по разному, но в большинстве случаев это будет чистая математика(сначала с множествами, потом можно перескочить на группы, затем на Hott), где используя базовые теоремы и составляя свои, вы будете постепенно выстраивать мат модель своей программы. Имея на руках мат модель, можно точно предсказывать поведение системы, планировать изменения так, что бы ничего не сломать, буквально знать все слабые места программы. Ничего из этого нам не даст ни один из видом тестирования. А вот о том, чем же можно формально верифицировать программы, мы поговорим уже в следующем посте.