|
Сейчас разбираюсь в User Interface функционального языка Factor. Много функций, определённых взаимной рекурсией. Распутываю клубок змей, ищу хвосты. Возникает острая необходимость как-то записывать то, что понял, чтобы не забыть и передать другим. Хочется писать содержательную "спецификацию", что должна делать программа, затем уже писать код и потом при сильном желании доказывать, что код делает то, что должен согласно спецификации. Есть язык TLA+, придуманный Лэмпортом и разные "исчисления процессов" (pi-calculus, CSP Хоара, ещё что-то). Кто-нибудь пробовал?
|