Логическое программирование

Использованный метод верификации программ дает способ синтеза программ, способный гарантировать соответствие программ своим спецификациям.

Традиционный способ разработки программ предполагает, что сначала создается программа, а затем она анализируется на соответствие спецификации, что, возможно, повлечет изменение программы и т.д. При синтезе программа логически выводится из спецификации, что гарантирует ее правильность, а затем с помощью сохраняющих правильность преобразований в программу вносятся изменения, повышающие ее эффективность. Современные методологии программирования основываются на использовании спецификаций и поддержки логической целостности на протяжении всего процесса создания программы, что позволяет минимизировать число ошибок.

Для вывода утверждений программы воспользуемся методом целенаправленного вывода, позволяющим получать предложения из спецификации `S` отдельно одно за другим. Вывод для отношения `r` начинается с цели `G_1`: ?–`r(t)`, а заканчивается некото-рой конъюнкцией целей вида `G_n`: ?–`r_1(t_1),\ …,\ r_k(t_k)`, причем `S,\ G_i\ ⊨\ G_{i+1}`. Это дает клаузу `r(t)\ ←\ r1(t_1),\ …,\ r_k(t_k)`.

Рассмотрим этот метод на примере нахождения всех пар `(u,v)` элементов множества `z`, удовлетворяющих некоторому бинарному отношению `p(u,v)`.

`S_1`: `"найти"(u,v,z)\ ⇔\ u∈z\ ∧\ v∈z\ ∧\ p(u,v)`

`S_2`: `u∈x\ ⇔\ ∃v∃z\ (z=x\ \\\ v\ ∧\ (u=v\ ∨\ u∈z))`

Для удобства запишем спецификацию в форме клауз.

`C_1`: `"найти"(u,v,z)\ ←\ u∈z,\ v∈z,\ p(u,v)`

`C_2`: `u∈z\ ←\ "найти"(u,v,z)`

`C_3`: `v∈z\ ←\ "найти"(u,v,z)`

`C_4`: `p(u,v)\ ←\ "найти"(u,v,z)`

`C_5`: `u∈x\ ←\ x=[u|z]`

`C_6`: `u∈x\ ←\ x=[v|z],\ u∈z`

Синтез программы начнем с цели

`G_1`: ?–`"найти"(u,v,z)`

`G_2`: ?–`u∈z,\ v∈z,\ p(u,v)`              (используем `C_1`)

`G_3`: ?–`v∈[u|z'],\ p(u,v)`                (используем `C_5` и заменим `z=[u|z']`)

`G_4`: ?–`p(u,u)`                             (используем `C_5` и заменим `v=u`)

Первое предложение получим после применения всех подстановок `{z=[u|z'],\ v=u}`:

`P_1`: `"найти"(u,u,z)\ ←\ z=[u|z'],\ p(u,u)`

Другие предложения можно найти, используя механизм возврата и выбирая альтернативные замены. Например, на третьем шаге можно выбрать `C_6` вместо `C_5`.

`G_4'`: ?–`v∈z',\ p(u,v)`                      (используем `C_6`)

`P_2`: `"найти"(u,v,z)\ ←\ z=[u|z'],\ v∈z',\ p(u,v)`

Аналогично, можно выбрать другой вариант на шаге 2.

`G_3'`: ?– `u∈z',\ v∈[v'|z'],\ p(u,v)`        (используем `C_6` и заменим `z=[v'|z']`)

`G_4''`: ?–`u∈z',\ p(u,v)`                      (используем `C_5` и заменим `v'=v`)

`P_3`: `"найти"(u,v,z)\ ←\ z=[v|z'],\ u∈z',\ p(u,v)`

И, наконец,

`G_4'''`: ?– `u∈z’,\ v∈z’,\ p(u,v)`             (используем `C_6` и заменим `z=[v'|z']`)

`G_5`: ?–`"найти"(u,v,z’)`                      (используем `C_2`,`C_3` и `C_4`)

`P_4`: `"найти"(u,v,z)\ ←\ z=[v'|z'],\ "найти"(u,v,z')`

Каждый путь на дереве вывода ведет к некоторой конъюнкции целей и дает некоторое предложение программы. Вывод завершается после исследования всех способов выбора `u` и `v` из первичного множества `z`. Найденные клаузы можно перевести на язык Пролог:

найти(U,U,[U|_]):-p(U,U).                   % P1
найти(U,V,[U|Z]):-принадлежит(V,Z),p(U,V).  % P2
найти(U,V,[V|Z]):-принадлежит(U,Z),p(U,V).  % P3
найти(U,V,[_|Z]):-найти(U,V,Z).             % P4

После получения набора предложений можно попытаться повысить эффективность программы. Если известно, что отношение `p` антирефлексивно, можно убрать предложение `P_1`. Если известно, что `p` симметрично, то можно убрать `P_2` или `P_3`.