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

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

Страницы: 1 2 3 4 Следующая »
#0
10:06, 16 авг. 2018

> В этом заключается опасность Си и плюсов. Поэтому, для обучения - когда целью стоит понять, что отличает плохую программу от хорошей - Си подходит очень плохо.
Уже который раз сталкиваюсь, так что пусть будет филиал перлов, специализирующийся на программах, которые работают за счёт честного слова и кое-чьей матери (а не из-за того, что они правильные).

И стартовый перл:
MikeNew
> "Усилили работу" слоев валидации в новом сдк - вывалилось несколько ошибок
> которые в предыдущем сдк не показывались.


#1
10:15, 16 авг. 2018

"правильность"  программы,  особенно на крестах - понятие,  максимально субъективное. Я бы даже сказал - сферически в вакууме субъективное

#2
10:26, 16 авг. 2018

Pathetic Mike
Но первый перл не про кресты а про вулкан. Да и вообще любой язык от этого не застрахован, даже на Coq наверняка можно накосячить так что будет "случайно" доказательство проходить.

#3
(Правка: 16:55) 11:26, 16 авг. 2018

Pathetic Mike
На любую программу p можно наложить требования: будучи запущенной из любого исходного состояния a, принадлежащего множеству корректных исходных состояний A, программа должна перевести машину в одно из ожидаемых состояний B[a]. Всё, что удовлетворяет этому требованию, образует множество корректных программ:

    Изображение

(
    Пример требований:

25.4.6.3 make_heap [make.heap]

template<class RandomAccessIterator>
void make_heap(RandomAccessIterator first, RandomAccessIterator last);

template<class RandomAccessIterator, class Compare>
void make_heap(RandomAccessIterator first, RandomAccessIterator last, Compare comp);

1 Effects: Constructs a heap out of the range [first,last).
2 Requires: The type of *first shall satisfy the MoveConstructible requirements (Table 20) and the MoveAssignable requirements (Table 22).

)

Стандарт, в свою очередь, для каждого исходного текста s определяет множество возможных программ P[s], которые допускается получить от реализации i. Это определяет множество корректных реализаций:

    Изображение

Используя эти определения требований и Стандарта, легко соорудить определение корректного исходного текста: это такой текст, который на любой корректной реализации даст корректную программу:

    Изображение

Или, что то же самое - исходный текст корректен, если любая программа, произведённая корректной реализацией, в любой ситуации обладает корректным поведением:

    Изображение

Этот тред предназначен для сбора исходных текстов двух категорий.

1. Некорректный текст, который по неудачному стечению обстоятельств компилируется в корректную программу:

    Изображение

2. Некорректный текст, который скомпилировался в некорректную программу, но автор не удосужился её нормально протестировать и поэтому всё время думал, что делал всё верно:

    Изображение

#4
15:34, 16 авг. 2018

Delfigamer
> На любую программу p можно наложить требования: будучи запущенной из любого
> исходного состояния a, принадлежащего множеству корректных исходных состояний
> A, программа должна перевести машину в одно из ожидаемых состояний B[a]. Всё,
> что удовлетворяет этому требованию, образует множество корректных программ:
Красиво, но на деле доказательство зачастую на порядок сложнее собсна написания алгоритма.

#5
16:31, 16 авг. 2018

1 frag / 2 deaths
> Красиво, но на деле доказательство зачастую на порядок сложнее собсна написания алгоритма.
Звучит, как типичное мышление типичного кодера, который уверен, что программисту не нужна математика.

#6
16:46, 16 авг. 2018

Delfigamer
> На любую программу p можно наложить требования: будучи запущенной из любого
> исходного состояния a, принадлежащего множеству корректных исходных состояний
> A, программа должна перевести машину в одно из ожидаемых состояний B[a]. Всё,
> что удовлетворяет этому требованию, образует множество корректных программ:
Вводим зависимость от времени без фиксированного шага и приплыли.

#7
16:51, 16 авг. 2018

Delfigamer
Ну практика ж показала, так что там с современным софтом?

#8
16:51, 16 авг. 2018

Delfigamer
> А ещё, твоя мама - гей, а твой отец - трап. Это тоже математически объективное
> утверждение.

Я где-то что-то обидное сказал,  раз вызвал такой высер в свою сторону?

#9
16:51, 16 авг. 2018

Delfigamer
> Звучит, как типичное мышление типичного кодера, который уверен, что
> программисту не нужна математика.
так толсто что аж тонко.
или речь о том что "на порядок" это чересчур заниженная оценка, я бы сказал что там цифры начинаются с трех порядков.

#10
(Правка: 16:57) 16:53, 16 авг. 2018

