Hoare Logic | Какое постусловие действительно, когда существует бесконечный цикл?

Question

Мой учитель сказал мне, что следующее утверждение действительно: {x> 3} в то время как истина (x: = 3) {x = 3}

Почему это утверждение верно? Это потому, что постусловие никогда не проверяется, или же постусловие теперь будет считаться инвариантной проверкой?

Короче говоря: может ли пост-условие быть чем-либо, когда есть бесконечный цикл?

Тогда это будет действительно: {x> 3}, в то время как true (x: = 3) {x = 0}

Answer 1

Бесконечный цикл может иметь любое постусловие вообще (включая что-то совершенно глупое, например, 1 = 0), и это будет пусто верно. На самом деле, всегда ложное постусловие - это способ обеспечить невозможность выхода из цикла.