Cтраница 4
Таким образом, мы показали, какой может быть последовательность шагов для достижения цели, т.е. для демонстрации истинности целевого утверждения. [46]
Остальные двухэлементные кортежи из R, такие как ( В: 0, В: D: 0) целевым утверждением G, очевидно, не запрашиваются и поэтому не принадлежат выделенному G интервалу. [47]
Другими словами, если процедуры логически следуют из спецификации, то программа будет частично правильной независимо от того, какое выбрано целевое утверждение. [48]
Напротив, единственным средством для построения этих явных значений, потребуйся они когда-либо ( например, для сообщения о полученном решении целевого утверждения), в СС-системе являются указатели или молекулы, которые хранятся в ячейках переменных. Кроме того, в СС-системе часто приходится выбирать компоненты структурированных термов, когда осуществляется попытка унифицировать эти термы с какими-то другими. При такого рода обстоятельствах мы фактически оказываемся вынужденными использовать в реализации операции построения низкого уровня, чего ранее избегали. [49]
Фактически это правило предписывает, чтобы проверка упорядоченности пар стоящих рядом элементов списка выполнялась сразу, как только пара появляется в текущем целевом утверждении. [50]
Предположим также, что для каждого t 1 мы имеем S, Gt 1 t Gt i - Другими словами, каждое выводимое целевое утверждение логически следует из S и предыдущего целевого утверждения. [51]
![]() |
Дерево вычислений для программы выхождения следующего элемента. [52] |
Здесь, оказывается, полное дерево вычислений и его поддерево, определяемое стандартным правилом выбора вызова, совпадают, поскольку в каждом целевом утверждении имеется только один вызов. [53]