Является ли пост-условие функции действительным во всех случаях или только если функция успешна?

Question

Допустим, у меня есть следующая функция:

int reserve(DmaChannel& channel, const uint8_t request)
{
    const auto ret = channel.reserve(request);
    if (ret != 0)
        return ret;

    channel_ = &channel;
    return 0;
}

Хорошо видно, что функция может выйти из строя (когда канал занят, но здесь это не имеет значения).

Могу ли я сказать, что в документации doxygen для этой функции ее пост-условие "канал зарезервирован", предполагая, что логично, что пост-условие выполняется только в случае успешного завершения функции?Или, может быть, я должен думать о постусловиях как о чем-то, что верно в абсолютно каждом возможном возврате из функции, со значением успеха, со значением ошибки или с исключением?

Как правило, пост-условие действительно только в том случае, еслиУспешная функция может быть легко выражена с помощью предложенных контрактов C ++ 20 , например:

int reserve(DmaChannel& channel, uint8_t request)
[[ ensures ret : channel.isReserved() == true || ret != 0 ]];

Однако я не уверен, совпадает ли моя логика с общепринятым пониманиемпостусловий.