#logic
#Логические
Вопрос:
Кто-нибудь может объяснить этот пример логики разделения?
В чем разница между первой строкой и второй строкой?
Комментарии:
1. Этот вопрос относится к cstheory.stackexchange.com
2. Спасибо за ваши комментарии, я задам вопрос в cstheory.stackexchange.com
Ответ №1:
В первой строке говорится, что куча содержит только один пакет данных, на который указывает ссылка x в хранилище, и он содержит значение 4,4 .
Это значение false в A, потому что оно забывает о пакете, на который указывает y (оно неправильно характеризует всю кучу).
Во второй строке говорится, что куча может быть разделена на два непересекающихся блока, так что на один из них указывает ссылка x и содержит 4,4 , а второй может быть любым.
В A второй пакет может быть тем, на который указывает y . В B второй пакет может быть emp .
Третья строка верна только в A, потому что в B блоки heaplets, которые указывают на 4,4 , не являются непересекающимися.
Четвертая строка имеет значение true только в B, потому что в ней говорится, что вся куча может быть описана как содержащая 4,4 , на которую ссылается x , и содержащая 4,4 , на которую ссылается y. Это неправильно в A, потому что A содержит две непересекающиеся копии 4,4 , поэтому его следует описывать с использованием разделяющего соединения.
Комментарии:
1. Большое вам спасибо. Я понял суть. Не могли бы вы посмотреть второй пример ниже для меня?
Ответ №2:
Это аксиомы для логики разделения. Я могу понять первый, второй и последний, но я не могу понять третий.
Кто-нибудь может мне это объяснить? Что это [X/x] значит?
«каждый x in e будет заменен на X «, это правильно?
Комментарии:
1.
{X = x / e -> Y} x := [e] {e[X/x] -> Y / Y = x}говорит: рассмотрим кучу с одним местоположениемe, содержащим некоторое значениеY, а местоположение хранилищаxсодержит значениеX, затем выполнениеx := [e]приводит к куче с одним местоположениемe[X/x], содержащим то же значениеY, и теперь местоположение хранилищаxсодержит значениеY. Выполнение этого оператора не влияет на кучу (по-прежнему существует только одно местоположение, содержащее значениеY), но оно влияет на местоположение хранилищаx.YиXявляются просто переменными-заполнителями для связи до и после. Это настолько общее, чтобы обслуживатьx := [x 1], например.