Contract assert

Assert & Assume

The statements Assert and Assume are both assert-like statements. These statements are used to validate conditions that must be true at any point in the code and that cannot be expressed as preconditions, postconditions or invariants.

Two variants are available (Assert & Assume). They do essentially the same thing, but are used in a different context. They have a different signature, as can be seen in the following code fragment.

public static void Assert(bool condition)
{
  // ...
}

public static bool Assume(bool condition)
{
  // ...
  return true;
}

Both statements validate a boolean condition. If the condition evaluates to false, the code throws an AssertViolation. If the condition evaluates to true, the code continues executing. The Assert statement is used as a separate statement in the code. The Assume statement is used inside a boolean expression. The examples in the following sections will clarify this.

Assert specification

The following example method illustrates how the Assert 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 IntArrayExtensionsAssert
{
    /// <summary>
    ///     Find the value of the maximum subarray sum
    ///     in the given <paramref name="values"/> array.
    /// </summary>
    /// <param name="values">
    ///     the given array;
    ///     must not be <c>null</c>
    /// </param>
    /// <returns>
    ///     The value of the maximum subarray when
    ///     <paramref name="values"/> is not empty, and
    ///     <c>null</c> when <paramref name="values"/>
    ///     is empty.
    /// </returns>
    public static int? MaxSubarraySum(this int[] values) (1)
    {
        Contract.Requires(values != null);

        int? best = null;
        int current = 0;

        foreach (int v in values)
        {
            current += v;

            // update best when sum improved
            if ((best == null) || (current > best))
            {
                best = current;
            }

            // Sanity check: best should never be less than current
            Contract.Assert(best >= current); (2)

            // sum up till now is negative, then restart
            if (current < 0)
            {
                current = 0;
            }
        }

        Contract.Ensures((best == null) || (values.Length > 0));
        return best;
    }
}

1	We added an assertion to this helper method.
2	Assertion: at this place in the code `best` must always be greater than or equal to `current`.

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

To illustrate how assertions can help find bugs, we introduce a faulty implementation in the next example. Assume that during a refactor, a critical piece of code was omitted.

// 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 IntArrayExtensionsAssertFaulty
{
    public static int? MaxSubarraySumFaulty(this int[] values) (1)
    {
        Contract.Requires(values != null);

        int? best = null;
        int current = 0;

        foreach (int v in values)
        {
            Contract.Invariant(current >= 0);

            current += v;

            // update best when sum improved
            if (best == null) (2)
            {
                best = current;
            }

            // Sanity check: best should never be less than current
            Contract.Assert(best >= current); (3)

            // sum up till now is negative, then restart
            if (current < 0)
            {
                current = 0;
            }
        }

        Contract.Ensures((best == null) || (values.Length > 0));
        return best;
    }
}

1	We added an assertion to this helper method.
2	We introduced a bug in the condition: a critical part of the boolean expression was omitted.
3	Assertion: the same assertion as in the previous example.

Assert validation

The following example shows unit test code that illustrates how the code behaves when an assertion is violated, and the build constant CONTRACTS_ASSERT 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 ContractAssert : BaseTest
{
    [Test]
    public void TestAssert_Correct_Empty() (1)
    {
        int[] values = [];
        int? maxSum = values.MaxSubarraySum();
        Assert.That(maxSum, Is.Null);
    }

    [Test]
    public void TestAssert_Correct_Not_Empty() (2)
    {
        int[] values = [-5, 7, -1, 8];
        int? maxSum = values.MaxSubarraySum();
        Assert.That(maxSum, Is.Not.Null);
        Assert.That(maxSum, Is.EqualTo(14));
    }

    [Test]
    public void TestAssert_Faulty() (3)
    {
        int[] values = [-5, 7, -1, 8];
        Assert.Throws<AssertViolation>(
            () =>
            {
                int? sum = values.MaxSubarraySumFaulty();
            },
            "Assert should throw for faulty implementation");
    }
}

