Skip to content

Latest commit

 

History

History
113 lines (76 loc) · 4.63 KB

properties.md

File metadata and controls

113 lines (76 loc) · 4.63 KB

Properties

Coming up with useful properties to test can be a bit daunting at first. Fortunately, there is a lot of good writing about effectively applying property-based testing. While the test library interfaces differ tremendously between languages/platforms, the underlying concepts usually port well.

Testing Stateful Systems

Beyond testing individual functions, property-based testing can also be used for testing stateful systems by generating a sequence of operations using them. (In C, this might be represented as an array of fixed-size "operation" structs, with an enum tag for each operation's API function and a union for any arguments.) The test function runs each operation, check its result, and then does an overall consistency check for the updated state of the system. If all operations run without any errors, then it checks whether the final state is as expected. If so, the test passes.

For example, for a key/value store, the test could run a series of operations, checking their results along the way:

  • If set(s, key, value)'s result indicates it stored successfully, the test should updated an in-memory list of records. If the key was invalid, it should check that the store returned an error.

  • Check that get(s, key) returns the most recent value from the in-memory records, or NOT FOUND.

  • delete(s, key) should return NOT FOUND if the key wasn't in the in-memory records. If it was, it should be removed from them.

Finally, once the test has run all the key/value store operations, it should be able to get(s, key) key still in the in-memory records, and all the values should match (otherwise the store lost/corrupted data).

The main constraint for a property test is that it can be run over and over with slightly different input -- this usually means testing using an in-memory database, simulated hardware, or some other stand-in for external interfaces that can be cleanly reset after each test. It can use a very simple implementation -- it doesn't need to run in production, it just needs to be correct, and fast enough for testing.

Example Properties

During performance tuning

  • For any input, code with clever optimizations should always produce the same result as a straightforward version that is too inefficient for production use, but is much easier to check.

In a data compression library

  • For any input, compressing and uncompressing it should produce output that matches the original input.

  • For any input, the compression output should never be larger than the original input, beyond some small algorithm-specific overhead.

  • For any input, the uncompression state machine should never get stuck; it should always be able to reach a valid end-of-stream state once the end of input is reached.

In a storage library

  • For any sequence of operations, any records that the library says have been safely written should be readable later.

  • Interleaving those operations with resetting the library's state in-memory and re-reading headers to recover the current storage state should never cause data loss.

  • Injecting temporary hardware faults should lead to errors being handled correctly and recovering without data loss.

In a parser

  • For any input, it should output either a successful parse with a valid parse tree, or error information.

  • For any valid input (generated by randomly walking the grammar), it should output a valid parse tree.

In a flash memory wear-leveling system

  • For any sequence of writes (of arbitrary, bounded size), no flash page should have significantly more writes than the others.

In a datagram-based network

  • For any order of receiving packets (including retransmissions), all packets should eventually be received and acknowledged, and every packet should be checksummed once, in order.

In data structure implementations

  • For any sequence of insertions and deletions, a balanced binary tree should always stay approximately balanced.

  • For any input, a sorting algorithm should produce sorted output.