Доказательное программирование. Лекция 2

Продолжается рассмотрение формального доказательства корректности программ по отношению к ее пред и пост условию. Рассматривается предикатная семантика основных операторов языка программирования - выбора, составного оператора, оператора цикла while. Вводятся важные понятия инварианта и варианта цикла. Показано, как доказывается корректность и завершаемость программ с циклами. Приводятся примеры.