1	Bugfree implementation: works correctly for an empty array.
2	Bugfree implementation: the assertion is satisfied and the code executes successfully.
3	Buggy implementation: the assertion is violated.

Whenever an assertion is violated, the Assert method will throw an exception of type AssertViolation. 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 assertion violations: an assertion is a kind of sanity check that the creator of the method places inside the code for his own benefit. When the assertion is violated, the creator of the code made an assumption which proves not to be true. The assertion helps to verify these kinds of assumptions and protects them when the code is refactored. The latter can help when applying performance optimizations.

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

Never write code that catches an AssertViolation!

Note that the exception message in the thrown AssertViolation contains the location in the source code of the assertion that was violated.

Assume specification

The following example illustrates how the Assume method can be used.

We introduce a helper class User for this. A User is a simple class that contains the Name property to hold a user’s name.

// 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 class User
{
    private readonly string _name;

    public User(string name) (1)
    {
        Contract.Requires(!string.IsNullOrEmpty(name)); (2)
        _name = name;
    }

    public string Name
        => _name; (3)
}

1	The `User` constructor requires a name as input.
2	Precondition: the given name must not be null or empty.
3	The `Name` property: the property only provides a getter and no setter.

As can be seen in the code, an instantiated User object has a Name that is not null and not the empty string.

The following code fragment contains a utility function designed to calculate the total length of usernames from a given list of users.

// 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 class User
{
    private readonly string _name;

    public User(string name) (1)
    {
        Contract.Requires(!string.IsNullOrEmpty(name)); (2)
        _name = name;
    }

    public string Name
        => _name; (3)
}

1	The helper method `SumNameLength`.
2	The assertion as a `Where` predicate.

Note that the User code specifies a postcondition that Name is never null or empty. In the filter on the given not-null users`, an Assume is added to assert that the Name is not null. The Assume statement is typically used inside LINQ predicates.

Assume validation

The following example shows unit test code that illustrates how the code behaves when an assertion in the form of an Assume is violated, and the build constant CONTRACTS_ASSERT is defined. Note that Assert and Assume shared the same build constant.

// 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 System.Reflection;

using NUnit.Framework;

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

public class ContractAssume : BaseTest
{
    [Test]
    public void TestAssume_Correct() (1)
    {
        User[] users =
        [
            new User("An"),
            new User("Bob")
        ];
        int totalLength = users.SumNameLength();
        Assert.That(totalLength, Is.EqualTo(5));
    }

    [Test]
    public void TestAssume_Failure() (2)
    {
        User[] users =
        [
            new User("An"),
            new User("Bob")
        ];
        FieldInfo nameFieldInfo =
            typeof(User)
                .GetField(
                    "_name",
                    BindingFlags.Instance | BindingFlags.NonPublic);
        Contract.Assert(nameFieldInfo != null);
        nameFieldInfo.SetValue(users[0], null); (3)
        Assert.Throws<AssertViolation>(
            () =>
            {
                int totalLength = users.SumNameLength();
            },
            "Assume should throw for broken postcondition");
    }
}

1	Bugfree implementation: the assertion in the form of `Assume` is satisfied and the code executes successfully.
2	Buggy code: the assumption made in the `Assume` statement is not met because the `Name` property is `null` for one of the users.
3	Even though the `Name` property cannot be set through a public accessor, the field itself was overwritten using reflection.

Whenever an assertion in the form of Assume is violated, the Assume method will throw an exception of type AssertViolation. This is the same as for the Assert method.

Take into account the remarks given in the above section for the Assert method: one should never write code to catch an AssertViolation. Whenever a AssertViolation is thrown (through both an Assert and an Assume call), there is a bug in the code and that bug must be fixed.

Never write code that catches an AssertViolation!

Regarding the example code given earlier: it might have been better to explicitly specify a postcondition for the Name property of User. If there was a postcondition that Name is never null or empty, then the postcondition would be violated and that would have been a better indication of the bug inside the code.