Ну, про [не]существование спецструктуры было закрыто, что и будем выполнять.
По второму поднятому снова вопросу. Уточню кое-что - что, возможно, послужит к закрытию и этой темы. Метод программирования, использующий структуры Дейкстры (указанные Карповым) существует. Да, он называется методом Хоара. Поскольку именно Ч. Хоар (он же К. Хоор, как его Никлаус Вальтерович называет), основываясь на определении защищенных команд Дейкстрой (подозреваю, что это м.б. в работе "Взаимодействие последовательных процессов" 1966 года - но нужно уточнение) предложил дедуктивную семантику для сочинения по формальным спецификациям программ "с присваиваниями". Т.е. для императивного, тьюринго-машинного исполнителя. В отличие от разобранного Кауфманом чуть раньше метода Бэкуса - преследующего ту же цель, но для исполнителя "математически-функционального", без присваивания (точнее - с нелокальным изменением памяти). Надеюсь, что в формулировках не слишком отклонился от истины...
Что есть и заключение о существовании уже такого метода (со структурами, напомню, разобрались). Есть ли формулировка его сути ("понятия") по ссылке? Да, вот оно:
Кауфман в download/file.php?id=3171 на с. 334 писал(а):
Замечание. "Вылавливать" идеи циклов из написанных программ - довольно неблагодарная работа. Правильнее было бы формулировать инварианты при проектировании программы, а при доказательстве пользоваться заранее заготовленными инвариантами. Мы лишены возможности так действовать, потому что само понятие инварианта цикла появилось в наших рассуждениях лишь недавно.
А недавно пооявилось потому, что так курс Кауфмана построен - повествовательно.Ну, это всё лишь иллюстрация к топику данной темы. Однако отсюда можно извлечь и кое-что содержательное. Но это уже для других веток...