Contract invariant

Invariant

An invariant can be expressed using the Invariant statement. There are several types of invariants, and here we make the distinction between loop invariants and object invariants. Loop invariants express conditions that are guaranteed for every iteration through the loop. Object invariants are conditions that are guaranteed to be true before and after method calls on the object.

For loop invariants, one could add all Invariant statements at the beginning of the loop. For object invariants, one would typically create a method CheckInvariants on the object that contains all Invariant statements for this object. This method must then be called at the end of every public method on the object.

Note that an invariant is a contract between the creator of the object and the user of the object. The creator of the object promises that certain conditions are met after every public method call on the object.

Invariant specification

The following example object illustrates how the Invariant method can be used.

The Chest class models a chest that can be opened and that can be locked. There is a dependency between the open and the locked state: a chest cannot be both open and locked. This is an invariant modeled using the Invariant statement.

// 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 PPWCode.Vernacular.Exceptions.IV;

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

public class Chest
{
    public Chest()
    {
        CheckInvariants(); (3)
    }

    private void CheckInvariants() (1)
    {
        Contract.Invariant(!(IsOpen && IsLocked)); (2)
    }

    public bool IsOpen { get; private set; } = false;

    public bool IsLocked { get; private set; } = false;

    public void Open()
    {
        if (IsLocked)
        {
            throw new SemanticException("Cannot open when locked.");
        }

        IsOpen = true;
        CheckInvariants(); (3)
    }

    public void Close()
    {
        IsOpen = false;
        CheckInvariants(); (3)
    }

    public void Lock()
    {
        if (IsOpen)
        {
            throw new SemanticException("Cannot lock when open.");
        }

        IsLocked = true;
        CheckInvariants(); (3)
    }

    public void Unlock()
    {
        IsLocked = false;
        CheckInvariants(); (3)
    }
}

1	The `CheckInvariants` method contains all invariants for the `Chest` class.
2	Invariant: the chest cannot be both open and locked at the same time.
3	Every public method validates the invariants at the end of the method body.

When the implementation of the object is correct, the invariants will always be met. The above implementation is correct, and as such, the invariants will never fail.

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

// 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 FaultyChest
{
    public FaultyChest()
    {
        CheckInvariants(); (3)
    }

    private void CheckInvariants() (1)
    {
        Contract.Invariant(!(IsOpen && IsLocked)); (2)
    }

    public bool IsOpen { get; private set; } = false;

    public bool IsLocked { get; private set; } = false;

    public void Open()
    {
        IsOpen = true;
        CheckInvariants(); (3)
    }

    public void Close()
    {
        IsOpen = false;
        CheckInvariants(); (3)
    }

    public void Lock()
    {
        IsLocked = true;
        CheckInvariants(); (3)
    }

    public void Unlock()
    {
        IsLocked = false;
        CheckInvariants(); (3)
    }
}

1	The `CheckInvariants` method contains all invariants for the `Chest` class.
2	Invariant: the chest cannot be both open and locked at the same time.
3	Every public method validates the invariants at the end of the method body.

Invariant validation

The following example shows unit test code that illustrates how the code behaves when an invariant is violated, and the build constant CONTRACTS_INVARIANT 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 System;

using NUnit.Framework;

using PPWCode.Vernacular.Exceptions.IV;

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

public class ContractInvariant : BaseTest
{
    private void Exec(Action action)
    {
        try
        {
            action();
        }
        catch (SemanticException)
        {
        }
    }

    [Test]
    public void TestInvariant_Correct() (1)
    {
        Chest chest = new();
        Assert.That(chest.IsOpen, Is.False);
        Assert.That(chest.IsLocked, Is.False);

        Exec(() => chest.Lock());
        Exec(() => chest.Open());
        Exec(() => chest.Unlock());
        Exec(() => chest.Open());

        Assert.That(chest.IsOpen, Is.True);
        Assert.That(chest.IsLocked, Is.False);
    }

    [Test]
    public void TestInvariant_Bug() (2)
    {
        FaultyChest chest = new();
        Assert.That(chest.IsOpen, Is.False);
        Assert.That(chest.IsLocked, Is.False);

        Exec(() => chest.Lock());
        Assert.Throws<InvariantViolation>(
            () => Exec(() => chest.Open()),
            "Invariant should throw for faulty implementation");
    }
}

1 Bugfree implementation: the chest protects the dependency between the states open and locked by throwing a SemanticException when an action is not possible. A SemanticException is a business exception, and something that can happen and that the implementation has to deal with. The Exec method ignores the SemanticException because the goal of the test is to validate that the implementation is correct and never puts the chest into an inconsistent state.

2 Buggy implementation: the chest does not protect the dependency between the states open and locked, and it is possible to put the chest into an inconsistent state. At that point, the invariant is violated.

Whenever an invariant is violated, the Invariant method will throw an exception of type InvariantViolation. 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 invariant violations: an invariant is a contract between the creator of the object (for an object invariant) and the caller of methods on that object. When such a contract is not respected, the code must be fixed. In the case of an invariant violation, the creator of the object did not respect the contract.

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

Never write code that catches a InvariantViolation!

Note that the exception message in the thrown InvariantViolation contains the location in the source code of the invariant that was violated.