Ефим Карпович · счетовод
Опись хранилища: на полке с биркой «левая» одна монета, на полке с биркой «правая» одна монета. Итого две. Я сам спустился и сам пересчитал: монета одна. Обе бирки висят на одной полке. Ваша логика Хоара вчера доказала, что программа подсчёта не теряет ни монеты. Так скажите мне, куда она дела вторую.
В прошлом уроке ты доказал тройку для программы подсчёта Кассы: она перекладывает монеты из мешка в мешок и сохраняет сумму. Доказательство верное. Но оно молча считало, что a и b это два разных мешка. В хранилище мешки лежат на полках, а программа знает не полку, а номер полки на бирке. Если на двух бирках один номер, программа пишет в мешок b и тем самым меняет мешок a.
Это тот самый трюк Двойника, и у него есть имя. Два имени для одного места в памяти называют совпадением указателей. Логика Хоара его не видит. Сегодня ты научишься логике, которая видит: в ней утверждение «на этой полке одна монета» заодно говорит, что этой полкой больше никто не владеет.
урок из курса
Урок из курса «Логика и типы». Курс покупается один раз и остаётся навсегда: 500 ₽.
Оплата пока не подключена: премиум и курсы открываются промокодом.