Для чего нужна часть курса ФСВП о спецификации

must read всем сомневающимся!

Возможно, не все понимают, зачем нужна первая часть нашего курса - та, в которой речь идет о формальной спецификации. Эта часть курса оправдана тем, что сейчас в практике программирования не редкостью является требование тщательной верификации кода (речь идет о верификации в широком смысле, тут и аналитическая верификация, и ручная экспертиза, и тестирование).


Курс затрагивает моменты, связанные лишь с верификацией выполнения *функциональных* требований. В общих чертах, вы уже себе представляете различные методы верификации. Но сейчас для нас важно то, что это должна быть именно тщательная, не упускающая важных особенностей, по возможности полная верификация. Без чего невозможно как оценить полноту уже сделанной работы (и, соответственно, дать оценку усилий, которые необходимы для завершения верификации), так и провести верификацию? Без чёткого представления проверяемой функциональности. Представьте, что вы пишете тесты "просто так", чтобы "что-то тестировалось" - тестирование с такими тестами вряд ли можно считать тщательным. Или  вы пишете тесты, не имея "схемы всех случаев", в которых поведение программы обладает рядом особенностей. Тесты, конечно, будут написаны, тестирование будет проведено. И, возможно, будут найдены ошибки. Или не найдены. Но дать уверенность, что это тестирование тщательное, будет опрометчивым.

Понимая изложенные выше проблемы и упор на тщательную верификацию, первая часть курса ФСВП нацеливается на выработку понимания, что значит чётко (формально) описать функциональность программы, какие существуют техники такого четкого описания. Один из подходов - это описание свойств, свойств функционирования программ. Иными словами, первая часть курса - о том, как задавать свойства программ, как сказать, какой должна быть правильная программа, выполняющая определенные задачи для пользователя, формальным образом. Чтобы заданные таким образом свойства становились отправной точкой и стержнем для тщательной верификации программ.

Курс не ставит своей целью описать свойства большого класса программ. Речь идет лишь о тех программах, работу которых можно представить как работу некого "устройства". Устройство принимает входные воздействия, возможно, выдает некоторую реакцию на воздействие. Модель вполне привычная: пользователь выполняет операции и получает их результаты. Пример устройства: БД, пример входных воздействий на БД:

• положить в БД данные
• удалить из БД данные (предположим, эти два воздействия не дают реакции, т.е. ничего не сообщают пользователю БД, например, БД просто принимает "в себя" данные и молчит, ждет следующей операции)
• выполнить проверку наличия данных (а на это воздействие БД должна "среагировать" с определенным внешним эффектом - пользователь получит информацию от БД, есть там запрашиваемые данные или нет).

Итак, про каждую *операцию* можно сказать, что она обладает

• именем
• аргументами
• возможно, изменением внутреннего состояния устройства
• возможно, *внешним эффектом*.

При этом само устройство внутри себя может быть реализовано довольно сложно. Или даже таких устройств может быть несколько, каждое устройство будет обладать своими *нефункциональными* характеристиками (объемом занимаемой памяти, скоростью выполнения операций и т.п.).

Еще пример: менеджер динамической памяти. У него ("над ним") есть, как минимум, две операции:

• аллоцировать память; аргумент - размер памяти, которую нужно аллоцировать; внешний эффект - адрес памяти или сообщение о невозможности аллоцировать память требуемого размера;
• деаллоцировать память; аргумент - адрес памяти, которая была ранее аллоцирована первой операцией; внешний эффект - сообщение об успехе деаллоцирования памяти или сообщение о неуспехе деаллоцирования памяти.

(продолжение следует)