Задавайте аксиомы для концептов

Причина

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

Пример

template<typename T>
    // Предполагается, что операторы +, -, *, и / для числа следуют обычным математическим правилам
    // axiom(T a, T b) { a + b == b + a; a - a == 0; a * (b + c) == a * b + a * c; /*...*/ }
    concept Number = requires(T a, T b) {
        { a + b } -> convertible_to<T>;
        { a - b } -> convertible_to<T>;
        { a * b } -> convertible_to<T>;
        { a / b } -> convertible_to<T>;
    };

Примечание

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

Примечание

В данном контексте аксиомы — это булевы выражения. Примеры см. в Пало-Альто TR. В настоящее время C++ не поддерживает аксиомы (даже ISO Concepts TS), поэтому некоторое время нам придётся ограничиться комментариями. Когда языковая поддержка появится, // перед аксиомой можно будет убрать.

Примечание

Концепты GSL имеют хорошо определённую семантику; см. Пало-Альто TR и Ranges TS.

Исключение

Ранние версии нового «концепта», находящегося в процессе разработки, зачастую определяют лишь простые наборы ограничений без чётко заданной семантики. Поиск хорошей семантики может потребовать времени и усилий. Неполный набор ограничений всё равно может быть весьма полезным:

// балансировщик для обобщённого бинарного дерева
template<typename Node> concept Balancer = requires(Node* p) {
    add_fixup(p);
    touch(p);
    detach(p);
};

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

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

Контроль

Искать слово «axiom» в комментариях к определению концепта

Открыть на isocpp.github.io →

template<typename T> // Предполагается, что операторы +, -, *, и / для числа следуют обычным математическим правилам // axiom(T a, T b) { a + b == b + a; a - a == 0; a * (b + c) == a * b + a * c; /*...*/ } concept Number = requires(T a, T b) { { a + b } -> convertible_to<T>; { a - b } -> convertible_to<T>; { a * b } -> convertible_to<T>; { a / b } -> convertible_to<T>; };

// балансировщик для обобщённого бинарного дерева template<typename Node> concept Balancer = requires(Node* p) { add_fixup(p); touch(p); detach(p); };