Condições de entrada e retorno

Uma atualização de estoque precisa conferir duas coisas: a quantidade pedida deve estar disponível, e o saldo deve corresponder às unidades retiradas. Escreva essas condições junto à assinatura da função.

// A checkout must conserve the requested quantity and never overdraw stock.

fn remaining_stock(available: int, requested: int) -> int
    requires available >= 0
    requires requested >= 0 && requested <= available
    ensures result >= 0 && result + requested == available
{
    if requested == 0 { return available }
    available - requested
}

let remaining = remaining_stock(12, 5)
assert(remaining == 7)
assert(remaining_stock(12, 0) == 12)
print("Remaining stock: {remaining}")

requires executa antes do corpo. ensures executa depois de um retorno normal e lê seu valor por result. Cada condição deve ser booleana. Uma condição falsa gera um erro com o nome da função, a condição e sua posição no código.

Uma condição não pode sair da função verificada por return ou ?. Use um callback interno ou attempt quando a condição precisar de seu próprio fluxo de controle.

A expressão final, return e ? passam pelas verificações de saída uma única vez. A limpeza do corpo termina antes delas. Propagar Result::Err por ? também é um retorno normal; um panic ou uma tarefa que falha não executa ensures. Em uma async fn, result é o valor concluído, e a verificação termina antes de a Future ser concluída.

Escreva todos os requires antes de ensures. As condições acessam parâmetros e nomes do escopo externo; variáveis locais do corpo ficam fora de seu alcance. Funções, métodos e métodos de trait com corpo padrão aceitam contratos. Generators rejeitam contratos porque um yield não conclui o retorno. Funções assíncronas com contratos não executam em comptime.