Программирование


Ответить в тред Ответить в тред

Check this out!
<<
Назад | Вниз | Каталог | Обновить тред | Автообновление
68 6 33

Формальное доказательство эквивалентности программ Аноним 02/12/19 Пнд 21:07:54 15361601
image.png (383Кб, 419x590)
419x590
Есть две программы на разных языках, обе реализуют один и тот же алгоритм. Как формально доказать, что для всех возможных входных данных они возвращают одинаковый результат? Очевидно, что с юнит-тестами тут облом. Это вообще возможно?

pic random
Аноним 02/12/19 Пнд 21:13:04 15361662
ты изначально подумай, как доказать полную корректность хоть 1 программы?

спойлер - формальная верификация. Вот если сделаешь это хоть для одной, для второй сделай так же
Аноним 02/12/19 Пнд 21:14:21 15361703
>>1536160 (OP)
Скрыл. Сейчас набежит петушня с пруверами.
Аноним 02/12/19 Пнд 21:27:51 15361794
>>1536170
На дваче таких вумников нет.
мимо непонятно зачем потратил 2 месяца своей жизни на метаматематику и SF
Аноним 02/12/19 Пнд 21:29:07 15361815
>>1536166
>спойлер - формальная верификация
Да знаю я, Агда-хуягда. Меня конкретика интересует, хотя бы на примере хелловорлд.
Аноним 02/12/19 Пнд 21:31:15 15361826
>>1536181
если у тебя вариативность инпута ограничена - то брутфорс, иначе к матанопетухам
Аноним 02/12/19 Пнд 21:33:47 15361837
>>1536182
>иначе к матанопетухам
Тут есть такие? Или все джависты ржаные-гречневые?
Аноним 02/12/19 Пнд 21:37:04 15361858
>>1536183
Зачем тебе это? Если ты не вонабиматематик с мехмата - формально верифицировать программы тебе никто не даст. Это вход для избранных.
Аноним 02/12/19 Пнд 21:38:35 15361879
>>1536185
Да хорош мозги ебать, это /зк или где? Есть конкретная прикладная задача, нужно не обосраться с новой версией программы.
Аноним 02/12/19 Пнд 23:00:29 153624110
>>1536187
Ну можешь поиграть с трансформацией. Мол задаёшь эквивалентные структуры и сравниваешь.
Если твои яп не поддерживают что-то такое из коробки то ты соснешь ибо сложно.
Я так понимаю доступный для тебя способ верификации это банальные тесты.
В чем проблема?

В мёд исследованиях используют например метод двойной проверки, когда 2 программиста независимо пишут программу а потом сверяют результат.
У тебя нечто ответсвеннее медицинских исследований?
Аноним 02/12/19 Пнд 23:05:14 153624911
>>1536241
>В чем проблема?
в том, что ты можешь написать хоть 1000 тестов, а на 1001-м появится разница в результатах, или на 100001-м, ну ты понел
Аноним 02/12/19 Пнд 23:06:31 153625012
>>1536241
> метод двойной проверки, когда 2 программиста независимо пишут программу а потом сверяют результат
есть, где об этом можно почитать? с исследованиями, хуе-мое
Аноним 02/12/19 Пнд 23:41:14 153626913
блять, вы тут все веб-макаки что ли?
Аноним 02/12/19 Пнд 23:51:47 153627514
>>1536269
Просто никто тут не мается такой далёкой от реальности хуитой, не имеющей никакого практического применения. Впрочем, кого я обманываю.
Аноним 03/12/19 Втр 09:26:51 153635515
15743015743090.png (283Кб, 586x634)
586x634
Если программы на разных яп, плохо дело. Чисто теоретически, если оба эти яп конпелируются в llvm, то стоит копать в сторону Coq + Vellvm/Crellvm. Агды хуягды сразу мимо, потому что такая задача требует для решения не только формализации яп, но и формализации самих анализируемых программ в виде элементов логики разделения (separation logic), а для агды все это придется писать самому, лол. В коке хотя бы что-то уже есть, хотя все равно придется дописывать. Я бы с такой задачей вообще связываться не стал, если речь не идёт о больших бабках.
Аноним 03/12/19 Втр 10:04:53 153637016
>>1536241
> Ну можешь поиграть с трансформацией. Мол задаёшь эквивалентные структуры и сравниваешь.
> Если твои яп не поддерживают что-то такое из коробки то ты соснешь ибо сложно.
А пример такого можно? В каких языках это есть?
Аноним 03/12/19 Втр 21:00:42 153701817
>>1536187
Для этого и существуют юнит-тесты. Старое зеленое, новое зеленое - значит работает. Недокументированные баги или непокрытый тестами случай - ну бывает, щито поделать.
Аноним 03/12/19 Втр 21:08:55 153703118
>>1537018
> ну бывает
Вот это ОПа и не устраивает, он хочет идеальную программу, которая гарантированно не имеет вообще ни одного бага. С такими спорить бесполезно.
Аноним 03/12/19 Втр 21:10:20 153703319
>>1537018
>значит работает
Нихуя это не значит. Точнее, значит, что работает вот именно с этими данными, которые ты в тестах нахуярил.

