out Blocks and Expression-based Contracts

out blocks for postconditions

This contract involves guarantees that the function provides. Such guarantees are called the function’s postconditions. An example of a function with a postcondition would be a function that returns the number of days in February: The function can guarantee that the returned value would always be either 28 or 29.

The postconditions are checked inside the out blocks of functions.

Because the value that a function returns by need not be defined as a variable inside the function, there is usually no name to refer to the return ...