Formal Schemas and Property Tests

These two concepts work together really well.

Recently I have been experimenting with Json Schema as a way to formally describe an API. It lists all possible inputs that are accepted in a single document. Equivalent schema documents exist for other contracts.

A property test is a way of stating invariants about a system. You write tests that make assertions about the system that are always true for a range of inputs. The testing tool generates an increasingly complex input an runs a series of assertions reporting the simplest case that fails.

If you have a formal input specification the simplest property test you have is I can accept this input without rejecting the message. The contract document gives you a source for the generators.

By creating a generator based upon a specification document allows the tests to keep up with all possible inputs. This is the closest that you can get to a formal proof for system correctness without requiring a single typesystem (which in a distributed system may be impossible).