>>1537031
>которая гарантированно не имеет вообще ни одного бага
Ты тупой? Нужна программа, которая работает так же как и старая. Ты читать вообще умеешь, макака ебаная?
Аноним 03/12/19 Втр 21:14:49 153703820
>>1537033
А стоит это затрат времени и сил на "гарантированно 100% копию программы"? Хорошо составленные юнит-тесты покроют тебе 99.9999% всех случаев, данные они ж не с балды, они обычно подчиняются какому-то закону, плюс краевые случаи там, тыры-пыры. Ну и представь, что исходная программа не идеальна, там где-то будет деление на ноль например при определенном входе. Тебе это тоже надо воспроизвести?
Аноним 03/12/19 Втр 21:20:18 153704021
>>1537038
Тест как-то помогают, да, но это какая-то поебень в 2019 году, неужели ничего нормального не придумали? Это как решать квадратное уравнение, пробуя брутфорсом разные значения, авось что подойдет. Пиздец.
Аноним 03/12/19 Втр 21:23:43 153704222
>>1537040
Скоро будут тебе квантовые вычисления, может будет профессия "квантовый тестировщик". А пока лучшее что ты можешь сделать не влезая в какой-то адский матан - полный брут на кластере из GPU.
Аноним 03/12/19 Втр 21:26:18 153704523
>>1537042
>адский матан
Так посоветуй матан, епт. Может, там уже все придумали, а вы до сих пор свои тестики дрочите. Блять, почему у вас раздел такое говно?
Аноним 05/12/19 Чтв 13:07:30 153813224
>>1537045

