Войти
ФлеймФорумЮмор

Даже неправильные программы могут иногда работать (2 стр)

Страницы: 1 2 3 4 Следующая »
#15
(Правка: 17:46) 17:44, 16 авг. 2018

Delfigamer
> Согласитесь, если спросить какого-нибудь пыхаскриптера о доказательстве - он ведь так и ответит, или сделает ещё более сильное утверждение о невозможности.
но если спросить кого-нибудь из тех кто три года доказывал корректность микроядра L4(и написал 200к строк доказательств для 7.5к строк кода) то он ответит тоже самое. Так что утиный тест скорее может помочь определить того кто уже услышал о доказательствах но сам еще ничего не доказывал.


#16
17:49, 16 авг. 2018

Delfigamer
> Если и правда все потоки остановятся и игра лаганёт на полсекунды - это
> правильное поведение, которое не содержит никаких проблем?
Нет, драйвер звука отвалится и можешь "лагать" хоть часами. Я к тому что как бы правильно мы не писали программу, всегда могут возникнуть внешние факторы которые не позволят ей корректно отработать, программа в виде мат. формул это программа в вакууме.

#17
17:57, 16 авг. 2018

Тот же Дейкстра считал подход с доказательством существующего кода малоперспективным.
Его идея как раз - программировать отталкиваясь от идеи, что код нужно доказывать ("доказательство и написание идут рука об руку") и проектировать соответственно. "Proof-oriented programming", так сказать.

Но Дейкстра не популярен.

Насколько я могу судить, самый большой его проект в этом стиле - THE operating system.
Исходники её у меня не находятся. Собственный отчёт Дейкстры - очень лаконичен, и упоминает довольно традиционные методы.

Не уверен насколько это помогло бы товарищам от L4.

#18
(Правка: 18:23) 18:19, 16 авг. 2018

Ха-ха, kipar подыграл Delfigamer-у и тоже завернул километровые простыни в ссылки, вместо того, чтобы рядом положить. Так удобно! Читать синий подчеркнутый текст, а потом возюкать по нему мышкой и всматриваться в мелкий шрифт в углу, чтобы понять, что нажимать смысла нет.

#19
18:49, 16 авг. 2018

Если кому интересно:
https://en.wikipedia.org/wiki/THE_multiprogramming_system
http://www.cs.utexas.edu/users/EWD/ewd01xx/EWD196.PDF
https://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/EWD1303.html

#20
(Правка: 19:35) 19:19, 16 авг. 2018

kipar
Наверно, следовало уточнить, что под "программой" я подразумевал не монстра на 75К, а единичную функцию. Или ты будешь утверждать, что для доказательства квиксорта на 30 строк нужно написать научстатью на 30 страниц?

