Defining your own preconditions

• User-defined types are entitled to have their own safety preconditions
• Include documentation so that they can later be determined and satisfied