Ты какой-то тугодум, всё уже тебе объяснили.
Аноним 05/12/19 Чтв 15:04:36 153825125
Аноним 05/12/19 Чтв 16:46:53 153835826
>>1536160 (OP)
"Доказать" в математическом понимании невозможно, потому что вне математики ты вообще хуй что-то докажешь, программы не исключение. Если тебе нужно подтверждение работы программы в практическом смысле, то два стула:
1) Классические black-box юнит-тесты, если набор ожидаемых входных-выходных данных в алгоритме не слишком широкий и их в принципе можно засунуть в десяток тестов и не ебать себе мозги
2) Тесты имплементации, когда ты прокидываешь между тестом и внутренностями алгоритма интерфейс и по шагам верифицируешь, что алгоритм выполняется как надо(выставляет на каждом шаге нужное значение и т.п). Обычно не стоит того, но со сложными алгоритмами это единственный способ их протестировать на 100%. https://blog.cleancoder.com/uncle-bob/2017/01/09/DiamondSquare.html
Аноним 05/12/19 Чтв 16:54:31 153836027
>>1538358
Доказать-то можно. Программирование строится на информатике и алгоритмах, которые-таки имеют теоретические обоснования и доказательную базу. Но это не умаляет того, что ОП поставил себе ебически сложную и абсолютно бессмысленную задачу.
Аноним 05/12/19 Чтв 17:47:45 153840328
>>1538360
На бумажке с установленным набором аксиом ты можешь доказать что угодно - это и есть суть математики. Но как только программа с бумажки переходит в реальный компьютер, то она тут же становится недоказуемой по определению.
Аноним 05/12/19 Чтв 17:51:12 153840829
>>1538403
>аксиом = постулат = говно
изначально не доказуемое говно
Аноним 05/12/19 Чтв 18:37:48 153843330
>>1536179
Потому что надо было тратить время не на SF, а на LF.
Аноним 05/12/19 Чтв 18:43:50 153843631
>>1538408
О, ещё один не понимает смысл аксиом.
Аноним 05/12/19 Чтв 20:26:19 153848632
>>1538403
>Но как только программа с бумажки переходит в реальный компьютер, то она тут же становится недоказуемой по определению.
Просто невероятно, какие же тут долбоебы сидят. Иди свой реакт дрочи, плебей.
Аноним 05/12/19 Чтв 22:14:30 153861833
>>1538486
>пук
Я понял, держи в курсе.
Аноним 05/12/19 Чтв 22:20:32 153863734
>>1538486
Это еще что, студентик, вот когда откроешь для себя принципиальную недоказуемость любой научной теории - так вообще охуеешь наверное.
Аноним 06/12/19 Птн 00:16:29 153877935
image.png (97Кб, 611x295)
611x295
>>1538637
>принципиальную недоказуемость любой научной теории
axaxaxaxaxa
Аноним 06/12/19 Птн 02:56:46 153883236
1
Аноним 06/12/19 Птн 03:07:06 153883637
image.png (106Кб, 498x374)
498x374
>>1538403
>Но как только программа с бумажки переходит в реальный компьютер, то она тут же становится недоказуемой по определению.
Аноним 06/12/19 Птн 05:18:42 153885538
>>1536160 (OP)
>Есть две программы на разных языках, обе реализуют один и тот же алгоритм. Как формально доказать, что для всех возможных входных данных они возвращают одинаковый результат?
Есть методы оценки и доказательства. Подозреваю их очень много. Этим занимается теория вычислимости. Она к сожалению в вывшем СССР слабо развита. Но труды есть, их много. Только их не просто гуглить, ибо ключевых слов тысячи. Есть также программные средства доказательства теорем, например Coq.

Тут есть упоминание
http://mk.cs.msu.ru/images/8/82/Thesis_Novikova.pdf
Аноним 06/12/19 Птн 09:09:55 153888839
>>1538779>>1538836
Что-то в голос, мамкины математики реально не в курсе, что в науке нет доказательств, только опровержения? Одна из главных причин кстати, по которым математика не классифицируется как наука. Но продолжайте, мне интересно послушать ваши шизоидные разрывы.
Аноним 06/12/19 Птн 09:21:21 153889440
>>1538888
> не различает разные типы наук
> пытается делать выводы из своей ложной предпоссылки
Аноним 06/12/19 Птн 09:41:40 153890041
>>1538894
Мань, еще раз, любая работающая с реальным миром наука не может ничего доказать просто по определению. Программы в каком мире исполняются, в реальном или на твоей бумажке, где ты их "доказал"?
Аноним 06/12/19 Птн 09:43:00 153890242
>>1538900
В голос с этого простака.
Аноним 06/12/19 Птн 10:40:02 153894443
>>1538888
Иди уроки учи, школьник. И не забудь почитать книги: "Математическая логика" Чёрча и с таким же названием книга Гилберта.
Аноним 06/12/19 Птн 17:05:58 153935844
15749993266750.png (70Кб, 323x323)
323x323
>>1538403
> как только программа с бумажки переходит в реальный компьютер, то она тут же становится недоказуемой по определению.
Ага, превращается в тыкву. Изоморфизм Карри-Говарда погугли, хотя все равно ничего не поймёшь.
Аноним 06/12/19 Птн 17:39:39 153942245
>>1538944>>1539358
То есть студенты матфака с обосранными штанами все равно не понимают, о чем именно речь и продолжают твердить себе "если на бумажке работает, то и в компьютере работает, вот попробуй на бумажку переписать структуру программы и тогда докажется". Я даже не знаю, каким еще более простым языком вам можно объяснить, давайте как детям:
1) Компьютерная программа - это по сути научная теория, на бумаге она сформулирована охуенной доказуемой математикой, но работать ей приходится в ужасном реальном мире
2) С реальным миром взаимодействовать можно только через эксперименты
3) Эксперимент не может доказать никакую теорию, только опровергнуть
4) Единственный способ взаимодействия с компьютерной программой, работающей в реальном мире - это эксперимент, а значит и доказать ее корректность нельзя.
А теперь попрошу вместо стандартного пердежа рассказать, с каким именно пунктом вы несогласны и как предлагаете доказывать научные теории, я посмеюсь.
Аноним 06/12/19 Птн 18:48:34 153948346
>>1539422
Ты узколобый необразованный невежда. Есть автоматические системы докательства теорем: Coq, Agda, и т.п. Есть формальные языки, описывающие семантику, прагматику языков программирования, используя которые можно рассуждать о корректности программ.