И тут, кстати, очень вовремя возник
FordPerfect
> Его идея как раз - программировать отталкиваясь от идеи, что код нужно
> доказывать ("доказательство и написание идут рука об руку") и проектировать
> соответственно. "Proof-oriented programming", так сказать.
В конечном счёте, Дейкстра оказался прав, ибо в современном мире существует SOLID, который в том числе является и гайдлайном к написанию таких программ, которые при попытке их доказать не оказывают вооружённого сопротивления.
Посудите сами:
1. Single responsibility principle - говорит о том, что A, B[a[/i] и s локализованы в одном месте и описывают одну концепцию. Как следствие - программа декомпозируется на небольшие самостоятельные элементы, которые доказываются по отдельности, в каждом отдельном доказательстве участвует минимальное число сущностей, и в результате, доказательства должны стать проще.
2. Open/closed principle - говорит о том, что добавление новых вещей не должно влиять на A и B[a[/i]; как следствие - однажды доказанный и проверенный s должен оставаться корректным дпри изменениях в других частях системы.
3. Liskov substitution principle -

Let ϕ(x) be a property provable about objects x of type T. Then ϕ(y) should be true for objects y of type S where S is a subtype of T.

Связь должна быть очевидна, но, на всякий случай, переведу на ITT-формализм - Изображение - все программы, корректные для типа T, так же должны быть корректны для его подтипа S.
Очевидно, это приводит к упрощению доказательства за счёт уменьшения числа участвующих сущностей - A и B[a[/i] достаточно знать только о T.
Так же интересно, что из описанного здесь формализма следуют и правила LSP:
Изображение - "preconditions cannot be strengthened in a subtype".
Изображение - "postconditions cannot be weakened in a subtype".
4. Interface segregation principle - опять же, упрощение за счёт уменьшения числа элементов.
5. Dependency inversion principle - и здесь тот же эффект: упрощение A и B[a] за счёт независимости от внутренних подробностей участвующих подмодулей.
Так вот как по-умному назывался мой блестящий велосипед - "инверсия зависимостей". Окей. Буду знать.

#21
19:24, 16 авг. 2018
entryway
ну да, так то Delfigamer один из самых умных чуваков здесь, поэтому обидеть ни в коем случае не хочу. Но вот этот "синий текст" со ссылками на всякие банальности бесит.
#22
19:32, 16 авг. 2018
kipar
Хех, я раза три хотел сообщением обратить на это внимание, но забивал по тем же причинам. А тут ты подвернулся как нельзя кстати, получилось как будто просто в эфир говорю, без претензий.
#23
(Правка: 19:46) 19:38, 16 авг. 2018
kipar
Ну а какие альтернативы для обозначения жирных намёков? «типичное мышление типичного кодера (см. "утиный тест")»? «типичное мышление типичного кодера* \\ * см. "утиный тест"»? Я всегда думал, что подсказка при наведении - самый эргономичный вариант. Те, кто поймут сразу - осознают и пойдут по своим делам. Кто не поймёт - нажмёт на ссылку и получит подробное объяснение шутки. И при этом, поток текста не нарушается - намёк содержится даже не в скобках, а вообще в отдельном подпространстве.

entryway
> мелкий шрифт в углу

+ 4К 21’’ крестьянин?

На самом деле, я не понимаю людей, которые не смотрят на адрес ссылки прежде, чем туда перейти. А вдруг это рикролл? Или мэйл.ру? Или вообще какой-нибудь данбоору? Обязательно нужно же проверять, на что тебя отправляют.
#24
(Правка: 20:04) 19:51, 16 авг. 2018

Delfigamer
> На самом деле, я не понимаю людей, которые не смотрят на адрес ссылки прежде,
> чем туда перейти.
В смысле не смотрят? В этом-то и проблема, что твои сообщения не получается читать глазами, их приходится читать глазами, руками и ещё косить в угол браузера.

Delfigamer
> Ну а какие альтернативы

Звучит, как типичное мышление типичного кодера, который уверен, что программисту не нужна математика.
https://en.wikipedia.org/wiki/Duck_test

Сразу понятно и что ты хотел сказать, и куда сослаться, и что там будет написано.
#25
19:54, 16 авг. 2018
Delfigamer
текстового указания вполне достаточно.
те кто знают термин - увидят его сразу и им не придется наводить мышку. Те кто не знают - сами способны загуглить если им интересно. Когда ссылка ведет на общеизвестные термины - ссылка выглядит как сомнение в знаниях собеседника, человек как будто с ребенком общается. Верх издевательства конечно когда ее еще за lgtfy прячут.
#26
(Правка: 20:23) 20:22, 16 авг. 2018

Delfigamer
> Или ты будешь утверждать, что для доказательства квиксорта на 30 строк нужно написать научстатью на 30 страниц?
Ну вот сходу из google:
https://maniagnosis.crsr.net/2017/08/AFL-verifying-quicksort.html
https://www.key-project.org/2017/08/17/dual-pivot/
http://www.cs.utexas.edu/users/sandip/publications/stobj-qsort/qs.pdf
https://www.researchgate.net/publication/239373253_Certification_… he_Coq_System
примерно того порядка, да (ну ок, чуть ближе к 10).

#27
20:40, 16 авг. 2018

kipar
> Верх издевательства конечно когда ее еще за lgtfy прячут.
То есть самый тонкий способ сказать мнение о собеседние - это такой?

#28
(Правка: 23:46) 23:42, 16 авг. 2018
Further, weirdly, proving that the result is sorted is frequently easier than proving that the result is a permutation.

Я звоню бычьему навозу. move-семантикой перестановочность доказывается чуть ли не на уровне компилятора.
Хотя, если стоит задача доказать неверблюдность компьютеру, то, может быть, это и правда сложно. Лично я никогда не пробовал доказать компьютеру, что я не верблюд.
#29
7:40, 17 авг. 2018

Ну и что? Вы не слышали о багах? О тех что проявляются весьма специфично.
Вот если бы один баг был бы "костылем" для другого тогда был бы фан.

Страницы: 1 2 3 4 Следующая »
ФлеймФорумЮмор