#172 - Code Contracts: Validating state with Assert, Assume, ForAll, Exists