EvilsInterrupt
@EvilsInterrupt
System programming, Reversing Engineering, C++

Как работает implies в Eiffel?

Мне нужно понять как работает implies в языке программирования Eiffel.

Читая книгу "Почувствуй класс" от Бертрана Майера и мне кажется, что у автора в книге код противоречивый. Вот пример:

ensure
  at_first : (not is_empty) implies (index=1)


Напомню работу implies: "The value of the boolean expression a implies b is true except if a is true and b false" взял в статье 8 DESIGN BY CONTRACT TM , ASSERTIONS, EXCEPTIONS

А теперь возьмем предложение:
"Сейчас по факту список пустой и индекс равен 5", тогда
* not is_empty дают False
* index = 1 дают False
согласно таблице истинности мы получаем:
* at_first = True

Но как такое может быть?
  • Вопрос задан
  • 2422 просмотра
Пригласить эксперта
Ваш ответ на вопрос

Войдите, чтобы написать ответ

Войти через центр авторизации
Похожие вопросы