6.Определение семантики языков на основе средств логического программирования. Определение базисных операторов на языке исчисления предикатов.

Логи́ческое программи́рование — парадигма программирования, основанная на автоматическом доказательстве теорем, а также раздел дискретной математики, изучающий принципы логического вывода информации на основе заданных фактов и правил вывода. Логическое программирование основано на теории и аппарате математической логики с использованием математических принципов резолюций.

Самым известным языком логического программирования является Prolog.

Первым языком логического программирования был язык Planner, в котором была заложена возможность автоматического вывода результата из данных и заданных правил перебора вариантов (совокупность которых называлась планом). Planner использовался для того, чтобы понизить требования к вычислительным ресурсам (с помощью метода backtracking) и обеспечить возможность вывода фактов, без активного использования стека. Затем был разработан язык Prolog, который не требовал плана перебора вариантов и был, в этом смысле, упрощением языка Planner.

Рассмотрим один из способов спецификации операторов языка программирования, основанный на языке исчисления предикатов. Введем понятие состояния программы через состояние переменных программы, в свою очередь определяемого через таблицу значений переменных программы. Состояние программы представляет из себя динамически изменяемый объект в процессе выполнения программы, которое может меняться в результате выполнения отдельной

программной конструкции (функции, оператора, модуля). Пусть s={x,y,…} -состояние программы (состояние переменных) до выполнения некоторой программной конструкции P , а

s'={x',y',…}- состояние программы после выполнения конструкции P. Тогда для спецификации конструкции P мы можем использовать предикат _P (s,s'), показывающий, как изменились значения переменных x,y,… в результате выполнения конструкции P.

Тождественный оператор- оставляет неизменными все значения переменных . IDENT=_df (x'=x) & (y'=y) .

Оператор присваивания. Пусть (e_x -> P) обозначает выражение, получаемое из P путем замены всех свободных вхождений переменной x на e и D_e -область определения выражения e. Тогда:

x:=e;P =_df  ( D_e) (e_x -> P)

Условный оператор. Пусть P и Q -спецификации и b - логическое выражение, не содержащее штрихованных переменных . Тогда выражение if b then P else Q является спецификацией программной конструкции , которая выполняется как P , если b -истинно , и как Q - в противном случае . Пусть D_b -область определения выражения b. Тогда:

if b then P else Q=_df  ( D_b) (b&P)  ( b&Q)

Последовательная композиция. Пусть P - спецификация, содержащая переменную p, значением которой может быть любая допустимая спецификация. Тогда, если Q - некоторая спецификация, определим выражение (Q_p ->>P) как соотношение, получаемое заменой всех вхождений переменной p на Q в выражении P. Содержательно точки вхождения переменной p в этом случае можно рассматривать как вызов процедуры или функции со спецификацией Q. Важно отметить, что данная операция подстановки (Q_p ->>P) имеет более высокий приоритет, нежели операция подстановки (e_x -> P) , то есть в любом случае :

Q_p ->>( e_x -> P)= (e_x ->( Q_p ->> P)) .

Выделим специальную переменную SKIP для обозначения успешного завершения программной конструкции. Пусть P и Q - некоторые спецификации, тогда последовательную композицию можно определить следующим образом:

P;Q =_df Q_SKIP->>P.

Содержательно, выражение P;Q определяет программную конструкцию, которая выполняется в соответствии со спецификацией P, и после успешного завершения конструкции P выполняется в

соответствии со спецификацией Q . Например, в конструкции y:=y/x; Q переход на выполнение Q может осуществиться только при x 0 .

Оператор цикла "while". Спецификацию циклического оператора определим рекурсивным образом: while b do P=_df if b then(P; while b do P) else SKIP, где b -логическое выражение, а P - спецификация тела цикла.