Invariants

[mristin]

The most interesting part of the design-by-contract, namely invariants, is still missing and I'd like to hear your feedback on how to implement it.

In an OO language, invariants should hold after the constructor and before and after invocation of each public method. They are particularly interesting way to formalize the properties on your more complex contained data structures. For example, if you internally use a sorted slice to perform binary search on it for interval queries, an invariant would be that the slice is always sorted. Another example is a directed acyclic graph with an invariant that there should be no cycles.

For a more detailed (and better) article on advantages of design-by-contract in general and invariants in particular, please see: https://cacm.acm.org/blogs/blog-cacm/227928-why-not-program-right/fulltext

Right now, gocontracts operates on individual files. To add the invariants to a type, I thought about passing the package folder (instead of individual files) to gocontracts, inspecting the type comments and iterating through all the public methods associated with the type. Since there are no constructors in Go, I'd establish the invariants in all the public methods as additional pre and postconditions.

I though that a documentation defining the invariants could look like this:

// SomeType represents something.
//
// SomeType establishes:
// * x >= 0
// * x < Width
// * x < somePrivateProperty
type SomeType struct {
   // ...
}

For some method:

// SomeFunc does something.
//
// SomeFunc requires:
// * x % 3 == 0
func (s *SomeType) SomeFunc(x int) {
   // ...
}

gocontracts would append the invariants of the type to the pre and postconditions and generate the checks as:

// SomeFunc does something.
//
// SomeFunc requires:
// * x % 3 == 0
func (s *SomeType) SomeFunc(x int) {
   // Pre-conditions
   switch {
   case !(s.x >= 0):
      // panic ...
   case !(x % 3 == 0):
      // panic ...
   // ...
   }

   // Post-conditions
   defer func() {
      switch {
      case !(s.x >= 0):
         // panic ...
      // ...
      }
   }()
   // ...
}

How do you like the idea? Is the syntax appealing? Would you mind if you could only disable/enable checks on per-package basis?

In case gocontracts would still keep on operating on individual files, would it be confusing if it parsed all the other go files in the file's directory to read the invariants and then apply it to only the given file (and not establishing invariants on the functions defined in other files)?

Thanks a lot for your feedback!

[tsipo]

I'm a big fan of design-by-contract since I learned it in the mid 90's. That said, I see some serious issues with implementing class invariants for modern multi-threaded languages (including golang). See below a few general comments about class invariants (so not specifically about your proposal) :

1. You should correct to

   In an OO language, invariants should hold after the constructor and before and after invocation of each public method.

See for example: Bertrand Meyer, Eiffel - The Language, Prentice Hall 1992, section 9.12 pp 127-128, and here.

2. This concept of class invariants dates back to the early 70's (C.A.R. Hoare: Proof of Correctness of Data Representation, in Acta Informatica, vol. 1, no. 4, December 1972, pages 271–281). Then, applications were single-threaded. I do not think this definition has been revisited since multi-threading was introduced, as it is obviously NOT thread-safe.

Namely, it allows a method to break a class invariant during its execution. So if you get a context switch at such a point, and another public method of the same class instance is being called, assertion of the invariant will fail at the entry to that method. This is especially important for golang, being a very concurrent language (goroutines).

The "greedy" and strict way to deal with that is to change this definition that a class invariant may never be broken at any time. This is very restricting. To start with, unless we deal with simple invariants, the method implementation can get very complex. Even more so, the invariant assertion mechanism needs to be invoked after every single statement. So I doubt whether it's practical at all.

Another way is to protect with an instance-level mutex all public methods of that instance. This basically turns the instance to be single-threaded. So it reduces the concurrency features of the language considerably.

So I believe that until the "right" way to define thread-safe invariants is found, there is little point in implementing these. This draft paper by Meyer from 2016 discusses concurrency, but I did not find there a clearcut thread-safe definition (it's a bit lengthy, though, I may have missed).

3. A third issue which applies to class invariants in OO languages is the inheritance of those by derived classes. This is spared from us in golang, which uses composition instead of inheritance.

[mristin]

Hi @tsipo , Thanks for your comments!

1.

You should correct to

In an OO language, invariants should hold after the constructor and before and after invocation of each public method.

Corrected, thanks for spotting it -- my mistake would have caused some minus points in the uni exam some fifteen years or so :smile:

2.

The "greedy" and strict way to deal with that is to change this definition that a class invariant may never be broken at any time. This is very restricting.

I agree. However, this is something that "plagues" pre and post-conditions as well as assertions -- they all suffer from differences in time of check - time of use (TOCTOU).

I have dealt with concurrency so far by using immutable objects (akin to functional programming) where a post-condition after the constructor suffices to document the properties (and copy/pasting if there are multiple constructors, which is rarely the case). I find the mix of mutability and multi-threading scary, and was lucky that I didn't have to work in such a scenario.

At the moment, Gocontracts allows you both to write conditions and to write an arbitrary function preamble. The preamble might include necessary locking (and unlocking), while conditions save you typing. Perhaps we need the same mechanism for the invariants? Then it's up to the programmer to decide how/what to test (and the readme should at least expose the problems related to the concurrency).