MIPT-Coq-24-Lect-15

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: синтаксис и семантика императивного ЯП (продолжение); теоремы о детерминизме; спецификации программ; расширения языка операторами FOR и BREAK.