Z notation — средство функциональной декомпозиции и спецификации программ. Ему около 30 лет.

Во многие ФЯ переносится один-в-один.

Это чтобы поменьше говорили об отсутствии методов декомпозиции для ФП.

Две ссылки на обозрение применения формальных методов в индустрии ПО:
An International Survey of Industrial Applications of Formal Methods: Volume 1 Purpose, Approach, Analysis, and Conclusions (1993)
An International Survey of Industrial Applications of Formal Methods Volume 2 Case Studies (1993)

(Ссылки ведут на CiteSeer, он иногда бывает недоступен. Есть названия статей, их можно отыскать на его зеркалах.)

Чем интересно это обозрение: приводится компания, в ней указывается место применения ФМ, область применения (и команда, и тип разрабатываемого ПО или комплекса) и даны общие характеристики результатов применения, в которые входят и влияние на время разработки, и на общую стоимость — что важно.

Многие ФМ применялись вместе с ОО языками. Например, Z notation была применена вместе со Smalltalk в фирме Tektronix.

В качестве бонуса — про исключения (и shameless plug — но по необходимости, ибо в Google слетела кодировка):
Ссылка на письмо в SU.SOFTW про семантику GOTO в Vienna Development Method. Она совпадает с семантикой исключений.

Exceptions considered harmful!