В первой части мы рассмотрели примеры тестов, из которых не все одинаково полезны. Затем попытались определиться, что же такое качество ПО, и предложили "распрямлять" код.
Теперь посмотрим, от каких ошибок защищают тесты, а от каких — другие инструменты из арсенала разработчика.
В первой части мы рассмотрели примеры тестов, из которых не все одинаково полезны. Затем попытались определиться, что же такое качество ПО, и как подходить к вопросу тестирования с системной точки зрения.
Теперь рассмотрим один из аспектов разработки, позволяющий уменьшить необходимое количество тестов — "прямолинейность" кода (как понятие, противоположное цикломатической сложности).
Сталкивались с тестами, которые толком ничего не тестируют? А тесты, которые что-то тестируют, но при этом всё равно постоянно возникают баги? Может быть, тесты, которые приходится каждый раз исправлять?
Несложно построить тест, обеспечивающий 100% покрытие, но при этом ничего не проверяющий и не гарантирующий. (См., например).
Проблемы юнит-тестов уже затрагивались на Хабре ранее:
В заметке рассматривается несколько разновидностей бестолковых тестов, а также некоторые ограничения самой идеи тестирования. А затем (в следующих частях) предлагаются разумные, на взгляд автора, меры обеспечения качества программ, включающие как уменьшение количества малополезных тестов, так и применение тестов там, где они уместны.
Это обзорная статья, в которой очень поверхностно и не подробно рассказывается о том, что такое формальная верификация программного кода, зачем она нужна и чем она отличается от аудита и тестирования.
Формальная верификация — это доказательство с использованием математических методов корректности программного обеспечения.
Формальная верификация молода. На сегодняшний день, на сайте хабр, например, нет (пока) специализации «Формальная верификация», нет специальности «Proof инженер» или «Специалист по формальной верификации». А люди, работающие по этой специальности — есть.
Программное обеспечение, которое прошло формальную верификацию считается надежным. Формальная верификация дает (с математической точностью) гарантии того, что программный код не будет содержать конкретных ошибок, что функции будут вести себя так, как ожидается.
В основе формальной верификации лежат математические методы. Слово «формальный» в названии - это отсылка к математике. Для доказательства утверждений о программном коде используются формальные методы математики: математическая логика, лямбда исчисление, теория категорий, математический анализ, алгоритмы для работы с функциональными и императивными структурами данных.
Инструменты для верификации — это программные средства для доказательства теорем (Coq, Isabelle ...), а также SAT-solvers.
В 70х годах предки формальной верификации — это доказательства простых утверждений о программе (конкретной функции) с помощью ручки и листка бумаги. Сегодня — это (иногда многолетние) исследовательские проекты для конкретного программного обеспечения, вот некоторые из них:
Привет! В первой и второй частях я поделился историей создания python библиотеки convtools (кратко: позволяет декларативно описывать преобразования данных, из которых генерируются python функции, реализующие заданные преобразования), сейчас расскажу об ускорении частных случаев datetime.strptime и datetime.strftime, а также о том интересном, что встретилось в datetime модуле по дороге.
Статья предлагает взглянуть на опыт разработки парсер комбинаторов для Python, что вылилось в библиотеку PGPC для разработки парсеров на Python. Библиотека была вдохновлена Parsec.
Особый интерес представляет эмуляция do-нотации через Python генераторы, отсюда и название библиотеки: Python Generator based Parser Combinator library.
Статья предполагает, что читатель имеет опыт работы с интерактивным программным средством доказательства теорем — Coq.
Статья является адаптированной русскоязычной версией моей статьи, написанной во время работы над формальной верификацией протокола криптовалюты Tezos.
В данной статье мы рассмотрим прием, который используется для работы с рекурсивными функциями, которые не проходят проверку завершаемости (тотальности) в Coq. Под «горючим» мы будем понимать натуральное число, которое вводится как дополнительный параметр в тело функции, чтобы обозначить верхнюю границу числа итераций, которые функция может совершить. Таким образом функция трансформируется в завершаемую, удобную для работы, и радушно принимаемую компилятором Coq. В литературе термин встречается под названиями: petrol, fuel, gas и т.д.
Положим, перед нами стоит задача: необходимо верифицировать функцию, написанную на каком-либо языке программирования. Мы разбираемся в том, что делает эта функция, уже прикидываем, какие леммы сформулируем, чтобы доказать, что она ведет себя именно так как ожидается. Переводим функцию на Coq (вручную, или с помощью автоматических переводчиков, если только таковые имеются для требуемого языка), и видим, что проверка Coq на завершаемость нашей функции (termination check) провалилась.
Это значит Coq не может определить какой аргумент на каждом шаге итерации будет уменьшаться. Можно попробовать явно указать Coq на аргумент, который, мы точно знаем будет уменьшаться на каждом шаге {struct уменьшаемый_аргумент}:
Данная статья является адаптированной русскоязычной версией моей статьи: Handling fold_left in proofs.
Функция fold_left , сворачивающая список, довольно популярна во многих (функциональных и не очень) языках программирования. Она есть и в Haskell, и в OCaml и в Rust. Используется чаще, чем fold_right, вероятно потому, что с ее помощью проще писать эффективный код.
fold_left и fold_right из библиотеки OCaml library: List.
Данная статья является адаптированным переводом моей статьи: Formalization of code in Coq - tactics, написанной в период работы над проектом coq-tezos-of-ocaml.
Суть проекта: часть исходного кода протокола криптовалюты Tezos была переведена на Coq, а затем верифицирована с помощью математических методов и формальной логики.
Статья предназначена для круга читателей, имеющих опыт работы с Coq.
Часто процесс формальной верификации становится утомительным и монотонным из за повторяющихся действий, которые пруф-инженеру (от английского слова proof - доказательство) приходится выполнять. К счастью, в Coq есть инструменты и техники автоматизации доказательств, которые позволяют не только значительно увеличить производительность, но и сделать доказательства короче.
В данной статье мы покажем, как использовать и писать тактики на примере формальной верификации исходного кода криптовалюты Tezos (написанной на OCaml), а именно, мы затронем следующие темы:
В данной статье рассматривается непопсовый метод тестирования чисел на простоту с использованием биномиальных коэффициентов. Авторы представляют алгоритм, позволяющий быстро и точно определить простые числа (но это не точно), ограничиваясь проверкой всего лишь половины биномиальных коэффициентов. Код реализации приводится на языке программирования Scala с использованием длинной арифметики. Результаты тестирования на большом наборе чисел демонстрируют эффективность и надежность предложенного метода.
В данной статье исследуется метод оценки параметров систем дифференциальных уравнений на основе неточных наблюдений. Автор проводит численный эксперимент с использованием языка программирования Scala для оценки реальных результатов и более подробного изучения предложенного алгоритма. Алгоритм оценки параметров включает подготовку данных, генерацию неточных наблюдений, использование численных методов для решения системы уравнений и оценку приближенных значений параметров. Эксперимент проводятся на системе Лоренца, и результаты оценки параметров сравниваются с реальными значениями. Заключение статьи делает выводы о применимости метода и его эффективности при оценке параметров систем дифференциальных уравнений на основе неточных наблюдений.
В данной статье рассматривается создание расширяемого алгоритма строкового калькулятора, который позволяет пользователю самостоятельно определять операции и константы, с которыми работает калькулятор. Основная цель статьи - предоставить описание процесса разработки и реализации такого алгоритма, а также продемонстрировать его гибкость и возможности для настройки под индивидуальные нужды пользователей.
Совсем недавно команда разработки Dart выпустила 3-ю версию языка, которая привнесла много новых крутых штук и возможностей. Одним из нововведений стали модификаторы классов, которые довольно сильно расширили выразительные возможности Dart. С одной стороны, новые модификаторы ложатся в стройную картину и даже логичны; с другой - чувствуется некоторая многословность ( abstract interface class вместо общепринятого interface) и появление ряда ограничений, которых ранее не было. Новые модификаторы классов безусловно интересны и требуют внимания, но сегодня мы будем говорить не о них). Оставим уже вышедшие модификаторы для одной из следующих статей. Логично задаться вопросом: о чем тогда сейчас пойдет речь? Заинтригованы? Тогда добро пожаловать под кат.
Привет, хабр!
Данная задача в разных вариациях мне давалась на нескольких собеседованиях несколько лет назад. Хоть мой дизайн и проходил, мне стало интересно реализовать это в коде с нуля. Сыроватый и сильно урезанный по функционалу MVP готов, ссылка на github будет под катом. Пока что мной запланировано 3 статьи - эта, по бэкенду и по фронту. Будет много кода на scala, много котов (cats effect), стримов (fs2), пара lock-free техник, scala js, и постараюсь сделать так, чтобы мозг от всего этого не взорвался.
Все, кому интересно - добро пожаловать под кат.
Привет! Меня зовут Сергей Грибков, я тимлид команды FM&RA в билайне, и в этом посте я хочу рассказать об одной фирменной особенности Scala под названием implicits. Это неявные параметры, неявные преобразования, неявные классы.
Почему неявные — потому что они не требуют прямого вызова, если мы говорим о методах, не требуют прямой передачи в метод, если мы говорим о параметрах, и так далее.
В Scala implicits широко распространены. Скорее всего, вы уже сталкивались с ними в различных библиотеках и фреймворках, например, Apache Spark.
Чтобы успешно использовать implicits в собственном коде и работать со сторонними библиотеками, требуется понимание принципов их работы. Поэтому давайте разберем, как всё устроено.
Итак, существует три основных категории implicits:
Любая комбинация софтвера и цифрового хардвера - от микроконтроллера, двигающего дворники у автомобиля - до серверной фермы с много-много-ядерными процессорами, аппаратными ускорителями ML и ChatGPT - сводятся к конечному автомату с достаточно большим состоянием. Независимо от сложности и адаптивности программ.
Сводится ли к конечному автомату человеческий интеллект? К сожалению, у человеческого интеллекта есть атрибут, природа которого современной науке неизвестна и который никогда не наблюдался у конечных автоматов, например у арифмометра. Этот атрибут - ощущение собственного "я", self-awareness. Конечно вы можете сделать в программе переменную "я_чувствую_собственное_я" и присвоить ей true, а потом утверждать, что вы симулируете собственное "я", но это жульничество, а не технология.
Я вовсе не пытаюсь нагонять мистику или агитировать за бога. Self-awareness наверняка такой же физический феномен, как какая-нибудь термоядерная реакция. Но скажем древние греки не знали природы термоядерной реакции. Наверное, они вели диалоги типа "если ты не веришь, что Солнце - просто большой костер из дров, то значит ты веришь в сказки про Зевса и других богов?"
Если бы Достоевский жил в наше время, смотрел по вечерам «Черное зеркало» и просто читал новости, то, скорее всего, Раскольникова судил бы Искусственный интеллект.
Сейчас довольно сложно представить, как будет выглядеть судебный процесс будущего, где условному судье не придется протирать 6 лет штаны на институтской скамье и насильно впихивать в свой мозг тонны законодательной базы. Кажется, это будет что-то коллективное и похожее на продвинутых присяжных с «закаченными» правовыми нормами, чтобы моральные аспекты при этом оставались на более близкой человеческой стороне.
Привет, Хабр, это команда Alliesverse – платформы для управления бизнесом – и это в наши воспаленные мозги попала идея о современном Раскольникове...
Случилось это на большом мероприятии, посвященному ChatGPT, на которое нас пригласили. Мы подумали: а что если ускорить наступление высокотехнологичного и справедливого суда и попробовать обучить ИИ всем российским кодексам ?
Так сформировался эмбрион LawAi by Alliesverse. Под катом, подобно ChatGPT, расскажем наш опыт обучения русскоязычных и зарубежных моделей нейросетей российскому законодательству.
Спойлер: несмотря на то, что современные системы преуспевают в нахождении экстрактивного диапазона, который отвечает на фактоидный вопрос в документе, они по-прежнему считают сложными настройки открытого домена, где модели необходимо найти свои собственные источники информации и генерировать длинные ответы.
Спойлер х2: использование ChatGPT, Notion и прочих готовых решений не подходит для создания юрисконсульта в кармане, т.к. они обучаются на международном массиве данных, у которого много расхождений с российским законодательством.
Привет! Меня зовут Никита Калинский, я разработчик в Тинькофф Бизнесе. Сейчас я занимаюсь продуктом под названием «Лента операций». Физлица в желтом приложении могут отслеживать все свои операции, и мы делаем такой же инструмент для предпринимателей.
Сегодня я хочу поговорить про основы различных систем исполнения эффектов в Scala. Мы разберем, как работают системы эффектов, как они реализованы в Scala в Cats Effects и ZIO и как эволюционировали между версиями. А также обсудим неявные особенности и подводные камни исполнения сред таких библиотек.
