namespace ContractExamples;

public readonly record struct Reservation(int Remaining, int Reserved);

public static class Stock
{
    public static void AssertReservation(Reservation value)
    {
        Dbc.Invariant(value.Remaining >= 0, "remaining stock must be nonnegative");
        Dbc.Invariant(value.Reserved >= 0, "reserved stock must be nonnegative");
    }

    public static Reservation ReserveStock(int available, int quantity)
    {
        // PRECONDITIONS: a failure is a bug in the caller of this internal method.
        Dbc.Requires(available >= 0, "available stock must be nonnegative");
        Dbc.Requires(quantity > 0, "quantity must be positive");
        Dbc.Requires(quantity <= available, "quantity must not exceed available stock");

        // WORK: calculate a candidate result without changing shared state.
        var result = new Reservation(
            Remaining: available - quantity,
            Reserved: quantity);

        // POSTCONDITIONS: a failure is a bug in this implementation.
        // Check after the work, before returning the result to the caller.
        AssertReservation(result);
        Dbc.Ensures(result.Reserved == quantity, "reserve exactly the requested quantity");
        Dbc.Ensures(
            (long)result.Remaining + result.Reserved == available,
            "stock must be conserved");
        return result;
    }
}