Specification-Driven Development (строительство по чертежу)

На пальцах

Представь, что инженер строит мост. До того как положить первый кирпич, у него на столе лежит подробный чертёж: какие опоры, какой пролёт, какую нагрузку выдержит. Строители не придумывают мост на ходу — они идут по чертежу. Specification-Driven Development — это то же самое в программировании: до написания кода составляется формальная спецификация, точное описание того, что программа должна делать и чего не должна. Код потом сверяется с этой спецификацией.

Что это

Метод разработки, в котором сначала создаётся формальная спецификация поведения системы — на специальном языке вроде Alloy, TLA+ или с помощью типов в языках вроде Idris или Lean, — а затем код пишется так, чтобы ей соответствовать. Спецификация — это контракт: система обязана делать одно и не делать другого.

Зачем

Например, у интернет-магазина есть корзина, оплата и склад. Без формальной спецификации разработчики могут по-разному понимать требования: «что значит списать товар?» — кто-то делает списание при клике «в корзину», кто-то — только при оплате. В итоге в системе появляются дыры: деньги списываются дважды, товар резервируется у двух покупателей одновременно. SDD заставляет всех опираться на одну точную спецификацию: код либо ей соответствует, либо нет — спорить не о чем.

Ещё SDD умеет:

• находить ошибки в требованиях ещё до написания кода (через формальную проверку модели)
• служить документацией, которая не расходится с кодом
• помогать при переписывании системы — есть точная цель, к которой идёшь
• применяться там, где цена ошибки высока: банкинг, авиация, криптография, сетевые протоколы