Yes. Moreover, one weakness of design by contract: some contracts are as complicated as the implementations to express as a single logical/mathematical expression. Some contracts can only be expressed compactly by examples, which explains why I like to use contract tests and consider those part of the interface. I think we do best by some combination of contract expressions and contract tests.