Всем привет. Меня зовут Андрей, и сегодня я хотел бы обсудить тему оценки и доказательства свойств программных решений. В чем состоит задача программиста? Один из самых популярных ответов – предоставлять некоторое решение существующей проблемы. Неотъемлемой частью этого процесса является стадия анализа разработанного решения, в которой мы пытаемся понять, что за решение мы получили, какие у него ограничения, область применения, и на какие компромиссы оно идет, то есть насколько хорошо оно решает изначальную проблему и сколько других проблем добавляет.
На сегодняшний день большая часть анализа протекает в неформальных терминах: «это ненадежное решение», «это плохо читаемый код», «плохо тестируется» и так далее. Для формального анализа в большинстве случаев мы используем различные виды тестов, основанные на тест-кейсах. Неформальный анализ нас сейчас не интересует, так как он имеет большее отношение к философии и софистике, нежели к точным наукам. Поэтому давайте сконцентрируемся на тестировании, взглянув на него именно с точки зрения точной науки, то есть математики.
Математики, как и программисты, создают решения и анализируют их. Возьмем для примера анализ функций (они ближе всего к программам). Что такое тест-кейс с точки зрения анализа функции? Это некоторая точка (входное значение) функции. Сам же тест, соответственно, представляет собой анализ поведения функции в этой точке (причем, точки обычно выбираются не случайно, а на разных участках с разным поведением функции – для этого, как правило, используется информация по покрытию кода).
Исследование поведения функции в некоторых важных точках – неотъемлемая часть математического анализа. Однако математики также уделяют много времени анализу свойств, справедливых на всей области определения, например, функция сложения ассоциативна, коммутативна и так далее.
Программы, как и математические функции, в большинстве случаев определены на очень большом числе значений (близком к бесконечному). Но программисты по какой-то причине не интересуются свойствами своих программ за пределами конкретных точек (тест-кейсов). Получается, что о поведении программы в остальных точках мы не можем сказать ничего определенного. Как это исправить?
Простой пример
Давайте рассмотрим для начала пример, взятый из базовой арифметики, а потом перейдем к более практической ситуации. Возьмем обыкновенное сложение. Как я уже упоминал, сложение обладает многими свойствами. К примеру, сумма двух неотрицательных чисел всегда больше каждого из слагаемых.
То есть, для любых a
и b
больших или равных нулю справедливо a + b >= a && a + b >= b
. На Javascript данное свойство можно записать в качестве функции:
function(a, b) {
return a + b >= a && a + b >= b;
}
Осталось только доказать это свойство. Какие у нас есть варианты:
Пойти математическим путем – обложиться Coq/Agda/TLA+/Lean Prover и другими штуками для доказательства теорем, и через пару лет мы, возможно, сможем проверить это свойство.
Как и всегда в программировании, мы можем, в отличии от математиков, чуть срезать углы и просто проверить это свойство очень много раз на разных значениях.
Сделать это довольно просто. Для начала напишем генератор необходимых значений:
function genPosNumber() {
return Math.random() * 10000000000
}
Затем напишем функцию, которая принимает генератор и свойство и конструирует проверку свойства:
function property(argGenerators, propertyFn) {
return function () {
var generatedArgs = argGenerators.map((gen) => gen())
return {
success: propertyFn(...generatedArgs),
args: generatedArgs,
}
}
}
Ну и саму функцию, которая будет проверять свойство заданное количество раз (по умолчанию 100):
function check(property, tries = 100) {
for (var i = 0; i < tries; i++) {
var res = property()
if (!res.success) {
throw new Error('Property hasnt held on arguments: ' + JSON.stringify(res.args, null, 2))
}
}
}
Теперь мы можем написать тест на наше свойство:
it('forall a, b - a + b >= a && a + b >= b', () => {
check(
property([genPosNumber, genPosNumber], function (a, b) {
return a + b >= a && a + b >= b
}),
)
})
Возникает вопрос: а надо ли было что-то писать, или все уже написано до нас? Ответ – да, все уже написано.
Данный подход называется property-based testing (а.к.a QuickCheck тесты, property тесты, генеративное тестирование), появился он в haskell сообществе. На сегодняшний день его реализации есть практически для всех языков и, конечно же, для Javascript. В примерах я буду использовать встроенный в Jesttestcheck-js, который на самом деле является биндингом к test.check написанному на ClojureScript. Наш пример с его использованием запишется так:
var testcheck = require('testcheck')
var gen = testcheck.gen
it('forall a, b - a + b >= a && a + b >= b', () => {
testcheck.check(
testcheck.property([gen.posInt, gen.posInt], function (a, b) {
return a + b >= a && a + b >= b
}),
)
})
В целом, практически ничего не изменилось, кроме использования уже готовых функций и генераторов вместо самописных. Перейдем к примеру посложнее.
Пример посложнее
Фронтенд почти всегда оперирует сущностями, которые были переданы нам с бэкенда, и зачастую для более удобного применения на фронтенде нам надо изменить их структуру. Тут все просто – у нас появляется некоторая функция convertFrom, которая конвертирует структуру (допустим, данные о семье) в удобную для отображения.
function convertFrom(structFromBackend) {
...
return structForFrontend;
}
Однако некоторые сущности не только отображаются, но и редактируются – тогда нам надо добавить также функцию convertTo. Она переведет структуру из представления фронтенда в исходную, которую мы сможем сохранить на бэкенде.
function convertTo(structForFrontend) {
...
return structFromBackend;
}
Наверное, вы уже заметили некоторое свойство этих двух функций: convertTo
–обратная функция для convertFrom
. То есть для любых a
справедливо, что convertFrom(convertTo(a))
эквивалентно a
.
Давайте запишем это свойство на Javascript:
function isRevertable(structFromBackend) {
var structForFrontend = convertFrom(structFromBackend)
var structForBackend = convertTo(structForFrontend)
expect(structFromBackend).toEqual(structForBackend)
}
Теперь необходимо написать генератор для structFromBackend
. Testcheck
уже имеет большой набор встроенных генераторов, комбинируя которые, мы можем получать новые генераторы. Пример:
gen.int // генератор целых чисел
gen.array // генератор массивов
gen.array(gen.int) // генератор массивов целых чисел
Из чего состоит наша структура (данные о семье):
type
– может бытьespoused
,single
,common_law_marriage
,undefined
;members
– массив объектов с такой структурой:role
– может бытьsibling
,child
,parent
,spouse
;fio
– объект с ключамиfirstname
,lastname
,middlename
;dependant
–boolean
илиundefined
.
Начнем с type
, воспользуемся документацией по генераторам.
Для перечислений используется генератор returnOneOf:
gen.returnOneOf(['espoused', 'single', 'common_law_marriage', undefined])
Теперь самое сложное – генератор объекта member
. Генератор для role
сконструируем с помощью уже использованного returnOneOf
:
gen.returnOneOf(['sibling', 'child', 'parent', 'spouse'])
Для dependant
используем генераторы gen.boolean, gen.undefined, скомбинировав их при помощи gen.oneOf:
// oneOf принимает несколько генераторов и возврашается генератор который
// случайным образом использует то один то другой генератор
gen.oneOf([gen.boolean, gen.undefined])
Для fio
используем gen.object в комбинации с gen.string, gen.undefined:
gen.object({
firstname: gen.oneOf([gen.string, gen.undefined]),
lastname: gen.oneOf([gen.string, gen.undefined]),
middlename: gen.oneOf([gen.string, gen.undefined]),
})
Сведем все вместе:
var familyInfoGen = gen.object({
type: gen.returnOneOf(['espoused', 'single', 'common_law_marriage', undefined]),
members: gen.array(
gen.object({
role: gen.returnOneOf(['sibling', 'child', 'parent', 'spouse']),
fio: gen.object({
firstname: gen.oneOf([gen.string, gen.undefined]),
lastname: gen.oneOf([gen.string, gen.undefined]),
middlename: gen.oneOf([gen.string, gen.undefined]),
}),
dependant: gen.oneOf([gen.boolean, gen.undefined]),
}),
),
})
Проверяем:
var sample = require('testcheck').sample
console.log(JSON.stringify(sample(familyInfoGen, { times: 2 }), null, 2))
/*
[
{
"type": "espoused",
"members": []
},
{
"members": []
}
]
*/
А вот и первая проблема. Иногда у нас генерятся структуры без супруги, но при этом с type === 'espoused'
. Так быть не может – нам не могут прийти такие данные с бэкенда. Как можно ограничить или преобразовать нашу генерируемую последовательность по какому-то правилу? Варианта два:
- suchThat — фильтрует генерируемую последовательность по предикату. Не очень подходит, так как увеличивает число попыток генерации, что замедляет тесты;
- map — отображает элементы генерируемой последовательности согласно некоторой функции.
Давайте посмотрим, как мы можем применить map
для наших целей. Для начала определимся с правилами:
- Супруга может быть только одна;
- Если она есть, то
type === 'espoused'
; - Если
type !== 'espoused'
, то ее быть не должно.
Так и запишем:
function mapFamily(familyObject) {
// находим всех супруг
var spouse = familyObject.members.filter((member) => member.role === 'spouse')
// если женат, а супруги нет
if (familyObject.type === 'espoused' && spouse.length === 0) {
return {
type: familyObject.type,
members: [
// то добавляем ее
{ role: 'spouse', fio: {} },
...familyObject.members,
],
}
// если не женат, а супруга есть
} else if (familyObject.type !== 'espoused' && spouse.length !== 0) {
return {
type: familyObject.type,
// убираем ее
members: familyObject.members.filter((member) => member.role !== 'spouse'),
}
// если супруг больше одной, то оставляем только первую
} else if (spouse.length > 1) {
return {
type: familyObject.type,
members: familyObject.members.reduce(
(acc, member) => {
if (member.role !== 'spouse' && acc.hasSpouse) {
acc.members.push(member)
} else if (member.role === 'spouse' && !acc.hasSpouse) {
acc.members.push(member)
acc.hasSpouse = true
}
return acc
},
{ members: [], hasSpouse: false },
).members,
}
}
// если структура верна, то возвращаем, ничего не меняя
return familyObject
}
Применим эту операцию к нашему генератору:
var familyInfoGenFixed = gen.map(mapFamily, familyInfoGen)
Проверяем:
console.log(JSON.stringify(sample(familyInfoGenFixed, { times: 2 }), null, 2))
/*
[
{
"type": "espoused",
"members": [
{
"role": "spouse",
"fio": {}
}
]
},
{
"type": "common_law_marriage",
"members": [
{
"role": "child",
"fio": {
"firstname": "&",
"lastname": "",
}
}
]
}
]
*/
Теперь генерируемые объекты точно соответствуют нашим требованиям –можно переходить непосредственно к проверке нашего свойства. Воспользуемся хелпером из пакета jasmine-check
check.it
–он принимает описания свойства, массив генераторов и свойство в виде функции.
require('jasmine-check').install()
check.it('convertTo is revert function for convertFrom', [familyInfoGenFixed], isRevertable)
Однако проверка нашего свойства заканчивается безуспешно:
● convertFrom and convertTo properties
› convertFrom -> convertTo save original shape (
{"type":"single","members":[{"role": "sibling", "fio": {}}]}
)
expect(received).toEqual(expected)
Expected value to equal:
{"type":"single","members": Array [
{"role": "sibling", "fio": Object {}}
]}
Received:
{"type":"single","members": Array [
{"role": "sibling", "fio": Object {}, "dependant": false}
]}
Difference:
- Expected
+ Received
Object {
"type":"single"
"members": Array [
Object {
"role": "sibling",
"fio": Object {},
+ "dependant": false
}
]
}
Все дело в том, что функция convertFrom
, помимо преобразований из одной структуры в другую, также проставляет некоторые значения по умолчанию (для dependant
это false
), то есть она не оставляет исходные значения. Что же делать?
Решение №1 — сложное
Дальше будет много кода, написаного на коленке в течение короткого промежутка времени в качестве Proof of concept. Данный код представлен только для того, чтобы показать некоторую идею, а не быть готовым для реального применения.
Первое, что приходит в голову – да, сами значения меняются, но структура-то остается прежней. Следовательно, мы можем ослабить свойство и проверять не на точное равенство, а на то, что структура не изменяется:
function isSameShape(structFromBackend) {
var structForFrontend = convertFrom(structFromBackend)
var structForBackend = convertTo(structForFrontend)
expect(checkFamilyStruct(structForBackend)).toBe(true)
}
Осталось только написать функцию checkFamilyStruct
.
Хм, а если подумать? Вспомните, ведь мы уже описывали структуру наших данных. В генераторе мы описали и типы, и различные ограничения для нашей структуры (в mapFamily
). Можем ли мы как-то переиспользовать создание нашего генератора для проверки структуры результата? Скорее всего, нет. Для этого понадобится анализировать внутреннюю структуру генератора, а она довольно непростая (так как он сам написан на ClojureScript).
Однако мы можем сделать то, что так любят делать программисты – придумать новое API определения структуры данных, при помощи которого мы сможем получать и функцию-генератор, и функцию-валидатор. И давайте сделаем его похожим на React.PropTypes, ведь все мы так любим React.
Единственным новым методом будет .invariant
, который будет отвечать за преобразование генерируемой последовательности (вспоминаем метод .map
).
Использование нашего API должно выглядеть так:
const makeFamilySpec = (spec) =>
spec
.shape({
type: spec.oneOf(['espoused', 'single', 'common_law_marriage']),
members: spec.arrayOf(
spec.shape({
role: spec.oneOf(['sibling', 'child', 'parent', 'spouse']).isRequired,
fio: spec.shape({
firstname: spec.string,
lastname: spec.string,
middlename: spec.string,
}),
dependant: spec.bool,
}).isRequired,
),
})
.invariant(mapFamily)
Соответственно, теперь нам надо определить объект spec
для валидатора и для генератора. Для валидации я буду использовать expect из Jest просто потому, что это единственное, что было под рукой. Очевидно, что для валидации можно использовать любую библиотеку для проверки данных, да и сам формат описания структуры может быть любым.
Для начала определим общую структуру API для валидатора:
const jestSpec = {
// specJest просто некоторая обертка, которая добавит все необходимые методы
string: specJest((actual) => expect(isString(actual)).toBe(true)), // для примитивов проверяем просто типы
bool: specJest((actual) => expect(isBoolean(actual)).toBe(true)),
oneOf: (list) => specJest((actual) => expect(list).toContainEqual(actual)),
shape: (shape) =>
specJest((actual) => {
expect(isPlainObject(actual)).toBe(true)
keys(shape).forEach((key) => {
// для объекта проверяем, что все ключи соответствуют описаниям
shape[key](actual[key])
})
}),
arrayOf: (itemSpec) =>
specJest((actual) => {
expect(isArray(actual)).toBe(true)
// для массива проверяем элементы, которые содержатся в нем
actual.forEach((item) => itemSpec(item))
}),
}
Теперь давайте сделаем то же самое для генератора:
export const genSpec = {
// specGen просто некоторая обертка, которая добавит все необходимые методы
string: specGen(gen.asciiString),
bool: specGen(gen.boolean),
oneOf: (list) => specGen(gen.returnOneOf(list)),
shape: (shape) => specGen(gen.object(shape)),
arrayOf: (itemSpec) => specGen(gen.array(itemSpec)),
}
Далее необходимо реализовать сами обертки, которые будут добавлять необходимые методы. Так как большая часть кода и для валидатора, и для генератора будет общей – вынесем ее в функцию makeSpecable
. Она будет принимать 2 функции, которые уже будут содержать логику, специфичную для генератора или валидатора:
makeNotRequired
— определит, как сделать из того, что нам передали, необязательный генератор/валидатор.
Здесь все довольно просто. Для валидатора:
;(check) => (actual) => isUndefined(actual) || check(actual)
Для генератора:
;(generator) => gen.oneOf([gen.undefined, generator])
makeInvariant
— определит как добавить ограничение по некоторой кастомной функции для генератора/валидатора
Для генератора мы такое уже делали – используем знакомый .map
:
;(generator, func) => gen.map(func, generator)
А вот с валидатором все сложнее. Давайте вспомним, что, по сути, делает mapFamily
? Приводит структуру к верному виду. А что она делает для структуры, которая не содержит нарушений? Правильно, ничего, она никак ее не меняет. Следовательно, мы можем сделать проверку – если mapFamily
ничего не изменила, значит, структура была верной:
expect(mapFamily(familyStruct)).toEqual(familyStruct)
Вооружившись этой идеей, напишем makeInvariant
для валидатора:
;(check, func) => (actual) => {
expect(func(actual)).toEqual(actual)
check(actual)
}
Ну и теперь осталось написать только makeSpecable
, которая будет добавлять необходимые методы:
const makeSpecable = (makeNotRequired, makeInvariant) => (specable) => {
const notRequired = makeNotRequired(specable)
notRequired.isRequired = specable
notRequired.invariant = (func) => makeInvariant(specable, func)
return notRequired
}
Проверяем:
const checkFamilyStruct = makeFamilySpec(jestSpec)
const generatorFamilyStruct = makeFamilySpec(genSpec)
describe('convertFrom and convertTo properties', () => {
check.it(
'convertFrom -> convertTo save original shape',
[generatorFamilyStruct],
(structFromBackend) => {
const structForFrontend = convertFrom(structFromBackend)
const structForBackend = convertTo(structForFrontend)
checkFamilyStruct(structForBackend)
},
)
})
Ура, заработало! Гист с полным кодом
Вообще, идея иметь одно описание данных и по нему получать и валидаторы, и генераторы придумана, конечно же, не мной. Именно на этом базируется довольно новая технология – clojure.spec, которая, в свою очередь, черпала вдохновение из системы контрактов Racket.
Еще дальше идет проект Automatic annotations для все той же Clojure. Ребята предлагают динамически анализировать юнит-тесты, вычислять по ним возможные ограничения на данные и далее использовать их как для compile-time проверок при помощи core.typed (система опциональной типизации для Clojure), так и для run-time проверок при помощи clojure.spec
.
С другой стороны, в Haskell сообществе существуют подходы, при которых тесты, проверяющие свойства, генерируются по типам в программе. Вот интересный доклад на эту тему.
Как типы могут помогать писать тесты, так и тесты могут помочь писать типы –между ними явно есть какая-то связь.
Такие решения позволяют проверять простые ограничения (например, что мы не передаем строки в функцию сложения чисел) статически – и получать мгновенный отклик, а сложные свойства(вроде того, что при любых операциях баланс пользователя не должен быть отрицательным, или то, что сериализация и десериализация любого типа возвращает исходный объект) – проверять динамически при помощи генеративных тестов (что, конечно, более медленно, но зато без необходимости использовать сложные системы типов, включающие dependant и refinement типы).
Какие, какие типы?
Люди, знакомые с языками со статической системой типов, возможно, уже могли заметить схожесть спецификаций, которые мы использовали для описания структуры семьи пользователя, с описанием типов в статических языках.
Сравните:
const makeFamilySpec = (spec) =>
spec
.shape({
type: spec.oneOf(['espoused', 'single', 'common_law_marriage']),
members: spec.arrayOf(
spec.shape({
role: spec.oneOf(['sibling', 'child', 'parent', 'spouse']).isRequired,
fio: spec.shape({
firstname: spec.string,
lastname: spec.string,
middlename: spec.string,
}),
dependant: spec.bool,
}).isRequired,
),
})
.invariant(mapFamily)
С кодом на TypeScript:
interface familySpec {
type?: 'espoused' | 'single' | 'common_law_marriage';
members: Array<{
role: 'sibling' | 'child' | 'parent' | 'spouse',
fio?: {
firstname?: string,
lastname?: string,
middlename?: string,
},
dependant?: boolean,
}>;
}
Согласитесь, эти две декларации крайне схожи по смыслу, хотя синтаксис и разный. Да и наше свойство мы можем легко записать на TypeScript в таком виде:
function convertFrom(family: familySpec): familyConverted
function convertTo(familyConverted: familyConverted): familySpec
Однако в системе типов TypeScript мы никак не можем указать инвариант mapFamily
, который проверяет структуру, что очень сильно снижает полезность нашей спецификации. Но это только частные проблемы TypeScript и других подобных систем типов. Существуют refinement и dependant типы, которые позволяют статически доказывать соответствие значения некоторому предикату. Простой пример — это тип «натуральные числа»:
type nat = {v : number | 0 ≤ v }
Похожим образом можно выразить и проверку структуры семьи пользователя. И это будет полностью статическая проверка, которая будет гарантированно соблюдаться во всех точках программы. Но при этом нам придется доказать компилятору, что данное свойство соблюдается везде. В случае сложных свойств это может потребовать кода больше, чем необходимо для описания логики приложения.
В итоге вся разница статических и динамических спецификаций сводится к следующему:
Статические: проверяются при помощи инструментов статической верификации, дают 100% гарантии соотвествия спецификации. Но по умолчанию считают, что ваш код не соответствует спецификации и заставляют писать много дополнительного кода для того, чтобы доказать, что код все-таки ей соответствует.
Динамические: проверяются при помощи генеративного тестирования (и других его видов), дают только вероятностную гарантию. То есть по умолчанию считается, что наш код работает согласно спецификации, и только если тестирование покажет обратное — спецификация считается нарушенной. Также нет необходимости в написании какого-либо специального кода для доказательства корректности нашего кода.
Нет никакого фундаментального противоречия между динамическими и статическими языками и системами типов.
Возможно, языки будущего вообще не будут разделяться на статические и динамические, а будут просто позволять управлять степенью строгости проверок и их количеством в процессе разработки программы.
На этапах разработки, когда корректность не очень важна (например, на этапе прототипа), мы будем довольствоваться небольшим набором свойств (частично выведенными в run-time из тестов, частично написанными нами), проверять которые будем при помощи property тестов в run-time. Постепенно переходя к этапам, когда корректность выходит на первый план (когда у нас уже много пользователей, много кода, много разработчиков), будем увеличивать количество свойств и начнем проверять их при помощи средств статической верификации (refinement и dependant типы).
В итоге одни и те же свойства мы сможем проверять как статически, так и динамически, в зависимости от того, что важнее для нас на данном этапе разработки — корректность или скорость и удобство разработки.
Решение №2 — простое
Однако мы немного отвлеклись от темы. Нашей целью было доказать, что convertTo
— функция обратная convertFrom
, но нам помешала простановка дефолтных значений. Можно ли было как-то решить эту проблему, не ослабляя требования к свойствам и без изобретения нового API?
Да, конечно, мы можем просто вынести простановку дефолтных значений в отдельную функцию setDefault
(которая будет выполняться перед или после convertFrom
) из convertFrom
, и тогда convertFrom
станет удовлетворять исходному свойству.
Иногда начинающие разработчики (такие, как я, например) при возникновении проблемы сразу бросаются писать код, который ее решает. Зачастую стоит сначала подумать: «может, проблему можно решить совсем на другом уровне?». Например, лучше разбить API модуля согласно тому, какие гарантии нам предоставляют те или иные вызовы — как в нашем случае.
По традиции, для тех, кто недостаточно устал от чтения моей статьи, дам небольшое «домашнее задание»: какому свойству может удовлетворять функция setDefault
? Напомню, что эта функция проставляет значения по умолчанию в структуре данных, если значения отсутствуют.
В чем сложности?
Несмотря на очевидную пользу, property-based тесты (а.к.a QuickCheck тесты) не имеют большой популярности среди разработчиков, даже учитывая то, что уже существует множество реализаций почти для любого языка программирования.
Причина в том, что свойства, пригодные для проверки, таким способом очень трудно выделить в типичном продакшен коде. Но почему?
Во-первых, разработчики не привыкли думать о свойствах, которые предоставляет их решение — соответственно, мы проектируем и разрабатываем систему без опоры на какие-либо свойства. TDD и BDD во многом приучили нас думать и разрабатывать отдельными сценариями — «если ввести A, то вернется B» — то есть, по сути, отдельными «точками». Очень сложно перейти от такого дискретного мышления к более непрерывному — «свойство выполняется для любого A из некоторого множества». Помочь здесь может только практика (как своя, так и чужая): пробуйте искать свойства в своем коде, смотрите как это делают другие (ниже я оставил ссылки на отличные статьи с примерами).
Во-вторых, можно было заметить, что в нашем примере исследуемые функции были чистыми (то есть без сайд-эффектов), но, к сожалению, большая часть фронтенд кода — это функции с сайд-эффектами (от походов в сеть до работы с глобальным состоянием). Общеизвестно, что функции с сайд-эффектами тестировать сложнее, чем чистые функции, определить же их свойства практически невозможно. Сайд-эффект имеет дело с чем-то, что находится за границами тестируемой сущности и обладает заведомо неопределенными свойствами, то есть его поведение непредсказуемо. Есть различные подходы, позволяющие отделять сайд-эффекты от основного кода (бизнес-логики), оставляя его чистым, однако, это тема для отдельной большой статьи.
Полезные ссылки
- Choosing properties for property-based testing — подробно разбираются множество практических кейсов для property-based тестирования (с примерами и даже картинками). Обязательна к прочтению для тех, кто хочет использовать данный подход на практике.
- JSVerify — еще одна реализация данного подхода на чистом Javascript. По возможности рекомендую использовать именно ее, так как ее намного проще отлаживать, в отличии от
testcheck-js
(стектрейсы не уводят в бесконечность ClojureScript рантайма). Имеет большой набор встроенных генераторов и поддержку асинхронных свойств. - JS.spec — биндинги к
clojure.spec
для JS. Пока очень сырые и не поддерживают из коробки генерацию по спецификациям, только валидацию. - Applying Property Based Testing to User Interfaces — хорошая статья о реальном применении property-based тестов для тестирования UI (на примере работы со стейтом пользователя). Пример описан для библиотеки Om, но в целом те же практики можно использовать и для тестирования Redux приложений.
- Unikernel Full-Stack на Erlang — веселый доклад про верификацию программ. Отвечает на вопрос: «А зачем это нужно на практике?».
- Refinement Types for TypeScript — интересный пейпер, в рамках которого создан верификатор программ на TypeScript на основе refinement типов.
- LiquidHaskell: изящные типы. — доклад, просто и понятно объясняющий refinement типы.
Напоследок хотелось бы сказать, что property-based тестирование, как и любые другие методы контроля поведения программ (статические типы, любое другое тестирование, верификация), приносят пользу даже в сам момент начала их применения, так как разработчик начинает задумываться о том, как работает его код, какие свойства и гарантии он предоставляет, и уже это позволяет выявить многие проблемы или просто прийти к лучшему решению c точки зрения архитектуры и API. Не бойтесь пытаться использовать новые практики для анализа своих программ — даже если вам не удастся их внедрить по каким-то причинам, возможно, вы начнете лучше понимать свой код.
Спасибо за внимание!
Возникшие вопросы или мысли по поводу данного подхода можно оставлять в комментариях или в твиттере — @bracketsarrows.