With Design by Contract one defines contracts, which are assertion-like statements about functions' input and output parameters (pre- and postconditions), as well as things that never change throughout the execution of the function (invariants). See the demo from Peli de Halleux and Manuel Fahndrich on the interaction of Code Contracts and Pex!