Fault-based testing is a technique where testers anticipate errors in a system under test in order to assess or generate test cases. The idea is to have enough test cases capable of detecting these anticipated errors. This paper presents a method of fault-based test case generation for pre and postcondition specifications. Here, errors are anticipated on the specification level by mutating the pre and postconditions. We present the underlying theory by giving test cases a formal semantics and translate this general testing theory to a constraint satisfaction problem. A prototype test case generator serves to demonstrate the automatization of the method. The current tool works with OCL specifications, but the theory and method are general and apply to many state-based specification languages.