Функциональное программирование *

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

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

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

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

В первой части мы рассмотрели примеры тестов, из которых не все одинаково полезны. Затем попытались определиться, что же такое качество ПО, и предложили "распрямлять" код. Рассмотрели классификацию ошибок.

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

В первой части мы рассмотрели примеры тестов, из которых не все одинаково полезны. Затем попытались определиться, что же такое качество ПО, и предложили "распрямлять" код.

Теперь посмотрим, от каких ошибок защищают тесты, а от каких — другие инструменты из арсенала разработчика.

В первой части мы рассмотрели примеры тестов, из которых не все одинаково полезны. Затем попытались определиться, что же такое качество ПО, и как подходить к вопросу тестирования с системной точки зрения.

Теперь рассмотрим один из аспектов разработки, позволяющий уменьшить необходимое количество тестов — "прямолинейность" кода (как понятие, противоположное цикломатической сложности).

Сталкивались с тестами, которые толком ничего не тестируют? А тесты, которые что-то тестируют, но при этом всё равно постоянно возникают баги? Может быть, тесты, которые приходится каждый раз исправлять?

Несложно построить тест, обеспечивающий 100% покрытие, но при этом ничего не проверяющий и не гарантирующий. (См., например).

Проблемы юнит-тестов уже затрагивались на Хабре ранее:

• Юнит-тесты переоценены @Stormglass (оригинал);
• Почему большинство юнит тестов — пустая трата времени? (перевод статьи) @Chudilka_007 (оригинал)

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

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

Формальная верификация — это доказательство с использованием математических методов корректности программного обеспечения.

Формальная верификация молода. На сегодняшний день, на сайте хабр, например, нет (пока) специализации «Формальная верификация», нет специальности «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: