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

PD>Разумеется, но не об этом же речь, а о том, что в принципе может быть сделан тест, который вот этот вид ошибки обнаруживает. Иными словами, она должна проявиться в рантайме хоть когда-нибудь. Если она в рантайме не проявляется никогда — ошибка ли она ? Я уже это говорил, а Вы почему-то назвали это демагогией.
Потому и назвал, что это подмена тезиса.

PD>Ну это мне как-то сомнительно. Даже банальное s = h*w может вызвать ошибку при переполнении. Как можно сказать что тут нет ошибки ?
Очень просто. В теорем прувер загружается аксиоматика. Если у нас h и w — полноценные целые (Z), то никакого переполнения тут быть не может.
Если это — битвектора с дополнением до 2х, то у них другая аксиоматика и другие результаты.
Если это — знаковые целые из С++, то там третья аксиоматика.
В любом случае нас интересует не наличие либо отсутствие переполнения, а доказательство корректности. Если я утверждаю, что моя функция int avg(int a, int b) для любых a и b возвращает такое r, что выполняются аксиомы усреднения, то это и надо доказать. Не перебором "граничных значений" и не "покрытием кода", а прямо математически строго — тройки Хоара, дедуктивная верификация.
И там не очень важно, проверяю ли я наличие переполнения, или веду вычисления в увеличенной разрядности, или вычисляю a >> 2 + b >> 2 + ((a & b) | 1).

PD>Ну вот и докажите, что s = h*w содержит или не содержит ошибку. В статике, конечно, без выполнения.
Невозможно найти "ошибку" в коде, для которого нет спецификации. Может, у меня там uint h и uint w, c предусловием h < 100 && w << 100. Тогда никакой ошибки нет.
Или у меня по смыслу нужно делать wraparound — я выбираю слот в массиве из 256 хеш-корзинок на основании значения ключа h с шагом w.
Это примерно то же самое, что просить найти ошибку в a = 42.

PD>Возможно. Но звучит заманчиво. Хотя возможно, и нереализуемо.
Не понимаю, в чём заманчивость.

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

PD>Собственно, все исследовательские проекты так и выглядят. Надо бы сделать, чтобы получилось вот такое, а как это добиться — бог знает. Думайте сами.
Нет. Исследовательские проекты ставят гораздо более узкие задачи. И с ними прекрасно справляется ИИ.

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