Contract postcondition

Ensures

A postcondition for a method can be expressed using the Ensures statement. Postconditions express conditions that are guaranteed to be true after the method finishes executing. Any method can have as many Ensures statements as needed. These statements must be placed as the last statements inside the method body. If the method returns a value, this value must be captured in a local variable that can be used inside the Ensures statements. As the final statement inside the method body, this variable is returned as the result.

Note that a postcondition is a contract between the creator of the method and the caller of the method. The creator of the method promises that certain conditions are met after the method is called.

Postcondition specification

The following example method illustrates how the Ensures 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 StringExtensionsPost
{
    /// <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 RepeatWithEnsures(this string source, int nr) (1)
    {
        Contract.Requires(source != null);
        Contract.Requires(nr >= 0);

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

        Contract.Ensures(result != null);                      (2)
        Contract.Ensures(result.Length == nr * source.Length); (3)
        return result;
    }
}

1	We added postconditions to this helper method.
2	Postcondition: the returned value is never `null`.
3	Postcondition: the length of the returned string should be `nr` times the length of the input string `source`.

When the implementation of a method is correct, the postconditions will always be met. The above implementation is correct, and as such, the postconditions will never fail.

To illustrate how postconditions can help find bugs, we introduce a faulty implementation in the next example.

// 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 StringExtensionsFaulty
{
    public static string RepeatWithBug(this string source, int nr) (1)
    {
        Contract.Requires(source != null);
        Contract.Requires(nr >= 0);

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

        Contract.Ensures(result.Length == nr * source.Length); (3)
        return result;
    }
}

1	We added postconditions to this helper method.
2	We introduced an off-by-one error in the loop counter.
3	Postcondition: the same one as in the correct implementation.

Postcondition validation

The following example shows unit test code that illustrates how the code behaves when a postcondition is violated, and the build constant CONTRACTS_POST 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 ContractEnsures : BaseTest
{
    [Test]
    public void TestEnsures_Correct() (1)
    {
        string s = "Hello";
        string repeated = s.RepeatWithEnsures(2);
        Assert.That(repeated, Is.EqualTo("HelloHello"));
    }

    [Test]
    public void TestEnsures_Bug() (2)
    {
        string s = "Hello";
        Assert.Throws<PostConditionViolation>(
            () => s.RepeatWithBug(2),
            "Postcondition should throw for faulty implementation");
    }
}

1	Bugfree implementation: all postconditions are satisfied and the code executes successfully.
2	Buggy implementation: the length of the returned value is not the expected length. The postcondition is violated.

Whenever a postcondition is violated, the Ensures method will throw an exception of type PostConditionViolation. 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 postcondition violations: a postcondition 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 postcondition violation, the creator of the method did not respect the contract.

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

Never write code that catches a PostConditionViolation!

Note that the exception message in the thrown PostConditionViolation contains the location in the source code of the postcondition that was violated.