Мне нужно понять как работает
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
Но как такое может быть?