Preconditions and postconditions seem like the wrong way to go about solving the issue they try to solve. They are essentially a secondary type system that tries to express information not expressed by the primary type system in a way that is awkwardly disconnected from the primary type system. You could instead just implement the functionality needed to incorporate that information into the primary type system. In practice this would result in an implementation of dependent types, which is fine.