using System;
using System.Diagnostics.CodeAnalysis;

namespace ContractExamples;

public enum ContractKind { Precondition, Postcondition, Invariant }

public sealed class ContractViolationException : Exception
{
    public ContractKind Kind { get; }

    public ContractViolationException(ContractKind kind, string rule)
        : base($"{kind}: {rule}") => Kind = kind;
}

public static class Dbc
{
    public static void Requires([DoesNotReturnIf(false)] bool condition, string rule)
    {
        if (!condition)
            throw new ContractViolationException(ContractKind.Precondition, rule);
    }

    public static void Ensures([DoesNotReturnIf(false)] bool condition, string rule)
    {
        if (!condition)
            throw new ContractViolationException(ContractKind.Postcondition, rule);
    }

    public static void Invariant([DoesNotReturnIf(false)] bool condition, string rule)
    {
        if (!condition)
            throw new ContractViolationException(ContractKind.Invariant, rule);
    }
}