"Не-Эйфелева" часть вашего вопроса интересна. Контракты имеют смысл, когда они поддерживаются в языке программирования, в противном случае это просто хороший синтаксис для комментариев.
Это приводит нас к языкам, которые поддерживают контракты. Я знаю три, кроме Эйфеля:
- ESC / Java добавляет контракты в Java с использованием языка с именем JML .
- .NET контракты для всех языков .NET (работает на уровне байт-кода)
- Frama-C добавляет контракты в C, используя язык ACSL
Первые два имеют исполняемые контракты. Преимущества: может использоваться как утверждение времени выполнения. Недостатки: не хватает выразительной силы, чтобы полностью указать, что функция делает в контракте. Вы можете в основном только писать проверки работоспособности.
ACSL-контракты, с другой стороны, более выразительны и не могут быть выполнены. Они позволяют полностью указать, что функция сортировки должна всегда завершаться, и оставлять в порядке те же элементы, что и в исходном массиве. Контракты ACSL можно использовать для статического анализа, особенно для расчета наиболее слабых предусловий в стиле Хоара.
И только будучи действительно знакомым с последним (отказ от ответственности: я работаю над Frama-C, но часть ACSL - работа многих людей, некоторые из которых внесли гораздо больше, чем я), я могу только упомянуть «ACSL by example» - библиотека C с открытым исходным кодом и контрактами ACSL, которая в настоящее время разрабатывается Fraunhofer FIRST. Он еще не выпущен, но будет частью проекта Device-soft . Я уверен, что вы могли бы получить предварительную версию, если вы были заинтересованы. Не стесняйтесь связаться с человеком, упомянутым в качестве контакта на этой последней веб-странице.