Condiciones de entrada y retorno

Una actualización de inventario debe comprobar la cantidad solicitada y el saldo restante. Use requires para las condiciones de entrada y ensures para el valor devuelto, accesible mediante el nombre result.

// 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}")

Las condiciones deben ser booleanas y se ejecutan una vez por llamada, en el orden escrito. Escriba todos los requires antes de los ensures. Una condición falsa genera un error con la función, la expresión y la ubicación en el código.

El retorno final, return y ? pasan por la misma comprobación, después de la limpieza del cuerpo. Result::Err es un retorno normal; panic y fallo de tarea no ejecutan las poscondiciones. En async fn, result es el valor completado y la comprobación termina antes de que se complete el Future.

Las condiciones pueden leer parámetros y variables del ámbito exterior, pero no variables locales del cuerpo. Los métodos y métodos de trait con cuerpo aceptan contratos. Las declaraciones sin cuerpo y los generators se rechazan. Las funciones asíncronas con contratos no se ejecutan en comptime.

Las condiciones no pueden retornar ni propagar errores fuera de la función comprobada. Use un callback interior o attempt cuando una condición necesite su propio flujo de control.