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

PD>>Ну это мне как-то сомнительно. Даже банальное s = h*w может вызвать ошибку при переполнении. Как можно сказать что тут нет ошибки ?
S>Очень просто. В теорем прувер загружается аксиоматика. Если у нас h и w — полноценные целые (Z), то никакого переполнения тут быть не может.

Что такое полноценные целые ? Google мне в поиске почему-то ничего о них не сказал.

S>Если это — битвектора с дополнением до 2х, то у них другая аксиоматика и другие результаты.
S>Если это — знаковые целые из С++, то там третья аксиоматика.
S>В любом случае нас интересует не наличие либо отсутствие переполнения, а доказательство корректности. Если я утверждаю, что моя функция int avg(int a, int b) для любых a и b возвращает такое r, что выполняются аксиомы усреднения, то это и надо доказать. Не перебором "граничных значений" и не "покрытием кода", а прямо математически строго — тройки Хоара, дедуктивная верификация.
S>И там не очень важно, проверяю ли я наличие переполнения, или веду вычисления в увеличенной разрядности, или вычисляю a >> 2 + b >> 2 + ((a & b) | 1).

PD>>Ну вот и докажите, что s = h*w содержит или не содержит ошибку. В статике, конечно, без выполнения.
S>Невозможно найти "ошибку" в коде, для которого нет спецификации. Может, у меня там uint h и uint w, c предусловием h < 100 && w << 100. Тогда никакой ошибки нет.

Меня интересует именно возможность переполнения. Это ширина и высота прямоугольника и площадь его соответственно. Тип — uint. Ограничения на h и w — не более 100000, допустим. Других данных у меня нет. Если оно будет , то все последующие действия накроются медным тазом. Вот и скажите, как определить статическим анализом его возможность или невозможность в этом случае. Без рассуждений об аксиоматике и каких-либо дополнительных требованиях — повторяю. у меня больше ничего нет.

PD>>А вот человеку можно и первое поручить. Не джуну, конечно, а хорошему специалисту, а то и команде их с участием специалистов разного профиля. Именно так задачу и поставить. "Измените код так, чтобы у нас продажи выросли в два раза без роста затрат на саппорт". На вопрос — а что именно сделать, дать ответ — думайте сами. Все.
S>Вы сами-то так пробовали делать? Или это опять фантазии про ребёнка, который обучается отличать котиков от собачек по 1 фотографии?

Вот это как раз демагогия и есть. Я же привел ниже пример, когда мне самому именно так задачу и поставили.


PD>>Я в таком проекте работал 3 года в начале 2000-х. Потоковая обработка фотографий, на каждое фото дается фиксированное время, не уложитесь — обработка этого фото снимается и выписывается penalty. При обработке фото делаются запросы к БД, не SQL, специальной БД, сделанной под эту задачу от какой-то фирмы. У нас все есть, и все работает, но время запросов слишком большое, а поэтому слишком много penalty. Сделайте, чтобы работало быстрее. Это вся постановка задачи. На мое предложение провести реверс-инжиниринг этой БД и посмотреть, что там делается, был получен категорический запрет — нарушает лицензионное соглашение.
PD>>Вот и все. Делайте, что хотите, для этого мы Вас сюда и взяли.
S>Вот такие задачи прекрасно решаются ИИ. Потому что это не про рост прибыли, а про конкретную, маленькую, узкоспециализированную задачу.
S>Там всё пространство решений — с гулькин хрен.
S>Более того, скорее всего кто-то в мире уже решал или такую же задачу, или очень похожую, и уже есть ряд решений, наработанных для подобных задач. ИИ позволяет быстренько спрототипировать десяток-другой идей, отбросить неудачные, и выбрать удачные.

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