Какой наиболее широко используемый проект с открытым исходным кодом, который использует дизайн по контракту?

Question

Мне любопытно, сколько дизайна по контракту используется на практике вне сообщества Eiffel. Существуют ли какие-либо активные проекты с открытым исходным кодом, которые используют дизайн по контракту?

Или, чтобы превратить вопрос в один, у которого есть один ответ: какой проект с открытым исходным кодом (не Эйфелева) наиболее широко используется, который использует дизайн по контракту?

Answer 1

"Не Эйфелева" часть вашего вопроса интересна. Контракты имеют смысл, когда они поддерживаются в языке программирования, в противном случае это просто хороший синтаксис для комментариев.

Это подводит нас к языкам, которые поддерживают контракты. Я знаю три, кроме Эйфеля:

• ESC / Java добавляет контракты в Java, используя язык с именем JML.
• Контракты.NET для всех языков.NET (работает на уровне байт-кода)
• Frama-C добавляет контракты к C, используя язык ACSL

Первые два имеют исполняемые контракты. Преимущества: может использоваться как утверждение времени выполнения. Недостатки: не хватает выразительной силы, чтобы полностью указать, что функция делает в контракте. Вы можете в основном только писать проверки здравомыслия.

Контракты ACSL, с другой стороны, являются более выразительными и не исполняемыми. Они позволяют полностью указать, что функция сортировки должна всегда завершаться, и оставлять в порядке те же элементы, что и в исходном массиве. Контракты ACSL могут использоваться для статического анализа, особенно для вычисления наиболее слабых предварительных условий в стиле Хоара.

И только будучи действительно знакомым с последним (отказ от ответственности: я работаю над Frama-C, но часть ACSL - это работа многих людей, некоторые из которых внесли гораздо больший вклад, чем я), я могу упомянуть только "ACSL от пример ", библиотека C с открытым исходным кодом и контрактами ACSL, в настоящее время разрабатываемая Fraunhofer FIRST. Он еще не выпущен, но будет частью проекта Device-soft. Я уверен, что вы могли бы получить предварительную версию, если вы были заинтересованы. Не стесняйтесь связаться с человеком, упомянутым в качестве контакта на этой последней веб-странице.