Aroch
> Вводим зависимость от времени без фиксированного шага и приплыли.
Зависимость чего от времени? Входных данных? Порядка выполнения? Всё это точно так же заворачивается в "исходное состояние".

Aroch
> без фиксированного шага
А вот это уже физически невозможно, ибо цифровые машины дискретны по своей природе.

Pathetic Mike
> Я где-то что-то обидное сказал, раз вызвал такой высер в свою сторону?
Тебя задело? Я думал, мы в интернете.
Окей, уберу.

1 frag / 2 deaths
> Ну практика ж показала, так что там с современным софтом?

In the code snippets so far [ Editor's note: (*i).toLower() - end note ], we used the unary * operator to retrieve the item (of type QString) stored at a certain iterator position, and we then called QString::toLower() on it. Most C++ compilers also allow us to write i->toLower(), but some don't.

Увы, но у значительной части кодеров очень неудобная докритическая масса каши в голове - достаточно, чтобы зафейлить программу как теорему, но недостаточно, чтобы зафейлить категории 1 и 2.
#11
16:58, 16 авг. 2018

Delfigamer
> А вот это уже физически невозможно, ибо цифровые машины дискретны по своей
> природе.
у тебя нет контроля над всей машиной, программа взаимодействует на уровне ОС, а ОС тебе может сказать иди отдохни у меня IO подвисло, как освобожусь постучусь. Проходит время, всё я освободилась, можешь считать дальше куда там игрок приземлился в прыжке над пропастью.

#12
(Правка: 17:03) 17:03, 16 авг. 2018

Aroch
И что, в такой ситуации нет возможности определить, какое поведение является корректным? Тогда скажи, что ситуации с длительными задержками не входят в A. Это равносильно тому, что пользование программой в такой ситуации - UB, то есть на поведение не накладывается совершенно никаких ограничений. Это не мешает накладывать ограничения на поведение в случаях, на которые программа рассчитана; а значит - определение корректности всё также существует и не колышется.

#13
17:18, 16 авг. 2018

Delfigamer
> И что, в такой ситуации нет возможности определить, какое поведение является
> корректным?
с точки зрения кого? Для программы любое поведение корректно пока она не грохнулась, и даже падение разраб может обозвать фичей, а не багом, только пользователя ты в этом вряд ли убедишь.
> Тогда скажи, что ситуации с длительными задержками не входят в A. Это
> равносильно тому, что пользование программой в такой ситуации - UB, то есть на
> поведение не накладывается совершенно никаких ограничений.
Ну вот смотри у тебя есть два потока, и тебе нужно их синхронизировать звук и видео, и тут из-за не завясящих от программы обстоятельств операция со звуком дает существенную задержку, а поток рендера в порядке. И что ты будешь делать? Игрок уже прыгнул в реку и плывет, а поток звука ждет когда же загрузится и проиграется крик "яхуу!" перед прыжком. Предлагаешь остановить все потоки и ждать чтобы не возникло рассинхронизации?

#14
(Правка: 17:32) 17:24, 16 авг. 2018

Я не говорю, что программист обязан доказывать корректность всего движка на 500+ килострок. Разумеется, это непосильная задача для человека.
Изначально, я задумывал этот тред как подборку всяких UB, опечаток, крестололов и прочих оплошностей. Главная тема этого треда - из того, что программа верно отработала энное число раз, не следует, что программа всегда будет верно работать в любых допустимых ситуациях. То есть - из корректности некоторых примеров не следует корректность самой программы.

Затем, в тред врываются знатоки и начинают утверждать:
> "правильность" программы, особенно на крестах - понятие, максимально
> субъективное. Я бы даже сказал - сферически в вакууме субъективное
В ответ, я показал, что эта точка зрения не верна; "правильность программы" - это объективный критерий, который поддаётся формализации, и как следствие - может быть проверен математическими методами; например - системой типов.

Касательно
> Красиво, но на деле доказательство зачастую на порядок сложнее собсна написания алгоритма.
я так и написал - "звучит, как" и даже сделал ссылку на утиный тест. Предполагалось, что это покажет, что речь идёт не о способностях Тараса (я их не знаю), а именно о самой фразе. Согласитесь, если спросить какого-нибудь пыхаскриптера о доказательстве - он ведь так и ответит, или сделает ещё более сильное утверждение о невозможности.
Конечно, существуют критерии, которые доказать невозможно, но это вовсе не то, о чём думает рядовой пыхаскриптер.

Aroch
> с точки зрения кого?
А! Наконец, у нас появился правильный вопрос.
Разумеется, у меня уже давно есть объективно формально математически правильный ответ.

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

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