Документирование процесса разработки ПО

https://www.researchgate.net/publication/367463805

1)
Взлет - посадка по LaTex-у.
2)
Полезные виды UML (блок-схема, схема реляционных связей
схема потоков данных, состояние автомата, схема наследования)
примеры состояний автомата для некоторых окон
оконного приложения
(главное окно, окно ввода данных, окно сообщения да-нет)
3)
RSL -- RAISE SPECIFICATION LANGUAGE, язык формальных спецификаций.
Его спел-чекер (раздел 2.6 Утилита RSLTC – не только проверка синтаксиса)

со ссылками на первоисточник
Introduction to RAISE
http://www.sel.unsl.edu.ar/ApuntesMaes/Anteriores/RAISE/Apunte_ChrisGeorge/report249.pdf

https://raisetools.github.io/material/documentation/raise-language.pdf

и
методички МГУ
Практикум по формальной спецификации программ на языке RSL
http://www.sp.cs.msu.ru/courses/progs2001/special/formspec01.pdf

В первоисточнике упоминается возможность проверки
правильности реализации спецификации, но отсутствует ascii - символ,
как писать выражение. :)) Называется проверка теории.
Отдаленный аналог для Си -- это хедер (абстрактная спецификация)
и сами функции (конкретная спецификация) -- сишный компилятор проверяет
прототипы функций.

В мгушной методички этого нет вообще.

тут в Документирование процесса разработки ПО
https://www.researchgate.net/publication/367463805

есть как это делать.
Пример в аттаче

Спецификация a1 реализует (уточняет) спецификацию a0