разница в Contract.Requires и Contract.Ensures

Requires – это предварительное условие, означающее, что указанное условие должно быть истинным до вызова метода. Ensures — это постусловие, означающее, что метод гарантирует, что указанное условие будет истинным после завершения вызова метода.

Предусловия и/или постусловия могут быть нарушены во время выполнения метода: проверки выполняются при входе в метод и выходе из него соответственно. Неизменное условие — это контракт, в котором говорится, что указанное условие всегда выполняется.

Прочтите Бертрана Мейера Конструкция объектно-ориентированного программного обеспечения, чтобы получить более [намного больше] подробностей. Эта статья Мейера короче [намного короче].