Contract precondition

Requires

A precondition for a method can be expressed using the Requires statement. Preconditions express the requirements that input parameters must satisfy to call the method. Any method can have as many Requires statements as needed. These statements must be placed as the first statements inside the method body.

Note that a precondition should not be confused with input validation. A precondition is essentially a contract between the creator of a method and the caller of that method. It is the responsibility of the caller to ensure that the preconditions are met before calling the method. If input validation is needed, the caller should do that validation.

Never use a precondition for input validation!

Precondition specification

The following example method illustrates how the Requires statement can be used.

// Copyright 2025 by PeopleWare n.v.
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
// http://www.apache.org/licenses/LICENSE-2.0
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

#nullable disable

namespace PPWCode.Vernacular.Contracts.I.Tests.Examples;

public static class StringExtensionsPre
{
    /// <summary>
    ///     Returns a string that is the concatenation of
    ///     <paramref name="nr"/> times the input string
    ///     <paramref name="source"/>.
    /// </summary>
    /// <param name="source">
    ///     the input string; this must not be <c>null</c>
    /// </param>
    /// <param name="nr">
    ///     the number of times that the source string must
    ///     be repeated; this must be a positive number
    /// </param>
    /// <returns>
    ///     A string concatenation of <paramref name="nr"/>
    ///     times the input string <paramref name="source"/>.
    /// </returns>
    /// <remarks>
    ///     The returned value is never <c>null</c>.
    /// </remarks>
    public static string RepeatWithRequires(this string source, int nr) (1)
    {
        Contract.Requires(source != null); (2)
        Contract.Requires(nr >= 0);        (3)

        string result = string.Empty;
        while (nr-- > 0)
        {
            result += source;
        }

        return result;
    }
}

1	We added preconditions to this helper method.
2	Precondition: input string `source` cannot be `null`.
3	Precondition: input number `nr` must be positive.

Precondition validation

The following example shows unit test code that illustrates how the code behaves when a precondition is violated, and the build constant CONTRACTS_PRE is defined.

// Copyright 2025 by PeopleWare n.v.
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
// http://www.apache.org/licenses/LICENSE-2.0
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

#nullable disable

using NUnit.Framework;

namespace PPWCode.Vernacular.Contracts.I.Tests.Examples;

public class ContractRequires : BaseTest
{
    [Test]
    public void TestRequires_ValidInput() (1)
    {
        string s = "Hello";
        string repeated = s.RepeatWithRequires(2);
        Assert.That(repeated, Is.EqualTo("HelloHello"));
    }

    [Test]
    public void TestRequires_InvalidInputSource() (2)
    {
        string s = null;
        Assert.Throws<PreConditionViolation>(
            () => s.RepeatWithRequires(2),
            "Precondition 'source != null' should throw");
    }

    [Test]
    public void TestRequires_InvalidInputNr() (3)
    {
        string s = "Hello";
        Assert.Throws<PreConditionViolation>(
            () => s.RepeatWithRequires(-1),
            "Precondition 'nr >= 0' should throw");
    }
}

1	All preconditions are satisfied, code executes successfully.
2	Input `source` is `null`. This violates the first precondition.
3	Input `nr` is negative. This violates the second precondition.

Whenever a precondition is violated, the Requires method will throw an exception of type PreConditionViolation. This exception derives from the general ContractViolation exception, which in turn derives from ProgrammingError.

ProgrammingError is defined in the PPWCode.Vernacular.Exceptions library and is used for problems at run-time that are caused by incorrect code. This is applicable for precondition violations: a precondition is a contract between the creator of the method and the caller of the method. When such a contract is not respected, the code must be fixed. In the case of a precondition violation, the caller of the method did not respect the contract.

With this in mind, one should never write code to catch a PreConditionViolation. Whenever a PreConditionViolation is thrown, there is a bug in the code and that bug must be fixed.

Never write code that catches a PreConditionViolation!

Note that the exception message in the thrown PreConditionViolation contains the location in the source code of the precondition that was violated.