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

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

А можно сказать все же, без "теоретических" соображений, что мне выдаст хоть статический верификатор , хоть ИИ на программу

void main()
{
unsigned int l,w,s;
sscanf("%d %d", &l, &w);
s = w * h;
printf("%d", s);
}

А то ведь у меня ничего, кроме этой программы, и нет.

Или я должен к каждой операции умножения приделать предусловие и постусловие в виде честного произведения бесконечноразрядных целых или же вычисления в unsigned long и сравнения ?

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

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

А можно сказать все же, без "теоретических" соображений, что мне выдаст хоть статический верификатор , хоть ИИ на программу

void main()
{
unsigned int l,w,s;
sscanf("%d %d", &l, &w);
s = w * l;
printf("%d", s);
}

А то ведь у меня ничего, кроме этой программы, и нет.

Или я должен к каждой операции умножения приделать предусловие и постусловие в виде честного произведения бесконечноразрядных целых или же вычисления в unsigned long и сравнения ?