У тебя абсолютно нулевое знание математики. Для начала ознакомься как доказываются теоремы, и что такое аксиомы. Почитай Колмогорова, он хорошо описывает принципы изучения математики, метаматематики, и доказательства.
Аноним 06/12/19 Птн 18:54:32 153948847
Да-да-да, ДС
Аноним 06/12/19 Птн 19:01:15 153949848
>>1539422
Чё ты мне простыни своего крайне ценного школьного мнения пишешь, я сослался на совершенно конкретную вещь, попробуй погуглить и понять, что ты не самый умный. Хотя, шизику что-то доказывать, такое себе...
Аноним 06/12/19 Птн 19:09:44 153950549
>>1539483
Манюнь, речь не о математике, а о том, что вне математики доказательств нет. Я же не спорю, что на бумажке все прекрасно доказываются и что теоремы с аксиомами заебись. Но теорема и теория - это немного разные вещи, жаль, что ты этого понять никак не можешь.
>>1539498
Классная вещь, жаль только, что чтобы провести соответствие между между программой и ее мат. доказательством, программу сначала надо переписать на бумажку, то есть возвращаемся к началу. Зачем ты себе в штаны насерил?
Аноним 06/12/19 Птн 19:27:44 153952550
>>1539505
Господи, ещё один шизик. Сколько вас тут? Хотя, ещё бы время тратить на очередное чучело зумера, считающее, что умнее всех.
Аноним 06/12/19 Птн 19:49:34 153955451
>>1539505
Ты наркоман штоле, сука? Тебе же сказали, есть специальные дисциплины, знания, методы, и инструменты, для доказательства компьютерных программ. Убейся аб стену!
Аноним 06/12/19 Птн 20:08:50 153957452
>>1539554
>есть
Покажи хоть один, который не полагается на "докажи корректность в голове/на бумаге, а потом перепиши в компьютер". Я думаю, ты запнешься еще на этапе "докажи, что переписал без опечаток".
Аноним 06/12/19 Птн 20:56:52 153960853
>>1539574
Ок, Мань. Вот смотри. Есть таблица умножения на бумаге, и есть счёты. Будет ли разница между вычислением на бумаге и на счетах? Далее, есть булева логика на бумаге и есть логические вентили в микросхеме. Будет ли разница между работой логических вентилей и такой же записью на бумаге? Тебе в рот ссать можно ещё очень и очень долго, мне просто лень приводить более сложные примеры.
Аноним 06/12/19 Птн 21:05:31 153961754
>>1539608
Я когда-то на луркморье прочитал что-то вроде правил демагога, и там говорилось, что это не тролль должен что-то доказывать, а доказывать должны ему, а он должен говорить, что доказательство - говно. Так что лучше бы не кормить его.
Аноним 06/12/19 Птн 21:11:33 153962055
>>1539608
>Будет ли разница между вычислением на бумаге и на счетах?
define "вычисления на счетах" для начала. В отрыве от человека, который эти счет перекидывает и совершает все вычисления в уме, никаких "вычислений на счетах" нет. Так что давай аналогию получше, обсеря.
>логические вентили в микросхеме
Уже лучше, теперь надо доказать, что микросхема не бракованная и что там ничего местами не перепутано. На бумажке напишешь, что процесс создания микросхемы шел по строгому алгоритму, а поэтому брака там быть не может?
Аноним 06/12/19 Птн 21:12:57 153962156
Bump
Аноним 06/12/19 Птн 21:17:15 153962757
>>1538855
спасибо, анон, наконец-то хоть кто-то в теме
Аноним 07/12/19 Суб 00:10:25 153976758
>>1539620
Ты читал, что я пишу? Разница будет в этих случаях или нет? Счёты и микросхема не бракованные.
Аноним 07/12/19 Суб 00:24:11 153977459
>>1539767
Что именно означает "не бракованные"? Что они идеальные? Или все-таки, что погрешность в допустимых значениях? Но если второе, то у тебя в итоге выйдет, что 1 = 1.0000000000001 = 0.9999999999999, это ты уже доказал в математике? И опять же, кто доказал, что они не бракованные и не примут вдруг неожиданное значение в одной из миллиарда комбинаций?
Аноним 07/12/19 Суб 00:42:19 153978660
>>1539774
Ок, давай иначе. Результат на бумаге и на счетах и на бумаге и микросхеме получился одинаковый. Что мы этим опровергли?
Аноним 07/12/19 Суб 01:31:10 153981461
>>1539774
доказывается корректность работы программы, а не микросхемы, идиот ебаный
Аноним 07/12/19 Суб 02:42:20 153983162
15712688944920.png (131Кб, 431x431)
431x431
Раньше всегда удивлялся, почему шизики легко примут и будут отстаивать с пеной у рта очевидную шизу и бред вместо нормальной, простой понятной и доказанной теории. А потом понял - одному шизу ближе и понятнее маняидеи другого такого же шиза, но не нормального здорового человека. Потому что шизофренический уклад един, ШУЕ.
Аноним 07/12/19 Суб 08:57:28 153988063
>>1539786
Чтобы сравнить результат на счетах и результат на бумаге, результат на счетах нужно сначала перевести на бумагу или хотя бы в голову. Как ты собрался это сделать без погрешности?
>>1539814
Молодец, ты уже что-то начал понимать. Я очень рад, что ты изобрел программы, которые могут выполняться в более высоком измерении, но обычные люди пока еще дрочатся с микросхемами(а некоторые даже со счетами) и программы выполнять могут только на них. Так вот, повторяю вопрос - как ты докажешь корректность работы программы, если даже не можешь доказать, что ее среда выполнения работает корректно?
Аноним 07/12/19 Суб 09:00:59 153988164
>>1539831
>доказанной теории
Теория не бывает доказанной. Подтвержденной - да, но это разные вещи и подтвержденная миллиард раз теория может быть опровергнута одним экспериментом в любой момент. Этим науки и отличаются от математики, что непонятного?
Аноним 07/12/19 Суб 13:46:00 153998565
>>1539880
Тебе лечиться нужно, ШИЗа.
Аноним 07/12/19 Суб 14:17:46 154000766
>>1536160 (OP)
Проверить код на более низком уровне, например машинном.
Аноним 07/12/19 Суб 14:36:26 154002567
>>1536160 (OP)
Прогнать на одинаковых тестах и не трахать мозги. Доказательства это сложная тема, на которую нужно потратить не один год жизни.
Аноним 07/12/19 Суб 22:12:17 154051468
Аноним 08/12/19 Вск 00:15:40 154060369
>>1540514
Ну давай, предложи свой вариант, умник.
Настройки X
Ответить в тред X
15000 [S]
Макс объем: 40Mб, макс кол-во файлов: 4
Кликни/брось файл/ctrl-v
Стикеры X
Избранное / Топ тредов