Как развернуть односвязный список на собеседовании

    Привет, Хабр.


    Я тут на днях сходил на собеседование в одну серьёзную фирму, и там мне предложили перевернуть односвязный список. К сожалению, эта задача заняла весь первый раунд собеседования, а по окончанию интервьювер сказал, что все остальные сегодня заболели, и поэтому я могу идти домой. Тем не менее, весь процесс решения этой задачи, включая пару вариантов алгоритма и последующее их обсуждение, а также рассуждения о том, что вообще такое переворачивание списка, под катом.


    image


    Решаем задачу


    Интервьювер был довольно приятным и дружелюбным:


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


    — Сейчас сделаю! А на каком языке лучше это сделать?


    На каком вам удобнее.


    Я собеседовался на C++-разработчика, но для описания алгоритмов на списках это не лучший язык. Кроме того, я где-то читал, что на собеседованиях сначала надо предложить неэффективное решение, а потом последовательно его улучшать, так что я открыл ноутбук, запустил vim и интерпретатор и набросал такой код:


    revDumb : List a -> List a
    revDumb [] = []
    revDumb (x :: xs) = revDumb xs ++ [x]

    Пока интервьювер всматривался в код, я решил сразу проявить инициативу и указал, что это на самом деле плохой алгоритм, потому что он имеет квадратичную сложность из-за неэффективного дописывания элемента в конец, и сразу написал улучшенный вариант, выполняющийся за линейное время:


    revOnto : List a -> List a -> List a
    revOnto acc [] = acc
    revOnto acc (x :: xs) = revOnto (x :: acc) xs
    
    revAcc : List a -> List a
    revAcc = revOnto []

    — Тут мы проходимся по списку один раз, и каждый раз дописываем новый элемент в начало, а не в конец, так что алгоритм линейный.


    Сравниваем решения


    Я ожидал каких-нибудь вопросов от интервьювера, но он лишь переводил взгляд с экрана на меня и обратно. Ещё немного подождав, я решил снова проявить инициативу (ведь компании же любят инициативных?) и хоть что-то говорить, чтобы заглушить неудобную тишину:


    — Ну, вообще говоря, не факт, что эти две функции делают одно и то же, поэтому давайте их проанализируем и докажем, что они действительно эквивалентны, то есть, на любом входе выдают одно и то же значение.


    С этими словами я снова взял клавиатуру и начал печатать


    revsEq : (xs : List a) -> revAcc xs = revDumb xs

    Интервьювер ничего не говорил, так что я продолжил:


    — Ну, сгенерируем определение и сделаем case split по единственному аргументу.


    Несколько нажатий — generate definition, case split, obvious proof search — и среда разработки превратила ту строку в


    revsEq : (xs : List a) -> revAcc xs = revDumb xs
    revsEq [] = Refl
    revsEq (x :: xs) = ?revsEq_rhs_1

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


    — Ну, с базовым случаем для пустого списка все очевидно, тайпчекер даже вон сам вывел, а вот теперь придётся немного подумать. Очевидно, что доказывать свойства рекурсивных функций имеет смысл по индукции, поэтому получим доказательство для меньшего списка и посмотрим, что нам после этого нужно будет сделать:


    revsEq : (xs : List a) -> revAcc xs = revDumb xs
    revsEq [] = Refl
    revsEq (x :: xs) = let rec = revsEq xs in ?wut

    — Если теперь посмотреть на дырку ?wut, то мы увидим среди прочего


      rec : revOnto [] xs = revDumb xs
    --------------------------------------
    wut : revOnto [x] xs = revDumb xs ++ [x]

    — Естественно захотеть подставить revDumb xs из пропозиционального равенства, даваемого rec. Заменим последнюю строчку на:


    revsEq (x :: xs) = let rec = revsEq xs in
                       rewrite sym rec in ?wut

    и получим цель


    --------------------------------------
    wut : revOnto [x] xs = revOnto [] xs ++ [x]

    — Вынеcем это в отдельную лемму и сфокусируемся на её доказательстве:


    lemma1 : (x0 : a) -> (xs : List a) -> revOnto [x0] xs = revOnto [] xs ++ [x0]

    Я снова делаю generate definition, case split по xs, obvious proof search для первой ветки и получаю


    lemma1 : (x0 : a) -> (xs : List a) -> revOnto [x0] xs = revOnto [] xs ++ [x0]
    lemma1 x0 [] = Refl
    lemma1 x0 (x :: xs) = ?lemma1_rhs_2

    — Снова доказываем утверждение по индукции, но теперь всё интереснее. Можно получить доказательство для lemma1 x xs, а можно для lemma1 x0 xs. Из соображений симметрии первое нам, скорее всего, подойдёт больше, так что перепишем последнюю строчку в


    lemma1 x0 (x :: xs) = let rec = lemma1 x xs in ?wut

    и посмотрим на дырку ?wut:


      rec : revOnto [x] xs = revOnto [] xs ++ [x]
    --------------------------------------
    wut : revOnto [x, x0] xs = revOnto [x] xs ++ [x0]

    — Возникает естественное желание заменить revOnto [x] xs из цели на выражение справа от знака равенства в rec. Попробуем:


    lemma1 x0 (x :: xs) = let rec = lemma1 x xs in
                          rewrite rec in ?wut

    — Посмотрим, во что превратилась наша цель доказательства:


    --------------------------------------
    wut : revOnto [x, x0] xs = (revOnto [] xs ++ [x]) ++ [x0]

    — Ух, какой там ужас. Давайте воспользуемся ассоциативностью конкатенации списков:


    lemma1 x0 (x :: xs) = let rec = lemma1 x xs in
                          rewrite rec in
                          rewrite sym $ appendAssociative (revOnto [] xs) [x] [x0] in ?wut

    — Теперь цель выглядит по-божески:


    --------------------------------------
    wut : revOnto [x, x0] xs = revOnto [] xs ++ [x, x0]

    — Так это же почти утверждение нашей оригинальной леммы! Разве что, наша лемма работает только для аккумулятора, содержащего один элемент, а тут необходимо работать с двумя элементами. Традиционно для математики упростим себе задачу, усилив доказываемое утверждение, и запишем новую лемму:


    lemma2 : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc

    Привычным движением заставляю IDE сделать всю грязную работу. При этом case split мы делаем по lst, а не по acc, так как revOnto рекурсивно определён по lst:


    lemma2 : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc
    lemma2 acc [] = Refl
    lemma2 acc (x :: xs) = ?wut1

    В wut1 нам надо доказать


    --------------------------------------
    wut1 : revOnto (x :: acc) xs = revOnto [x] xs ++ acc

    Снова воспользуемся индукцией для второго случая:


    lemma2 acc (x :: xs) = let rec = lemma2 (x :: acc) xs in ?wut1

    Теперь мы имеем


      rec : revOnto (x :: acc) xs = revOnto [] xs ++ x :: acc
    --------------------------------------
    wut1 : revOnto (x :: acc) xs = revOnto [x] xs ++ acc

    Перепишем цель с использованием rec:


    lemma2 acc (x :: xs) = let rec = lemma2 (x :: acc) xs in
                           rewrite rec in ?wut1

    и получим новую цель


    --------------------------------------
    wut1 : revOnto [] xs ++ x :: acc = revOnto [x] xs ++ acc

    — Правая часть снова что-то напоминает. Действительно, тут мы могли бы воспользоваться нашей lemma1 для единичного элемента, но заметим, что lemma2 тоже подходит, так как lemma1 x xs даёт то же утверждение, что lemma2 [x] xs:


    lemma2 acc (x :: xs) = let rec1 = lemma2 (x :: acc) xs in
                           let rec2 = lemma2 [x] xs in
                           rewrite rec1 in
                           rewrite rec2 in ?wut1

    Теперь наша цель выглядит так:


    --------------------------------------
    wut1 : revOnto [] xs ++ x :: acc = (revOnto [] xs ++ [x]) ++ acc

    Тут снова можно воспользовать ассоциативностью конкатенации, после чего цель будет решить легко:


    lemma2 : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc
    lemma2 acc [] = Refl
    lemma2 acc (x :: xs) = let rec1 = lemma2 (x :: acc) xs in
                           let rec2 = lemma2 [x] xs in
                           rewrite rec1 in
                           rewrite rec2 in 
                           rewrite sym $ appendAssociative (revOnto [] xs) [x] acc in Refl

    — Заметим, что lemma1 нам теперь не нужна, и мы можем её выкинуть, переименовав lemma2 просто в lemma. И теперь мы, наконец, можем на неё сослаться в нашем исходном доказательстве, получив итоговый вариант:


    lemma : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc
    lemma acc [] = Refl
    lemma acc (x :: xs) = let rec1 = lemma (x :: acc) xs in
                          let rec2 = lemma [x] xs in
                          rewrite rec1 in
                          rewrite rec2 in 
                          rewrite sym $ appendAssociative (revOnto [] xs) [x] acc in Refl
    
    revsEq : (xs : List a) -> revAcc xs = revDumb xs
    revsEq [] = Refl
    revsEq (x :: xs) = let rec = revsEq xs in
                       rewrite sym rec in lemma [x] xs

    У меня оставалось ещё минут 15, интервьювер по-прежнему ничего не говорил, поэтому я решил продолжить.


    — Ну, если хотите, мы можем ещё что-нибудь обсудить.


    Хорошо, предположим, вы вот написали это всё. Но вы же даже ни разу не запустили этот код! Как вы можете быть уверены, что вы действительно написали функцию обращения списка? Где тесты?!


    Проверяем решение


    — Прекрасно! Я рад, что вы об этом заговорили! Действительно, а откуда мы вообще знаем, что наше решение верное? Что вообще значит «перевернуть список»? Представляется разумным следующее определение: если xs — некоторый список, то xs' будет его «переворот» тогда и только тогда, когда левая свёртка исходного списка с любой функцией и любым начальным значением даёт тот же результат, что правая свёртка перевёрнутого списка с той же функцией и тем же начальным значением. Давайте это запишем!


    revCorrect : (xs : List a) ->
                 (f : b -> a -> b) ->
                 (init : b) ->
                 foldl f init (revDumb xs) = foldr (flip f) init xs

    — Так как мы уже доказали, что revDumb равно revAcc (технически мы доказали forall xs. revDumb xs = revAcc xs, а равенство функций следует из экстенсиональности, которую мы, увы, не можем интернализировать), то нам неважно, какую из функций обращения списка рассматривать, так что мы для простоты возьмём revDumb.


    В очередной раз делаем привычные заклинания, вызываем индуктивную гипотезу и получаем


    revCorrect : (xs : List a) ->
                 (f : b -> a -> b) ->
                 (init : b) ->
                 foldl f init (revDumb xs) = foldr (flip f) init xs
    revCorrect [] f init = Refl
    revCorrect (x :: xs) f init = let rec = revCorrect xs f init in ?wut

    Наша цель сейчас выглядит так:


      rec : foldl f init (revDumb xs) = foldr (flip f) init xs
    --------------------------------------
    wut : foldl f init (revDumb xs ++ [x]) = f (foldr (flip f) init xs) x

    — Снова пользуемся равенством из индуктивной гипотезы:


    revCorrect (x :: xs) f init = let rec = revCorrect xs f init in
                                  rewrite sym rec in ?wut

    получая


    --------------------------------------
    wut : foldl f init (revDumb xs ++ [x]) = f (foldl f init (revDumb xs)) x

    — Начиная с этого момента revDumb xs нам не нужен. Нам достаточно сформулировать и доказать довольно очевидное свойство левых свёрток: свёртка всего списка с функцией f эквивалентна функции f, вызванной с результатом свёртки префикса списка и последнего элемента списка. Или в коде:


    foldlRhs : (f : b -> a -> b) ->
               (init : b) ->
               (x : a) ->
               (xs : List a) ->
               foldl f init (xs ++ [x]) = f (foldl f init xs) x

    — Доказательство совсем простое, и поэтому мы его сразу напишем и воспользуемся этой леммой для доказательства исходного утверждения. Итого:


    foldlRhs : (f : b -> a -> b) ->
               (init : b) ->
               (x : a) ->
               (xs : List a) ->
               foldl f init (xs ++ [x]) = f (foldl f init xs) x
    foldlRhs f init x [] = Refl
    foldlRhs f init x (y :: xs) = foldlRhs f (f init y) x xs
    
    revCorrect : (xs : List a) ->
                 (f : b -> a -> b) ->
                 (init : b) ->
                 foldl f init (revDumb xs) = foldr (flip f) init xs
    revCorrect [] f init = Refl
    revCorrect (x :: xs) f init = let rec = revCorrect xs f init in
                                  rewrite sym rec in foldlRhs f init x (revDumb xs)

    Так а тесты-то где?
    — А они не нужны. Мы же формально доказали, что мы обращаем список.
    … Хм, похоже, время вышло. Ну, спасибо за то, что пришли к нам на интервью, всего доброго, мы вам перезвоним.


    Правда, почему-то до сих пор не перезвонили.

    Поделиться публикацией

    Похожие публикации

    AdBlock похитил этот баннер, но баннеры не зубы — отрастут

    Подробнее
    Реклама

    Комментарии 463

      +4
      Правда, почему-то до сих пор не перезвонили.

      Потому что надо быть проще :D
        0
        Зачем? Ведь грамотно всё разжевал…
        +29

        Хорошо, а теперь оцените объем памяти, требуемый для исполнения этой функции.

          +3

          Время интервью вышло, так что отвечу кратко: возьму uniqueness types, а дальше достаточно умный компилятор всё сделает без дополнительных аллокаций.

            +29
            Все вы так говорите
              +3
              А как это доказать?
                +10

                Так же формально за полчаса не получится. Чуть менее формально — потому что компилятор знает, что каждый элемент используется не более одного раза, поэтому он спокойно может мутировать указатели вместо создания новых элементов.


                Компилятор Idris'а, на самом деле, не настолько умён, в него слишком мало ресурсов вкладывается (я удивлюсь, если reverse с uniqueness types он скомпилирует в инплейс), но вот какой-нибудь ghc, когда может подобные вещи вывести (ибо в хаскеле пока нет афинных типов), вполне себе так оптимизирует код.


                Чё-то я тут слишком серьёзный, похоже.

                  +43

                  Это наверное такой мем от функциональщиков — я раз несколько на Хабре в статьях о ФП видел утверждение, что "компилятор оптимизирует", или что "оптимальный код — забота компилятора". Кажется, иногда это говорили всерьез.

                    +1
                    Ну насчет хаскелля не скажу, но, например, в лиспе, lparallels действительно даёт возможность просто писать многопоточный код по сравнению с императивными языками. Да и вообще выявлять, и, главное, оптимизировать узкие места проще (впрочем, не исключаю confirmation bias задач, которые я решал на лиспе)
                      0
                      Что за lparallels, о которых вы говорите? Гугл не выдаёт ничего внятного.
                        0
                        Да вроде в первой строчке выдаче
                        lparallel.org
                      +3
                      А кто ещё может оптимизировать? Людям это доверять нельзя, они баги вносят, когда пытаются оптимизировать.
                +58
                Подчиненный перед лицом начальствующим должен иметь вид лихой и придурковатый, чтобы умом своим не смущать начальства.
                  +6
                  Почему не оформлено как цитата? Или вы всё ещё живы?
                    +6

                    Потому что это и не цитата. Просто забавная выдумка, автор которой не известен.

                      –1
                      Пётр первый…
                        +6
                        Если верить…
                      +25

                      Ну, как минимум, потому, что с телефона это оформлять неудобно. Да и:
                      "Главная проблема цитат в интернете в том, что люди сразу верят в их подлинность". (с) В. И. Ульянов (Ленин)

                      0
                      чтобы умом своим не смущать начальства.
                      Новый уровень ума — мудрость.
                        +1
                        — В чем состоит наипервейшая обязанность придворного? — спросил эмир.
                        Ходжа Насреддин ответил ему так:
                        — О великий и блистательный повелитель! Наипервейшая обязанность придворного состоит в каждодневном упражнении спинного хребта, дабы последний приобрел необходимую гибкость, без чего придворный не может достойным образом выразить свою преданность и свое благоговение. Спинной хребет придворного должен обладать способностью изгибаться, а также извиваться во всех направлениях, в отличие от окостеневшего хребта какого-нибудь простолюдина, который даже и поклониться не умеет как следует.

                        (Повесть о Ходже Насреддине)
                        +24

                        Статья вызывает улыбку. Но кроме всего прочего поднимет проблему важности soft skill наряду с развитыми hard skill.

                          +25

                          Мне бы, пожалуй, скорее хотелось бы поднять вопрос скучных задачек на собеседованиях. Но его уже и так сто раз поднимали.

                            +25
                            Зато троллинг skills у вас прокачан огого!
                              +7
                              Это для вас они скучные.
                              А у меня знакомый набирал людей на разработку — так кандидаты не знали, сколько бит в байте и сколько байт в 32-разрядном инте. Что такое указатель — вообще страшная тайна, шаманство какое-то…
                                +2
                                Тоже на С++?
                                  0
                                  Угу. Там работа с оборудованием на довольно низком уровне — посему кандидатам неплохо было бы знать, как типы данных лежат в памяти.
                                    0
                                    Когда меня брали на, то давали схемы и потом просили описать пути электронов после подачи питания.
                                    И да — это важно знать, если ты пишешь микрокод контроллера шины.
                                      +4
                                      Надеюсь там электроны двигались против направления тока.
                                        +2

                                        Вы хотели сказать, против условного направления тока?

                                          0
                                          ну да, как-то так
                                        0

                                        А скорость движения электронов спрашивали?
                                        А то бывают интересные версии...

                                    +12
                                    >не знали, сколько бит в байте
                                    Это вы им показали 9-битные и попросили обосновать?
                                      +1
                                      Там действительно мой знакомый, и проект у них вполне практический. И оборудование достаточно стандартное — процессоры x86 почти везде, кое-где вроде как пытались внедрить ARMы. Так что байты там нормальные, восьмибитные.
                                      Но выясняется страшное: приходят собеседоваться специалисты, которые вообще никогда не задумывались о том, как именно данные хранятся в памяти. А им по работе надо пакеты между нодами туда-сюда гонять по чахлым каналам связи…
                                        +2

                                        Неспроста в университетах обучение идёт с основ: базовая логика, структуры данных, ассемблер, С и только потом уже идут C#, Java, Python. Многим это не нравится, потому что не получается сразу начать писать практический код. Но по факту если человек начинает изучение программирования сразу с языка скриптового уровня, то ему потом становится сложно подтягивать базу, потому что это требует времени.

                                          +5

                                          А если с языка низкого уровня, то многие заболевают преждевременной оптимизацией.

                                            0
                                            Возможно, наоборот aka эффект декомпрессии. Не надо байтики руками перекладывать, можно использовать композицию функций, объекты, часть паттернов и гуй из коробки… В итоге код легко пишется, неплохо читается и поддерживается, но жрёт много памяти и проца и местами подтекает.
                                              +1

                                              Нет, чаще народ начинает искать, что быстрее i < n или i <= n — 1, и заменять деление на сдвиги.

                                                0
                                                Такая фигня обычно проходит после первого коммерческого проекта на языке, особенно если сроки горят.
                                                  +2

                                                  Я видел такое от программистов с годами опыта. В основном они любят утверждать, что софта на ГЦ нет потому что на нем нельзя писать рилтайм приложения, и скоро С++ захватит мир. Невыдуманная история.

                                                    0
                                                    Насколько я знаю, специфика и подходы к написанию риалтаймовых приложений одинаковы, но дополнительно надо очень хорошо знать устройство виртуальной машины. Имхо, какую-нибудь RTOS я бы на условной Java писать не стал, просто из экономии времени на разработку.
                                                      +2

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

                                                        0
                                                        А за это не бьют на ревью или просто тимлды/архитекторы? В кровавом энтерпрайзе опыта работы нет, потому не знаю, что из того, что как бы должно быть, есть на самом деле.
                                                    0

                                                    Оно не то, что проходит, а даже становится хуже.
                                                    Конструкции вида OrderBy(...).First() появляются всё чаще и чаще.

                                                      0
                                                      т.е. вместо поиска условно максимума сначала сортируют весь массив/лист/etc и получают вместо O(n) O(nlogn)?
                                                        0

                                                        Именно.

                                                          0

                                                          Суть в том, что если в массиве максимум 10 элементов, такой код проще и понятнее оптимального (придется либо писать свой экстеншн, либо переписывать на ручной цикл), и имеет право а жизнь. Но многие триггерятся на сам факт неоптимальности (Как же так! Тут логарифм появился просто так!). Не знаю, предпочел бы я в данном случае читаемость или цикломатику, но я прекрасно понимаю людей, которые не будут сильно париться над этим. Не потому, что они говнокодеры и им лишь бы пожрать лишних циклов CPU, а потом что там дальше пересылка по сети и выигрышь 10 тактов процессора не даст ничего.

                                                            0

                                                            Самый читаемый вариант тут всё же- MaxBy(...) или MinBy(...). И этот же вариант как раз даёт нужный профиль исполнения — это ж вообще праздник, согласитесь.

                                                              0

                                                              Безусловно, но, увы, в стандартной поставке его нет.


                                                              А писать свою стд и тасказть за собой — у многих разных разработчиков "разные" библиотеки хелперов, и дружить их такое себе занятие.

                                                0

                                                Проблема в том, что многие базовые знания никто не оценивает на собеседованиях, и денег за это особо не платят(точнее выходы в те места где за это платят часто ограниченны ещё кучей требований.

                                            +7

                                            Так я тоже не знаю.


                                            Сколько бит в байте, зависит от архитектуры. Стандарт С определяет байт как размер char, для связи которого с разрядностью тоже нужно знать об архитектуре и настройках компилятора.

                                              +2

                                              Стандарт С ISO 9899:1999 http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf
                                              определяет что в char можно записать как минимум значения 0..255 или -127..128 (0..UCHAR_MAX, SCHAR_MIN..SCHAR_MAX) 5.2.4.2.1 Sizes of integer types "Their implementation-defined values shall be equal or greater in magnitude (absolute value) to those shown, with the same sign." и что в char должно быть не менее 8 бит (CHAR_BIT 8), т.е. стандартом допускаются машины с более длинным char.
                                              Байт определен независимо от char как адресуемая единица памяти, без уточнения числа бит: 3.6 byte "addressable unit of data storage large enough to hold any member of the basic character set of the execution environment" "A byte is composed of a contiguous sequence of bits, the number of which is implementation defined"
                                              (POSIX определяет байт как октет, т.е. 8 бит)
                                              Книга комментариев к стандарту http://www.coding-guidelines.com/cbook/cbook1_1.pdf на стр 190 приводит примеры
                                              "Motorola DSP56300 which has a 24 bit word… Analog Devices SHARC has a 32-bit word" и уточняет на 191 стр, что в байте не может быть менее 8 бит "The number of bits must be at least 8, the minimum value of the CHAR_BIT macro" (в стандарте это 6.2.6.1 General сноска 40 "A byte contains CHAR_BIT bits")

                                                +5

                                                Хм, там же последняя фраза в той сноске (в 6.2.6.1/3) говорит


                                                A byte contains CHAR_BIT bits, and the values of type unsigned char range from 0 to 2CHAR_BIT− 1
                                                  0
                                                  Выходит, что в байте CHAR_BIT бит, а в char — не менее CHAR_BIT бит. Значит, в общем случае неверно, что
                                                  Стандарт С определяет байт как размер char
                                                    0

                                                    5.2.4.2.1/2 намекает на ограничение сверху, так что там, по идее, строгое равенство.

                                                      +1
                                                      То есть, такая машина невозможна в C:

                                                      1. Память — набор 16-битных ячеек, т.е. прибавляя к указателю 1,
                                                      void* next = (void*)((size_t)current+1);
                                                      получается указатель на следующий 16-битный байт.

                                                      2. Регистры есть как 16-битные (int), так и 8-битные (char)
                                                      При этом, загрузка ячейки в char урезает содержимое до младших 8 бит, как и при любых конвертациях в целый тип меньшего размера.
                                                      int* ptr;
                                                      char value = *ptr; // младшие 8 бит
                                                      int value = *ptr; // весь 16-битный байт из одной ячейки памяти.
                                                        +1

                                                        Похоже на то (по крайней мере, 8-битные регистры будут оперировать чем-то отличным от char): минимально адресуемый кусок памяти — 16 бит, значит, CHAR_BIT должен содержать 16 бит, значит, в char должно быть 16 бит (или даже «хотя бы 16 бит», если ослабить формулировку и взять вашу).


                                                        Я недостаточно хорошо знаю стандарт С, чтобы судить, разрешает ли он типы меньшие, чем char, в конкретных реализациях. В плюсах-то всё просто: есть bool с очевидно меньшим пространством возможных значений.

                                                          0
                                                          Ну хорошо, а если в машине есть 24-битные регистры (char) и 32-битные (int), а память остаётся 16-битной. В этом случае я не вижу противоречий со стандартом.
                                                            0

                                                            Тогда чему равен CHAR_BITS?

                                                              0
                                                              CHAR_BITS=16
                                                                0
                                                                the values of type unsigned char range from 0 to 2CHAR_BIT − 1.

                                                                Мне сходу не удалось найти причины char и unsigned char совпадать по размеру, но ЕМНИП это так. Так что, получается, charы могут быть только 16-битными.

                                                            +3
                                                            sizeof(char) == 1 по 6.5.3.4, поэтому не разрешает, char всегда минимум
                                                    +1
                                                    Правильно.
                                                    А ещё посмотрите, как в Си++ и в Си (в stdbool.h) определяется тип bool и как они бинарно совместимы между собой на уровне библиотек (т.е. если взять библиотеку от С и подключить к проекту с Си++). :)
                                                      +1
                                                      Ох, знали бы вы, сколько багов происходят от того, что два куска программы компилируются с разным определением bool!
                                                  0
                                                  так кандидаты не знали, сколько бит в байте

                                                  Хм… недавно была новость, что кто-то там судился с гуглом, что их на собеседовании завалили, потому что они старые были. Один из аргументов был, что интервьювер посмел допустить, что в байте 8 бит. А ведь "senior" разработчики предположительно с очень старым железом работали. А там от 6 до 40 бит могло быть.


                                                  Так что, если ваши кандидаты было достаточно в возрасте, то вы зря на них серчаете.

                                                    0
                                                    Так что, если ваши кандидаты было достаточно в возрасте, то вы зря на них серчаете.

                                                    Мопед не мой, и контора не моя — так что набирал не я. :)
                                                    Насколько я знаю, приходили в основном довольно молодые люди — лет 27-35.
                                                    И если бы кандидат просто сказал, что по-разному бывает и вот работал он на системе, где в байте 6 бит — никто бы не осерчал, я вас уверяю. Наоборот, это ж прекрасный повод обсудить разные архитектуры. Но у кандидатов просто был ступор — что, мол, за вопросы такие дурацкие, кому в здравом уме может понадобиться знание о размерах типов данных?
                                                      0
                                                      IMHO это троллинг. Популярная архитектура — 8бит.
                                                      Где используется нестандартная — менее 1% от всего?

                                                      IMHO это не причина вообще зацикливаться на этом.
                                                        +3

                                                        Да, поэтому достаточно сказать «стандарт утверждает то-то и то-то, поэтому в общем случае это зависит от целевой архитектуры и настроек компилятора, но в интересующих нас случаях это почти наверняка будет 8 бит».


                                                        Если интервьювер ожидал два слова «8 бит!», и такой ответ будет для него минусом, то лучше это выяснить сразу.

                                                      0
                                                      А вы знаете сколько бит в байте? Я вот оже думал, что знаю. Сказал что 8 — обсмеяли с пруфами.
                                                      Теперь прежде чем отвечать про биты и байты, я спрашиваю о том, какая архитектура подразумевается.
                                                        +1
                                                        Пруфы были предоставлены в железном виде, или в музей водили?
                                                        Надо было обсмеять их в ответ и спросить, когда последний раз программировали для невосьмибитной архитектуры для продакшена.
                                                          –1
                                                          Меня в википедию сводили, так что чувствую себя как девушка, которую на свидание в макдональдс пригласили. (Им это вроде бы не нравится) А так общение было целиком и полностью теоретическим и за кружечкой водки, поэтому почему нет?

                                                          До этого момента я шибко не задумывался о размерностях байтов. Думал восьмерку выбрали как наиболее удобную и о существовании невосьмерок не подозревал.
                                                            +2
                                                            А с порядком байт в многобайтных переменных вас познакомили? :) Не все архитектуры little-endian. Очень прикольно переносить какой-нибудь С/С++ с одной платформы на другую, если используются низкоуровневые фишки (например, чтобы протокол обмена реализовать).
                                                              –1
                                                              Не, про такое не рассказывали, но я сам где-то и что-то читал. Да и какой в задницу C++ если я тихонько быдлокодерствую на php? Там вообще можно с улицы прийти и сбацать.
                                                                +1
                                                                А есть ещё дополнительный и прямой код для знаковых чисел. Вояки что-то прямой код любят, как я смотрю. То ли они допкода не знают, то ли это какой-то пережиток 50-х.
                                                                Кстати, ip-адреса на big-endian построены в сокетных библиотеках. И функция переворачивания в подарок тоже предусмотрена. :)
                                                              0
                                                              Вот как раз это очень даже полезная и актуальная информация, поскольку встречается сплошь и рядом. И не только на Си возникают проблемы.
                                                                0

                                                                Есть ещё и middle endian. А тот же ARM вообще можно переключать между Big и Little.

                                                                  0
                                                                  Вы бы ещё про bom спросили.
                                                                +1
                                                                Не поверите — сейчас тоже есть всякие DSP с 32 битным char (особенно, отечественные современные копии привета из 80-х). И, что характерно, оно используется. Мы, например, такое используем прямо сейчас.
                                                              +1

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

                                                                +1

                                                                Вот кстати да. Мимоходом всегда интересуюсь, сколько различных целых значений может хранить один байт. И знаете, процентах в 30 люди не знают. Кто-то говорит, что 2^256 или 2^128. Из знающих же многие пишут 2^8 (это хороший знак, в принципе).


                                                                Как-то жаловался одному товарищу, что, может, я зря это спрашиваю. Он такой: «Да ты чо, это ж самые самые азы computer science, которые проходят на первых лекциях, их просто обязаны понимать все» — это меня немного успокоило.

                                                                  +1

                                                                  Слышал историю, как в Гугле знакомый знакомого проводил заключительное интервью с чуваком, у которого было уже 4 собеса с идеальным фидбеком.


                                                                  Он дал ему следующее задание для разогрева — есть массив из n даблов, это курс обмена USD <-> EUR по каждому из n дней. В начале есть 1 USD. Нужно ровно один раз поменять его в EUR, а потом в один из последующих дней назад в USD. Сколько может быть максимум в конце?


                                                                  Он не смог решить это за ЧАС, и чуть не попал на работу, если бы не этот знакомый знакомого.

                                                                    0
                                                                    Есть ли решение со сложностью лучше, чем O(n^2)? Может, кандидат его искал больше часа, подумав, что очевидное решение «в лоб» не подходит?
                                                                      0
                                                                      В целом я придумал решение за O(n∙logn).
                                                                      Spoiler header
                                                                      Нужно использовать двоичную кучу. Перебирая первый искомый индекс (цикл по n), выбирая в оставшейся части массива макс. элемент из кучи, и просеивая кучу, удаляя текущий элемент (log n).
                                                                        +3

                                                                        Есть же за линию решение! Идем по массиву и поддерживаем минимум. Каждый раз смотрим, является ли лучшим решение поменять в известном минимуме и назад по текущему курсу.


                                                                        Это как ваше решение с кучей, но, если цикл пустить с конца, то максимум можно просто пересчитывать за константу.

                                                                          0
                                                                          Первоначальный поиск одного минимального элемента — O(n), но как поддерживать минимум за константу, выкидывая пройденный элемент?

                                                                          Например, в массиве 1,8,12,4,1 минимум = 1.
                                                                          Когда мы выкинули первый (или последний) элемент, как за O(1) пересчитать минимум?
                                                                            +1

                                                                            Мы пересчитываем минимум в префиксе массива:


                                                                            Для массива {3, 4, 2, 5, 1} — минимумы будут {3, 3, 2, 2, 1}. Пересчитывается тупо cur_min = min(a[i], cur_min).


                                                                            А потом для каждого элемента сначала берем предыдущий минимум, а потом текущий элемент.


                                                                            Вы уже заметили, что для каждого первого дня надо в качестве второго дня брать максимум в суффиксе массива. Аналогично можно для каждого второго дня (обмена назад) брать минимум из всех дней до него. Этот минимум для всех префиксов можно вот так за O(1) пересчитать, потому что тут каждый раз ровно один элемент добавляется в множество, по которому берется минимум.

                                                                              0
                                                                              Спасибо, стало понятно.
                                                                        +1

                                                                        Конечно. O(N), причём за 1 проход. Это пример очень простой задачи на динамическое программирования. Итерируем по дням и для каждого дня храним 2 числа: MaxUSD и MaxEUR:
                                                                        MaxEUR[k] — максимальное количество EUR, которое у нас может быть на руках на k-й день.
                                                                        MaxUSR[k] — максимальное количество USD, которое у нас может быть на руках на k-й день, при условии ровно одного обмена 1 USD -> EUR -> USD.
                                                                        c[k] — курс обмена


                                                                        0-й день — база индукции: MaxUSD[0] = 0, MaxEUR[0] = 0.
                                                                        k-й день: MaxUSD[k] = max(MaxUSD[k — 1], MaxEUR[k — 1] / c[k])
                                                                        MaxEUR[k] = max(MaxEUR[k — 1], c[k])

                                                                          0

                                                                          Вы даже более сложную задачу решили. В условии надо менять ровно один раз туда и ровно один раз обратно. Ваше же решение может менять сколько угодно раз.


                                                                          И у вас опечатка в последней строчке кода — забыли c[k] на MaxUSD[k-1] умножить.

                                                                            0
                                                                            MaxEUR[k] = max(MaxEUR[k — 1], c[k])
                                                                            Как раз это учитывает ваше предыдущее замечание: если в k-тый день меняем доллары на евро, то все предыдущие обмены игнорируются, начинаем с суммы $1 (я ещё подумал, почему граничное условие MaxUSD[0] = 0, так оно и гарантирует, что был хотя бы один обмен и сработало MaxEUR[k] = c[k]).
                                                                              0

                                                                              Согласен, был не прав.

                                                                              0
                                                                              И у вас опечатка в последней строчке кода — забыли c[k] на MaxUSD[k-1] умножить.

                                                                              Нет, не забыл. c[k] надо умножать на MaxUSD[k-1], если мы можем сколько угодно раз менять валюту. Но по условию мы можем менять только один раз, а изначально у нас был только 1 USD.

                                                                              0
                                                                              Идея интересная, и даже проще для понимания, чем суффиксы.
                                                                              0
                                                                              Ммм… Пусть у нас в массиве хранится USD/EUR. Ищем в нём самый правый по позиции максимум. Пусть это будет позиция k. Берём подмассив [0; k-1], ищем там минимум. Делим максимум на минимум, получаем количество USD на выходе. Потом ищем самый левый минимум во всём массиве, затем максимум в [k+1; n]. Считаем ещё одно соотношение максимум/минимум. Сравниваем результаты и берём больший. Где я ошибаюсь?
                                                                                0
                                                                                Контр-пример:
                                                                                3,11,2,3,10,1,3
                                                                                Лучший вариант: 2-10
                                                                                Ваш алгоритм находит 2 не лучшие пары: 1,3 и 3,11
                                                                                  0
                                                                                  Да, точно. «У любой задачи есть очевидное простое...» :-)
                                                                                    0
                                                                                    function find(x)
                                                                                    	local min,max,p0,p1,p2=x[1],1,1,1,1
                                                                                    	for i=2,#x do
                                                                                    		local v=x[i]/min
                                                                                    		if v>max then max=v p1=p0 p2=i end
                                                                                    		if x[i]<min then min=x[i] p0=i end
                                                                                    	end
                                                                                    	return max,x[p1],x[p2]
                                                                                    end 
                                                                                    
                                                                                      0
                                                                                      Здесь не выполнено требование, что нужен обмен, даже если он невыгоден.
                                                                                      Тестовый пример: 20,10
                                                                                        0
                                                                                        Нет просто обмен в тот же день. 20,20
                                                                                        Но если сильно надо то можно и не выгодный обмен сделать
                                                                                        function find(x)
                                                                                        	local min,max,p0,p1,p2=x[1],0,1,1,1
                                                                                        	for i=2,#x do
                                                                                        		local v=x[i]/min
                                                                                        		if v>max then max=v p1=p0 p2=i end
                                                                                        		if x[i]<min then min=x[i] p0=i end
                                                                                        	end
                                                                                        	return max,x[p1],x[p2]
                                                                                        end
                                                                                        
                                                                                          0
                                                                                          Нет просто обмен в тот же день. 20,20
                                                                                          Это запрещено по условиям задачи.
                                                                            0

                                                                            Хммм… Так, а сколько же бит в байте?

                                                                              +1
                                                                              Так зависит от архитектуры =)
                                                                              +1
                                                                              так кандидаты не знали, сколько бит в байте

                                                                              Ну так это смотря в каком байте. Не любой байт октет.

                                                                              +5
                                                                              Скучные задачи, увы, обязательны. И для интервьюера они скучны намного больше, т.к. кандидат видит эту задачу впервые (ну или второй-третий раз), а интервьюер эту задачу видит десятый или сотый раз. Но если такую задачу не дать, а дать сразу интересную (как для Senior'a) и кандидат с ней не справится — то не ясно, то ли задача была слишком сложной (кандидат — джун или миддл), то ли кандидат слабый (даже не джун). А т.к. большинство кандидатов по уровню не выше мидла, то и до интересных задач обычно не доходит дело.
                                                                              Это из своего личного опыта говорю (как в роли кандидата, так и в роли интервьюера).
                                                                              0

                                                                              Тут у интервьюэра софт скилз на нуле. Или :) он умно дождался конца, чтобы формально отфутболить знающего идрис чувака.

                                                                              +5
                                                                              Зачетный троллинг.
                                                                                +30
                                                                                Пока читал пост, было ощушение, что вернулся на пятнадцать лет назад и сижу на лекции в университете, где понимаю только знаки препинания.
                                                                                Вероятно вашему собеседнику вы сломали всю логику собеседования и он пропустил всю часть собеседования и перешёл к шагу «попить кофе после дурацкого собеседования, как же они меня все достали»
                                                                                Всёж большинство собеседований (по собственному опыту) состоят из обязательной части, где задают очевидные вопросы и ожидают ответы в стиле ЕГЭ и дополнительной, где уже можно обсудить интересные особенности.
                                                                                  +4
                                                                                  А можно ссылку на .vimrc?

                                                                                  А вообще зачётно, в духе постов Aphyr.
                                                                                    0

                                                                                    Вечером выложу куда-нибудь, а то уже не у основной машины.


                                                                                    Конкретно для идриса там ничего особо интересного кроме https://github.com/idris-hackers/idris-vim и https://github.com/dense-analysis/ale .

                                                                                      +1
                                                                                      Статья однозначно мегазачет, а за ссылку на Aphyr вам отдельное спасибо. Я полнейший балбес, раз умудрился такое пропустить.
                                                                                      +3
                                                                                      А это какой язык-то?
                                                                                        +2
                                                                                          +4

                                                                                          Таки Idris (а то там чуть ниже ту же опечатку сделали).

                                                                                            +2
                                                                                            Вон оно чо. А я то думаю похоже на Хаскель, но не Хаскель.
                                                                                        +9
                                                                                        Я не понял — кто кого интервьюировал?
                                                                                          +2
                                                                                          А это на какую зарплату было собеседование?
                                                                                            +13

                                                                                            На зарплату старшего научного сотрудника-академика.

                                                                                            +27

                                                                                            А каким образом ваши формальные доказательства покрывают отсутствие багов в Irdis? Т.е. я много раз видел ситуацию, когда программист был 100% уверен в результате (оно не может быть другим) — а оно было, причём по самым дурацким причинам. Например, потому что в динамическом линкере именно данная последовательность бинарных байт вызывала ошибочку и перезаписывала INC на NOOP (бага, бага, закрыта в новой версии, но в продакшене старая непатченная версия). Т.е. логика нам говорит "баги нет", а ядро нам говорит "segmentation fault" для нашего бинаря.


                                                                                            Тесты — они такие...

                                                                                              +9

                                                                                              Более того, формальные доказательства не покрывают правильное понимание решаемой задачи. Если заказчик от меня веб-сайт хотел, а я ему формально верифицированную криптовалюту сделал, то толку-то.


                                                                                              А с юнит-тестов ровно по вашей логике толку примерно столько же. Все скомпилированное приложение целиком надо тестировать.

                                                                                                +3

                                                                                                На самом деле, скомпилированные юнит-тесты уже проверят этот код. Упор на слово "скомпилированные", потому что получится, что unit-test'ы — это такие неявные интеграционные тесты между компилятором, исходным текстом и ОС, где это всё запускается.


                                                                                                … Потому что может быть даже печальнее, например,


                                                                                                idris 1.irdis 
                                                                                                  File "1.irdis", line 1
                                                                                                    revDumb : List a -> List a
                                                                                                            ^
                                                                                                SyntaxError: invalid syntax

                                                                                                (да, alias irdis=python).

                                                                                                  +4

                                                                                                  Но ведь, опять же, по вашей же логике их вовсе недостаточно. Вдруг в компиляторе/линкере/етц есть баги такие, что юнит-тесты отрабатывают, а всё вместе в составе конечного приложения — нет?

                                                                                                    +1
                                                                                                    Только юнит тестов никогда не достаточно для полноценной проверки того, что всё работает в сборе. Совсем без юнит тестов тоже может быть тяжело, потому что полноценные интеграционные тесты обычно идут долго, и соответственно не дают фидбека сразу. Получается, что лучше иметь и то и другое (в идеале :))
                                                                                                      +1

                                                                                                      Ну, если всерьез говорить, то я пишу тесты, чтобы убедиться, что я правильно понял целевую задачу (этакие интеграционные тесты-спеки), и в идеале доказательства на все остальное.

                                                                                                        +2
                                                                                                        Надеюсь, вы всё-таки не используете Idris в продакшене :). Ну или у компании, в которой вы работаете, будут большие проблемы с поиском замены для Вас, когда вы уволитесь.
                                                                                                          +1

                                                                                                          Если серьёзно, то компилятор идриса к продакшену ещё не готов, и я при всей моей любви буду против использования его для чего бы то ни было достаточно серьёзного (поэтому сейчас читаю CPDT, ага).

                                                                                                            0
                                                                                                            Ну так они и в FAQ честно пишут, мол, «Idris is primarily a research tool for exploring the possibilities of software development with dependent types, meaning that the primary goal is not (yet) to make a system which could be used in production.» (С)
                                                                                                              +2

                                                                                                              Главное — чтобы Эдвин Брэди после переписывания идриса (изначально написанного на хаскеле) на идрисе не начал переписывать идрис снова. А то так никогда до продакшена и не дойдет.

                                                                                                      +8
                                                                                                      Тестирование программы может весьма эффективно продемонстрировать наличие ошибок, но безнадежно неадекватно для демонстрации их отсутствия.
                                                                                                      Edsger Wybe Dijkstra
                                                                                                        0

                                                                                                        Именно!

                                                                                                          +1
                                                                                                          Это ведь не отменяет необходимости (не совсем правильно подобранное слово) писать тесты, а ваше утверждение
                                                                                                          А они не нужны. Мы же формально доказали, что мы обращаем список.
                                                                                                          выглядит весьма категорично.
                                                                                                            +2

                                                                                                            А что добавят тесты в этом случае?


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

                                                                                                              0
                                                                                                              А что добавят тесты в этом случае?

                                                                                                              +100 к уверенности.
                                                                                                              Я не понимаю ваш код, напишите тесты для меня/интервьюера/etc
                                                                                                                0

                                                                                                                Ну уверенность дело субъективное, у меня от тестов при наличии доказательства не сильно больше не становится.


                                                                                                                А непонимание кода… Ну для него не тесты нужны.

                                                                                                                  +3
                                                                                                                  В штате компании будут работать программисты разной квалификации, да и вполне вероятно, что вы когда-нибудь уволитесь, а код-то останется.
                                                                                                                  Как ни крути, с тестами лучше, чем без тестов.
                                                                                                                  А непонимание кода… Ну для него не тесты нужны.
                                                                                                                  Но тесты могут поспособствовать понимаю.
                                                                                                                0
                                                                                                                но по этой же логике вам надо писать тесты на фреймворк тестов.

                                                                                                                Вообще-то надо. Тесты — код первого порядка и должен подчиняться всем требованиям релизного кода: стили, ревью, ограничения на выбор зависимостей (и расширений в случае Хаскеля) и наличие тестов.
                                                                                                                Другое дело, что писать тесты на внешний код — ну такое.
                                                                                                                  0

                                                                                                                  Ну вот так же и код ядра тайпчекера — внешний код.


                                                                                                                  Тут языкам с тактиками вообще хорошо, которые критерию de Bruijn'а удовлетворяют.

                                                                                                                  +2

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

                                                                                                                    0

                                                                                                                    Так доказательство корректности придется менять точно так же, как тесты.

                                                                                                                      +1

                                                                                                                      А можно автоматически проверить что доказательство по прежнему относится к этому коду?

                                                                                                                        +2

                                                                                                                        Ну, если вы поменяете реализацию существенным образом, но не поменяете доказательство, то доказательство перестанет тайпчекаться, и весь модуль не соберётся.

                                                                                                                          +1

                                                                                                                          А если недостаточным для тайпчека, но достаточным для лёгкого изменения логики?

                                                                                                                            0

                                                                                                                            Значит, вы доказали не все существенные аспекты вашего алгоритма.


                                                                                                                            Я бы даже сказал, что в этом всем формальном программировании есть обратная проблема: при не влияющих на семантику изменениях иногда (или даже часто) приходится менять доказательство. По крайней мере, в языках с явным построением proof term'а (вроде идриса).

                                                                                                                    0

                                                                                                                    Тесты не только для вас. Если в коде нет опечаток, то код работает именно так, как вы его написали. Довольно много программистов абсолютно уверенны в своем коде. Они же прочитали его 100500 раз и, может быть, в уме или на бумажке уже доказали его. Но иногда такой код все-таки делает не то, что нужно.


                                                                                                                    Ваше доказательство тут — это тоже код. Вы уверенны что нигде не допустили ошибки? Напишите-ка доказательство для доказательства?


                                                                                                                    Наличие тупо тестов, которые как пробка простые и без логики, все-таки необходимо. Во-первых, для Вас, чтобы убедится что в доказательстве нет ошибок. Во-вторых, для тех, кто ваш код читать будет, чтобы было очевидно что он делает хотя бы в некоторых случаях.

                                                                                                                      0
                                                                                                                      Ваше доказательство тут — это тоже код. Вы уверенны что нигде не допустили ошибки? Напишите-ка доказательство для доказательства?

                                                                                                                      А вы просите написать тесты для тестов?

                                                                                                                        0

                                                                                                                        Обычно тесты сильно проще той магии, что вы тут используете. Буквально input = ...; output = Call(input); Assert(output = ...).

                                                                                                                          0

                                                                                                                          Так доказываемое утверждение тоже достаточно простое. Буквально revDumb xs = revAcc xs — проще любых тестов. Или, если отталкиваться от определения обращения, foldl f init (revDumb xs) = foldr (flip f) init xs. Тоже легко прочитать и понять, что утверждается.

                                                                                                                            0

                                                                                                                            А вот само доказательство — с двумя леммами и кучей кода — ну нифига не простое.

                                                                                                                              0

                                                                                                                              А его вам проверять не надо, его машина проверит.

                                                                                                                                0

                                                                                                                                Я не очень понимаю, как эта проверка работает. Можно ли там в доказательстве написать какой-нибудь бред вида True = False, только завуалированный, и из него вывести правильность любого утверждения?

                                                                                                                                  0

                                                                                                                                  Нет, иначе толку с этих формальных доказательств-то.


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

                                                                                                                          0
                                                                                                                          Просим, и пишем.
                                                                                                                          У меня уже дважды по-крупному случалось, что тестовая среда начинала гнать false positives.
                                                                                                                          Да, может, в чём-то сами виноваты — переусложнили обстановку. Но не уверен, что более простая схема взлетела бы.
                                                                                                                          Поэтому приёмы убедиться, что тесты сами что-то проверяют — обязательны.
                                                                                                                          И это не TDDʼшное «сначала должно упасть» — нет, проверяться на это должно и давно существующее, хотя бы в характерных избранных точках и ситуациях.

                                                                                                                          Но тут существенно, конечно, что тест должен читаться в разы проще тестируемого кода. Иначе — нет смысла. В исходном постинге это явно не соблюдается…
                                                                                                                      +1
                                                                                                                      Как вы только что процитировали, тесты позволяют реально только продемонстрировать наличие ошибок. Но не их отсутствие. Что бы вы хотели ими продемонстрировать? Что код работает правильно? Так они этого не показывают (в общем случае). Что правильно работает один случайно выбранный пример?

                                                                                                                      Если мы формально доказали, то стоит обсудить доказательство, допущения, сделанные в процессе доказательства, и т.п.

                                                                                                                      А если вы не понимаете доказательство, то скорее всего вы не понимаете, что формально означает обратить список (и это в общем типично для многих нетривиальных задач) — то откуда у вас после тестов уверенность-то возьмется +100%, что задача решена верно? Для этого уж как минимум придется прикрутить что-то типа property based testing, а там снова будут доказательства, и все по-новой…

                                                                                                                      Ну то есть, что для вас субъективно это важно — верю, но это именно суббъективное чувство. У меня вот тоже от наличия тестов его не прибавляется — а только от наличия того самого «понимания кода». Тесты к нему имеют некоторое отношение, но не прямое.
                                                                                                                        +1
                                                                                                                        Как вы только что процитировали, тесты позволяют реально только продемонстрировать наличие ошибок. Но не их отсутствие. Что бы вы хотели ими продемонстрировать?

                                                                                                                        То, что код протестирован. Чем выше процент покрытия тестами, тем проще отладка. А отсутствие тестов, что демонстрирует?
                                                                                                                        откуда у вас после тестов уверенность-то возьмется +100%, что задача решена верно?

                                                                                                                        не +100%, а +100 к параметру уверенность. И не задача решена верно, а программа компилируется и запускается.
                                                                                                                          0
                                                                                                                          Чем выше процент покрытия тестами, тем проще отладка.

                                                                                                                          Смысл всей этой формальной ерунды в том, что вы формализовали спеку, доказали соответствие этой спеке, и потом вам ничего в рантайме проверять или отлаживать не надо, потому что вы уже всё доказали.

                                                                                                                            +1
                                                                                                                            >То, что код протестирован
                                                                                                                            Ну мыж только что обсудили, что это не дает гарантий? Никаких. Или вы Дейкстру процитировали, но с ним не согласны?

                                                                                                                            >А отсутствие тестов, что демонстрирует?
                                                                                                                            На мой взгляд — что кто-то дурью маялся. Не вообще, а конкретно вот тут.

                                                                                                                            Ну то есть, я хочу сказать что — бывают языки, где вы не можете доказать формально почти ничего. Бывают сложные системы, где стоимость такого доказательства запредельно велика. В таком случае я соглашусь, что лучше иметь тесты, и какое-никакое покрытие ими.

                                                                                                                            Но при возможности и наличии формального доказательства? Зачем?
                                                                                                                              0
                                                                                                                              Или вы Дейкстру процитировали, но с ним не согласны?

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

                                                                                                                              Тесты могут показать наличие ошибок, а могут и не показать, но они никогда не покажут наличие отсутствия ошибок. Акцент на второй части предложения после запятой.
                                                                                                                              Тесты практически ничего не гарантируют, кроме покрытия.
                                                                                                                              Ну то есть, я хочу сказать что — бывают языки, где вы не можете доказать формально почти ничего. Бывают сложные системы, где стоимость такого доказательства запредельно велика. В таком случае я соглашусь, что лучше иметь тесты, и какое-никакое покрытие ими.

                                                                                                                              Вот именно, дело в покрытии, а какой именно процент покрытия должен быть и на что вообще писать тесты, а на что нет — зависит от бизнеса.
                                                                                                                                +1
                                                                                                                                >Акцент на второй части предложения после запятой.
                                                                                                                                Ну я ровно так это и понимаю. Вы можете писать мало тестов, или много — но гарантии отсутствия ошибок все равно нет. При этом тесты стоят денег, и требуют времени (что где-то одно и тоже).

                                                                                                                                А тут у нас реальный, достаточно редкий на сегодня случай, когда есть формальное доказательство правильности некоторого небольшого куска кода. Ну и зачем нам вот прямо тут тесты? У нас правда нет более нужных вещей, на которые можно деньги потратить?

                                                                                                                                Скажем, запустить, и убедиться что все заработало — ну я еще могу это понять. В конце концов — померять время выполнения и потребляемые ресурсы (которые формальным доказательством не были охвачены). Ну то есть — нефункциональные тесты.
                                                                                                                                  0
                                                                                                                                  А тут у нас реальный, достаточно редкий на сегодня случай, когда есть формальное доказательство правильности некоторого небольшого куска кода. Ну и зачем нам вот прямо тут тесты? У нас правда нет более нужных вещей, на которые можно деньги потратить?

                                                                                                                                  Насколько я понял — случай выдуманный.
                                                                                                                                  Может действительно нет причин писать тест в этом случае, а может есть косвенные причины, но мы этого не знаем.
                                                                                                                                  С одной стороны имеем формальное доказательство, что задача выполнена. С другой стороны, есть достаточно явное указание на то, что решение задачи не может быть верифицировано, ввиду отсутствия тестов.
                                                                                                                                    +1
                                                                                                                                    >Насколько я понял — случай выдуманный.
                                                                                                                                    Насколько я понял, верификация обращения списка — не выдуманная ни разу.

                                                                                                                                    > мы этого не знаем
                                                                                                                                    Ну мы может и не знаем Idris, но это вообще-то не повод говорить, что он не работает.

                                                                                                                                    У нас есть доказательство работоспособности. Правильно ли оно само — я сказать не могу, но идея доказательства по крайней мере вопросов не вызывает (что левая свертка на оригинальном списке работает так же, как правая на инвертированном). Оно использует вполне фундаментальные свойства списков, и чтобы написать любой осмысленный тест (кроме самых тривиальных), вам все равно придется такие же свойства сформулировать, и проверить, что они выполняются.
                                                                                                                                      0
                                                                                                                                      Ну мы может и не знаем Idris, но это вообще-то не повод говорить, что он не работает.

                                                                                                                                      Мы не знаем по каким причинам интервьюер указывал на отсутствие тестов. Насколько я понимаю, прямых причин нет, но могут быть косвенные — установленные требования бизнеса, например.
                                                                                                                                        +1
                                                                                                                                        Вы не уловили. foldl для оригинального списка с любой функцией и любым начальным значением == foldr для инвертированного. Доказательство — это и есть тест. Берете любую пригодную функцию, и любое значение, и проверяете, что результаты идентичны. Тесты из доказательства выводятся на раз-два, по крайней мере в этом частном случае. Наоборот — далеко не так просто.
                                                                                                                                          0
                                                                                                                                          Я понимаю то, что бессмысленно писать тесты, если есть формальное доказательство в целях проверки кода.
                                                                                                                                          Но есть и другие требования бизнеса и коммуникация с другими разработчиками, я это уже писал.
                                                                                                                                          В штате компании будут работать программисты разной квалификации, да и вполне вероятно, что вы когда-нибудь уволитесь, а код-то останется.
                                                                                                                                          Как ни крути, с тестами лучше, чем без тестов.

                                                                                                                                          Толку-то если приняв оффер, на работе вы будете писать доказательства такого уровня, что их мало кто будет понимать. А тесты дублируют код, их почти всегда просто понять.
                                                                                                                                            0
                                                                                                                                            >А тесты дублируют код, их почти всегда просто понять.
                                                                                                                                            Ну вот напишите (на любом удобном языке ;) тест к данному примеру? На самом деле это нифига не просто, и понять такие тесты будет не всегда просто.

                                                                                                                                            >вы будете писать доказательства такого уровня
                                                                                                                                            Боюсь что не будете, к сожалению. На сегодня это слишком сложно для промышленного применения.
                                                                                                                  +1
                                                                                                                  unit-test'ы — это такие неявные интеграционные тесты между компилятором, исходным текстом и ОС, где это всё запускается.

                                                                                                                  Ещё стоит добавить процессор, память и всё сопутствующее, потому что в них тоже бывают баги, необнаружимые статическим анализом кода.
                                                                                                                  +9
                                                                                                                  Ну, интервьювер по глупому сказал, чтобы вы использовали любой удобный для вас язык.

                                                                                                                  А теперь представим, что он irdis не знает, следовательно в вашем коде он разобраться не может. Если предположить. что это метаязык, суто может быть и уловит, но главное было все-таки хотя бы просто запустить на нескольких примерах, чтобы увидеть что ваша программа действительно работает.

                                                                                                                  А вы этого не сделали, тестов рабочих не предоставили, просто углубились в математические формальности.

                                                                                                                  Предположим, они берут вас на работу, и просят реализовать простую вещь. В результате получают множество раз переписанный, оптимизированный и вылизанных пулл реквест, который ни разу не запускался на локальном дев енвайрнменте, и в CI он идет без единого теста, то есть первый запуск будет где-то аж на UAT, а то и вообще в PROD?
                                                                                                                    +1
                                                                                                                    А вы этого не сделали, тестов рабочих не предоставили, просто углубились в математические формальности.

                                                                                                                    А вы правда тесты ставите выше доказательств корректности алгоритмов? Речь же не об особенностях операционной семантики языка, скажем.


                                                                                                                    В результате получают множество раз переписанный, оптимизированный и вылизанных пулл реквест, который ни разу не запускался на локальном дев енвайрнменте, и в CI он идет без единого теста, то есть первый запуск будет где-то аж на UAT, а то и вообще в PROD?

                                                                                                                    Так вакансия ж на C++ была, поэтому, увы, так не получится, придётся тесты писать :(

                                                                                                                      +3
                                                                                                                      А вы снова суть не уловили.

                                                                                                                      Интервьювер правильно сказал — что вы программу даже не запустили, я уж не говорю про тесты. Тесты даже необязательно писать, просто запустить программу и показать что она обратила список, который вы туда передали аргументов, или даже захардкодили.

                                                                                                                      Если я не знаю вашего irdis, то формальному доказательству я может и поверю, но как я могу проверить что он правильно реализован с точки зрения кода?

                                                                                                                      Ведь нельзя сказать, что любой математик, который может формально доказать теорему пифагора, способен запрограммировать ее решение?
                                                                                                                        –1
                                                                                                                        Тесты даже необязательно писать, просто запустить программу и показать что она обратила список, который вы туда передали аргументов, или даже захардкодили.

                                                                                                                        Зачем? Какую дополнительную информацию это даёт, при условии, что вы знаете Idris?


                                                                                                                        Если я не знаю вашего irdis

                                                                                                                        А если не знаете, то какая разница, запустил я программу или нет? Может, я там в обработке нажатий от клавиатуры системную функцию reverse вызвал, а не свои эти вот, и она все ваши проверки отработает. Или захардкодил входной список и захардкодил выходной.


                                                                                                                        то формальному доказательству я может и поверю, но как я могу проверить что он правильно реализован с точки зрения кода?

                                                                                                                        А вам не надо это проверять. Реализацию проверяет сам язык (в этом вся прелесть proofs-as-terms и тайпчекинга).


                                                                                                                        Утверждение, которое доказывается, во-первых, ИМХО, достаточно читабельно. Во-вторых, даже если я сильно ошибаюсь, то чем тесты лучше? Может, опять же, я там захардкодил ответ на пару входных списков, и где-то в коде у меня что-то вроде


                                                                                                                        if input == "1 2 3" then print "3 2 1"
                                                                                                                        if input == "1" then print "1"

                                                                                                                        Ведь нельзя сказать, что любой математик, который может формально доказать теорему пифагора, способен запрограммировать ее решение?

                                                                                                                        Нельзя, конечно. Но если математик доказал, что запрограммированное решение правда решает теорему Пифагора (что бы это ни значило), то этому верить, наверное, можно, по меньшей мере, с той же уверенностью, что и тестам?

                                                                                                                          +4
                                                                                                                          С таким подходом я нисколько не удивляюсь, что не позвонили. Они просто сразу поняли весь спектр возможных проблем, начиная с межличностных.
                                                                                                                            0

                                                                                                                            А если вас попросят написать тесты для фреймворка тестов на интервью, вы это тоже с радостью сделаете или будете отказываться?


                                                                                                                            Я не очень люблю делать бессмысленные действия, и, действительно, лучше это выяснить сразу. Не назвал бы это межличностной проблемой, впрочем.

                                                                                                                              +2
                                                                                                                              А завтра вам в голову придёт, что весь продукт компании, над которым вам предстоит работать — бессмысленный. Не стоит вам с таким подходом вообще наниматься на работу.
                                                                                                                                0

                                                                                                                                Вы абсолютно правы, и вопрос о том, связан проект с какой-то ерундой, или же им заниматься интересно, он важный.


                                                                                                                                Впрочем, если уж мы заговорили об этом… Вы никогда не задаётесь вопросами целесообразности того, что вам предлагают делать?

                                                                                                                                +1
                                                                                                                                Всё не просто, а очень просто. Что-то доказывать нужно человеку, а не компилятору. Потому что именно он принимает решение и берёт на себя ответственность. И если что, фейсом по клаве будут возюкать его. Ну а потом он будут делать тоже самое с тобой. И есть вероятность, что все остальные тоже присоединятся к этому увлекательному действу. Даже те, кто плюсовал карму и ржал в комментах. Ну я вот тоже ржал — смешно же. По не позвонил бы.
                                                                                                                                Потому что вся статья это просто попытка поднять чсв за чужой счет. А нарциссизм он того — до добра не доводит. Потому что всегда нужно помнить одну простую вещь — даже теория относительности относительна.
                                                                                                                                А тут какие-то формальные доказательства, безоглядная надёжа на компилятор, и вера в постановщика задачи, ну и задранное чсв.
                                                                                                                                В общем, я бы не взял такого сотрудника, ибо страшно далёк он от реальности.
                                                                                                                                  0
                                                                                                                                  безоглядная надёжа на компилятор, и вера в постановщика задачи

                                                                                                                                  Вера в тесты, получается, лучше?

                                                                                                                                    0
                                                                                                                                    Нееет, дело не в вере, а в ответственности. А ответственность на вере это такая зыбкая штука. А у тебя получается вера. Вера в формальное доказательство правильности решения, в правильность задачи, в яп, в компилятор/интерпретатор, библиотеки и тд. Вера, как известно, не приемлет логики. Критерий истины — практика. Поэтому тебя и спрашивают " где тесты, Карл?". Где результат?
                                                                                                                                    «не верю (с)»
                                                                                                                                      0
                                                                                                                                      Где результат?

                                                                                                                                      Вон терм нужного типа, он тайпчекается. Вот и результат. Вполне себе на практике.


                                                                                                                                      " где тесты, Карл?"

                                                                                                                                      А в чём их смысл при таких вводных-то? Ведь то, что тесты проходят, опирается на веру в компилятор/интерпретатор, библиотеки, фреймворк тестов и прочее подобное.

                                                                                                                                        0
                                                                                                                                        Насколько я понял Kemet и некоторых прочих комментаторов, они пытаются указать на разницу между текстом программы и собственно программой. Программа является рабочей, если она хоть раз выполнила своё предназначения, иначе она просто объект современного искусства. Так что в описанной ситуации программу стоило бы хоть раз запустить.
                                                                                                                                          0

                                                                                                                                          А чем запуск тайпчекера на тексте программы принципиально отличается? Вы же не маркером на доске доказательство пишете, а в виде кода в компьютере, и проверку этого доказательства в том или ином виде регулярно запускаете.

                                                                                                                                            0
                                                                                                                                            Сермяжностью, прикладным характером. Запустил программу — получил развёрнутый лист, программа работает. Всё предельно понятно.
                                                                                                                                              0
                                                                                                                                              Вы же не маркером на доске доказательство пишете, а в виде кода в компьютере, и проверку этого доказательства в том или ином виде регулярно запускаете.

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

                                                                                                                                                По коду, написанному маркером на доске, тайпчекер не пробегается, и машина его корректность не проверяет.

                                                                                                                                    +2
                                                                                                                                    Вы, видимо, не до конца понимаете задачу тестов. Они нужны не для того, чтобы доказать корректность алгоритма, а чтобы, как минимум, обезопасить код и проект от неочевидных ошибок при изменении реализации.

                                                                                                                                    Вы вот взяли и написали такой крутой алгоритм разворота списка. Доказали его формально. Залили на прод. А завтра пришел программист Вася, у которого с математикой всё не так хорошо, и добавил/изменил пару строчек. И сразу вылил, тестов же нет. А на следующий день боевой сервер упал и фирма потеряла 100500 тысяч долларов.

                                                                                                                                    Любая мало-мальски крупная разработка, в первую очередь, про безопасность и тройные проверки, которые, с вашей точки зрения, бессмысленные.
                                                                                                                                      0
                                                                                                                                      чтобы, как минимум, обезопасить код и проект от неочевидных ошибок при изменении реализации.

                                                                                                                                      «Тестирование программного обеспечения не может доказать, что система, алгоритм или программа не содержит никаких ошибок и дефектов и удовлетворяет определённому свойству. Это может сделать формальная верификация.» (С)
                                                                                                                                      И сразу вылил, тестов же нет. А на следующий день боевой сервер упал и фирма потеряла 100500 тысяч долларов.

                                                                                                                                      Ну если в фирме считается нормальным «сразу выливать» без пул-реквестов и код-ревью, то поделом.
                                                                                                                                        +1
                                                                                                                                        Ну а если код ревью может сделать единственный математик в компании, а потом он уволится, что делать?
                                                                                                                                          0
                                                                                                                                          Нанять больше математиков )))
                                                                                                                                        +2

                                                                                                                                        Вы, видимо, не до конца понимаете суть формальных доказательств.


                                                                                                                                        Доказательства — они там, рядом, в том же файле, что и основная реализация, и проверяются при каждой сборке. У вас физически не получится изменить реализацию так, что доказательство станет ложным, и при этом что-то куда-то вылить: модуль просто не соберётся.


                                                                                                                                        Спасибо за ваш комментарий, я стал чуть лучше понимать суть претензий.

                                                                                                                        0

                                                                                                                        Хм, а тут разве односвязный список используется?

                                                                                                                          0

                                                                                                                          Да, канонический односвязный список.

                                                                                                                          0
                                                                                                                          Подумали, что overqualified.
                                                                                                                            +6
                                                                                                                            Даже не просто overqualified, а что то уровня профессора computer science, который почему то пришёл на позицию junior programmer, с которой он сбежит на следующий же день.
                                                                                                                              0
                                                                                                                              что то уровня профессора computer science

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

                                                                                                                            +8

                                                                                                                            Кажется, я видел похожий пост, только там, как в анекдоте, не "развернуть список", а "решить FizzBuzz", и не "функциональное программирование", а "машинное обучение", и не "тесты не нужны — мы формально доказали", а "надо было взять более глубокую нейронную сеть": https://habr.com/ru/post/301536/

                                                                                                                              +3

                                                                                                                              О, прекрасно, спасибо! Я как раз, наконец, начал писать пост про формальную верификацию fizzbuzz.

                                                                                                                                0
                                                                                                                                В копилку, тоже замечательный пост про дурацкий вопрос:
                                                                                                                                habr.com/ru/post/301924
                                                                                                                                0
                                                                                                                                а «решить FizzBuzz»

                                                                                                                                Мне больше нравится вот это решение FizzBuzz'a FizzBuzzEnterpriseEdition. там, конечно, не машинное обучение, но тоже доставляет.
                                                                                                                                  +1
                                                                                                                                  Я сейчас обратил внимание, что на гитхабе используется коричневый цвет для обозначения java-кода. Совпадение?
                                                                                                                                    +1
                                                                                                                                    Разруха не в клозетах языках, а в головах! (с) Собачье сердце

                                                                                                                                    Говнокодить и оверэнженерить можно на любом языке, так же практически на любом современном высокоуровневым мало-мальски популярном языке можно писать хороший и эффективный код.

                                                                                                                                    Тот же FizzBuzzEnterpriseEdition можно переписать абсолютно на любом языке.