Мой учитель сказал мне, что следующее утверждение верно: {x > 3}, тогда как верно (x := 3) {x = 3}
Почему это утверждение справедливо? Это потому, что пост-условие никогда не проверяется, или пост-условие теперь будет считаться инвариантной проверкой?
Короче говоря, может ли постусловие быть чем угодно, если есть бесконечный цикл?
Тогда это будет действительным: {x > 3}, а true (x := 3) {x = 0}
