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).

One thought on “Formal Schemas and Property Tests

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s