Тёмный

Мощный метод проверки кода на баги 

S0ER
Подписаться 106 тыс.
Просмотров 17 тыс.
50% 1

Опубликовано:

 

29 окт 2024

Поделиться:

Ссылка:

Скачать:

Готовим ссылку...

Добавить в:

Мой плейлист
Посмотреть позже
Комментарии : 54   
@EmeraldFeed
@EmeraldFeed 2 года назад
Я понимаю что на простой задаче это можно классно расписать, но на реальной задаче я не представляю как это можно использовать. Мне всегда казалось что формальное представление программ (алгоритмов) это конечно хорошо, но дальше университета на практике вообще не применимо, ибо подобная запись сильно далека от простого человеческого понятия и никто на практике таким заниматься не будет. Было бы замечательно увидеть пример анализа на небольшом проекте :)
@ДенисДавыдов-ц6х
@ДенисДавыдов-ц6х 2 года назад
Проблема всех этих видео, со всеми этими методами - сейчас я вам покажу как эффективно делать %some% на примере hello world. А дальше hello world это конечно же работает, возможно формально описать (наверное возможно, опять же мои познания в этом небольшие) задачу, алгоритм и т.д., но в чем я уверен, так это в том, что любую реальную задачу из реально бизнеса, невероятно сложно формализовать и потребуется x3 если не больше времени на разработку, которую никто вам никогда не даст, ради того, чтобы вы там свои математические штучки расписывали. Это возможно разве, что на очень серьезных проектах, авиация, ПО для систем реального времени, реакторы там ядерные и т.д. и т.п. А в задачах даже серьезного софта энтерпрайз уровня вам врятли удастся выделить столько времени на верификацию ПО.
@VasyaFF
@VasyaFF 2 года назад
Если сделать пример из реальной жизни, то вам придётся потратить МНОГО мозговых усилий, чтобы это понять. Поэтому зрители такого контента просто не станут это смотреть. +так будет труднее применить эти знания уже в своём проекте. поэтому проще показать простой пример, а дальше уже всё зависит от вашей смекалки. Это не говоря, про авторские права на реальный пример. (есть пример, когда очень ценного сотрудника уволили за то, что на полузакрытой конференции в общей форме рассказал пример с работы)
@luckyman5983
@luckyman5983 2 года назад
Тем временем подавляющее число разработчиков: - Я не знаю как это работает, оно не ломается и ладно
@ЭнджонИгнишин
@ЭнджонИгнишин 2 года назад
Ну не знаю... Последние лет пять скорее "я знаю, как оно работает, и слава Богу что я не ошибся". А потом оказывается, что ошибся)))
@markrotko7123
@markrotko7123 2 года назад
Спасибо за видео, но не понимаю как показанное вами можно применить к реальному коду решающему бизнес задачу, буду благодарен если в одном из следующих видео это продемонстрируете. А ещё поделитесь, пожалуйста, литературой или сайтами где в подобное можно углубиться новичку.
@ПетрОкладников-ш2б
По большому счету вопрос типизации в рамках решаемой задачи является изучение (представление) изменения переменной в граничных условиях, а время разработки и качество кода будет определяться тем насколько хорошо программист (ка) будет знать эти граничные условия
@mwave3388
@mwave3388 2 года назад
Правильно! Так их! Наимпортируют библиотек всяких в питонах своих и давай абстракцию реализовывать, да код со стаковерфлоу адаптировать! То ли дело мы - настоящие погромисты, пару циклов написал - рабочий день закончился. Зато без багов.
@ДенисДавыдов-ц6х
@ДенисДавыдов-ц6х 2 года назад
Евгений, хотелось бы конечно увидеть подобного рода верификацию не формальных вещей, типа математики и типов данных, а неформальных - бизнес правил. Как можно построить мат. модель реальной предметной области, где не то что формализмом, иногда даже здравым смыслом не пахнет. "Выдавать скидку каждому 4 клиенту в 10 день после последнего полнолуния, с условием, что у клиента среди приведенных им в наш сервис пользователей есть его родственник мужского пола по имени Зина."
@goosedb4470
@goosedb4470 2 года назад
Для тебя, видимо, верификация работает каким-то магическим образом. Для того, чтобы доказать некоторые свойства программы, нужно задать аксиомы, исходя из которых можно доказать некоторые теоремы. Какие аксиомы у тебя в твоей _бизнес логике_?
@ДенисДавыдов-ц6х
@ДенисДавыдов-ц6х 2 года назад
@@goosedb4470 Спасибо большое, я понимаю, что нужно сделать для верификакации, но в том и вопрос: как определить аксиомы для реальных приложений, не игрушечных, не учебных, где предметная область сама по себе не имеет четкой формализации и очень часто в которой размытые понятия. Евгений показал нам способ как верифицировать корректность ПО, где можно довольно просто определить аксиомы, где все базируется на просто школьной математике и используются её аксиомы. Т.е. предметная область приложения показанного в видео, это инкрементирование чисел, т.е. сложение, т.е. правила предметной области в целом совпадают с правилами математики. "Какие аксиомы у тебя в твоей _бизнес логике_?". В том то и дело, если бы в реальных приложениях которые пишутся для удовлетворения потребностей реального бизнеса были бы аксиомы, то моего вопроса бы не было.
@goosedb4470
@goosedb4470 2 года назад
@@ДенисДавыдов-ц6х ну вот и не может быть формальной верификации без аксиом
@ДенисДавыдов-ц6х
@ДенисДавыдов-ц6х 2 года назад
@@goosedb4470 ну то есть метод показанный Евгением в коммерческой разработке обычных приложений, которые пишут обычные программисты - не применим.
@S0ERDEVS
@S0ERDEVS 2 года назад
Ответил в своем телеграм канале - t.me/softwareengineervlog/887
@gorbachew5598
@gorbachew5598 2 года назад
Одна проблема. Как это все успеть сделать между срочной и очень срочной задачами)
@igroykt
@igroykt 2 года назад
оооочень сложно но все таки допер. для тех кто не понял приведу более простую аналогию. чтобы выполнилось условие i>=0 марио должен идти по правой части экрана, но в случае когда i=-1 марио идет в левую часть экрана и появляется с правой части, что не попадает под условие (с точки зрения математики получается 0-1=n, где n это максимум) потому и возникает рекурсия, а i=-1 возникает как раз из-за математической коллизии)
@pavelnemoi
@pavelnemoi 2 года назад
Спасибо за видео! Метод достаточно интересен, но на практике в большинстве бизнесовых задач не особо вижу применение в связи с высокой степенью волокиты с анализом и формализацией алгоритма. Зачастую также приходится полагаться на объекты, то есть на структуры данных местами крупные и такой анализ кропотливый просто с точки зрения время затрат по мне неособо оправдан в day to day work. Думаю оттачивание практики написания тестов и достижения ими хорошего покрытия (path coverage, например), а также навык поиска и определения так называемых "edge cases" может помочь. Также можно посмотреть в сторону мутационного тестирования кода, которое тоже может хорошо выявить различного рода потенциальные бажки в критически важных для продукта местах.
@pavelnemoi
@pavelnemoi 2 года назад
Возможно, качественный стат. анализ кода также поможет избежать потенциальных багов и поможет найти граничные знач-я для тестов )
@TheRedbeardster
@TheRedbeardster 2 года назад
Про Isabelle/HOL, Coq, Lean не планируете видео?
@CatherineHicks-hy9nl
@CatherineHicks-hy9nl Год назад
Не могу понять, а как вы поднимаетесь с кейса бомжа? я пробовал пару раз и чето не пошло
@torburgmax
@torburgmax 2 года назад
не очень понятно вот что. мы потратили 5 минут на формализацию 1 переменной и цикла с ней. в идеале у нас должна вся программа быть описана математически, так? то есть это этап проектирования, который должен быть у любого хорошего софта? во сколько раз это замедляет разработку?
@IvanIvanov-wn7ep
@IvanIvanov-wn7ep 2 года назад
Ускоряет, так как экономит время на вылов багов в последствии)
@КириллКутузов-з2п
​@@IvanIvanov-wn7ep важнее выпустить продукт быстрее, чтобы быстрее охватить рынок, а уже потом заниматься рефактором
@alexandr-v
@alexandr-v 2 года назад
А может быть просто стоило бы убрать это так называемое кольцо из языков программирования, чтобы компилятор сразу ошибку выдавал. Или для чего оно нужно уж тогда?
@AlexAlex-ms3bg
@AlexAlex-ms3bg 2 года назад
11:58. Представляем типы как множество... О каких типах идет речь? О числовых и символьных? Это понятно. Структура и класс - это вроде тоже типы. Их как будем приводить к множеству и диапазону?
@IvanIvanov-wn7ep
@IvanIvanov-wn7ep 2 года назад
Тип определяется множеством значений, который объект может принимать, множеством операций, которые можно над ним производить и для объектов классов - множеством интерфейсов, к которым можно обращаться.
@AlexAlex-ms3bg
@AlexAlex-ms3bg 2 года назад
@@IvanIvanov-wn7ep Это понятно. Но вопрос был о другом - "как"
@IvanIvanov-wn7ep
@IvanIvanov-wn7ep 2 года назад
​@@AlexAlex-ms3bg я же говорю, что придётся рассматривать все множества свойств объекта: множество возможных значений, множество операций и множество интерфейсов. Если с числовыми понятно как, то что здесь непонятно? Проверять на возможность ошибок не только в плане принимаемых значений, но и в плане операций (подходит та или иная операция для объекта) и в плане интерфейсов (правильно ли объект используется другими объектами)
@unknyver
@unknyver 2 года назад
Спасибо Женя)
@mlr__roal_6867
@mlr__roal_6867 2 года назад
Было бы очень интересно послушать о том сколько ты зарабатываешь , сколько имеешь свободного времени, и про приоритеты - за какие бы деньги минимум согласился работать на неинтересной (но очень высокооплачиваемой) работе и за какие деньги минимум согласился бы работать на сверхинтересной (по твоему вкусу) работе.
@alekseyerin4191
@alekseyerin4191 7 месяцев назад
Здравствуйте, подскажите пожалуйста не могли бы Вы помочь в проблеме с кодом пожалуйста
@scarlatum
@scarlatum 2 года назад
TLDR: Не ешь суп ножом.
@dann1kid
@dann1kid 2 года назад
спасибо
@green1278dramost5
@green1278dramost5 2 года назад
Воу, компьютерная графика очень даже приятная :)
@user-df5pk9qp6k
@user-df5pk9qp6k 2 года назад
Как называется тема для KDE? Извиняюсь за оффтоп.
@kselnaag2482
@kselnaag2482 2 года назад
Это намек, что надо переходить на haskell ?
@kotikvacia9970
@kotikvacia9970 2 года назад
В чат зашел один Брагилевский
@vic7871
@vic7871 2 года назад
Спасибо!
@ДмитрийРаботягов-ц3ь
Спасибо, очень лаконично и познавательно
@snatvb
@snatvb 2 года назад
никто из рядовых разрабов(а именно они локомотивы бОльшей части кода) этим заниматься не будет, да и сеньеры тоже, только скорее увлеченные. Ты предлагаешь забивать мебельные гвоздики огромной кувалдой - это не решение проблемы. Ты затронул решение по типам, только как по мне ушел не в ту степь. На самом деле на уровне типа должно выражение 0 - 1 завершать программу с ошибкой. Для человека механизм переполнения не естественный, потому стоит его обрабатывать явно (явное лучше неявного). В твоем примере ошибка была допущена аж на этапе дизайна языка. Например rust требует такое поведение описать явно, когда ты делаешь математические операции. Хороший пример, показательный, почему люди е любят C/C++. На ровном месте отстрелил себе колено :)
@snatvb
@snatvb 2 года назад
PS вместо того чтоб бороться с человеческой природой, возможно стоит делать языки и инструменты более интуитивно понятные и ориентированные человеку(в целом тенденция сейчас такая и есть). Дизайн это и делает, так и появился UI.
@ВладиславПростяков
Сложновато, а значит нецелесообразно, ну в областях атомной энергетики , космонавтики и военной техники вполне реальный подход))
@eugenesidelnyk4600
@eugenesidelnyk4600 2 года назад
А как искать баги, связанные с многопоточностью?
@ПавелИванов-м5ю
@ПавелИванов-м5ю 2 года назад
После 10 минуты я понял что теряю время . Описанные ошибки возникают из-за того что программист не владеет языком ( и скорее всего головой) . Любая книга по языку до 2005 года начиналась с изучения типов и изучения поведения типов в подобных ситуациях , чтобы сразу дать пирожок с полки для ума , где может быть засада . Подобные ошибки я допускал где-то в первые год-два, по неопытности и 15 летнему возрасту , но не по незнанию мат части, просто тогда я ещё не допетрил до момента логирования. Проводить тесты на такие ошибки бессмысленно , надо искать грамотных людей владеющих языком , а не вот это вот всё. Даже с точки зрения бюджета это на порядок выгоднее .
@phil2964
@phil2964 2 года назад
👍👍👍👍
@crueldarkdreams
@crueldarkdreams 2 года назад
Оккама достаёт свою бритву
@kirillsushilnikov9614
@kirillsushilnikov9614 2 года назад
а я думал, что если из 0 вычесть единицу, то программа упадет. Пойду посмотрю что будет, если так сделать в Java, думаю что IllegalArgumentException будет.
@a-sher
@a-sher 9 месяцев назад
ничего не понятно, но очень интересно 😁
@ruslansitdikov1489
@ruslansitdikov1489 2 года назад
Кто-то ещё утверждает, что математика программистам не нужна?
@cccrazzz
@cccrazzz 2 года назад
Вы переехали в страну с легализированными наркотиками?
@jeszcze1raz54
@jeszcze1raz54 2 года назад
27 минут воды. В итоге баг так и не исправил. Очень мощный метод.
@nmg_prm
@nmg_prm 2 года назад
Тема не об исправлении, а о методах поиска
@IvanIvanov-wn7ep
@IvanIvanov-wn7ep 2 года назад
@Anton Shvedov принтф как раз запутал и ничего не показал в чём состоит баг.
Далее
Random Emoji Beatbox Challenge #beatbox #tiktok
00:47
КАК ЧИТАТЬ И ПОНИМАТЬ С/C++ КОД?
8:21
Анализирую NPM (начало)
20:36
Просмотров 10 тыс.