Здравствуйте, Pavel Dvorkin, Вы писали:

PD>Что такое полноценные целые ? Google мне в поиске почему-то ничего о них не сказал.
Множество Z: https://ru.wikipedia.org/wiki/%D0%A6%D0%B5%D0%BB%D0%BE%D0%B5_%D1%87%D0%B8%D1%81%D0%BB%D0%BE

PD>Меня интересует именно возможность переполнения. Это ширина и высота прямоугольника и площадь его соответственно. Тип — uint. Ограничения на h и w — не более 100000, допустим. Других данных у меня нет. Если оно будет , то все последующие действия накроются медным тазом. Вот и скажите, как определить статическим анализом его возможность или невозможность в этом случае. Без рассуждений об аксиоматике и каких-либо дополнительных требованиях — повторяю. у меня больше ничего нет.
Переполнение — это когда результат произведения в uint отличается от результата "настоящего" произведения.
Это даёт нам два возможных способа записи постусловия:
— сравнением результата с честным произведением бесконечноразрядных целых
— сравнением результата с произведением в удвоенной битности.
Как только мы записали предусловие, постусловие, и сформулированы критерии верификации, любой SAT/SMT солвер вам сразу найдёт контрпример.