Псевдокод для логики [Предикат логики в CS]
Мы пытаемся перевести очень простую программу с псевдокодом в Predicate Logic. Программа проста и не содержит циклов. (Последовательный)
Он состоит только из присвоений переменных и операторов if-else.
К сожалению, мы не располагаем какой-либо хорошей информацией для решения проблемы. Было бы здорово, если у кого-то есть
- примеры "преобразования" простых фрагментов кода 5liner или
- ссылки на источники для бесплатной информации, которые описывают тему на поверхностном уровне. (Мы используем только предикатную и предлогическую логику и не хотим погружаться намного глубже в логическое пространство.)
С уважением
ОБНОВЛЕНИЕ: После достаточного исследования я нашел решение и могу поделиться им вкл. Примеры. Хитрость заключается в том, чтобы думать о состоянии программы как о множестве всех наших произвольных переменных inc. программный счетчик, который обозначает текущую инструкцию, которая будет выполнена.
x = input;
x = x*2;
if (y>0)
x = x∗y ;
else
x = y;
Мы сформируем Предикат P(x,i,y,pc). Отсюда мы можем строить обещания, например:
∀i∀x∀y(P (x, i, y, 1) => P (i, i, y, 2))
∀i∀x∀y(P (x, i, y, 2) => P (x ∗ 2, i, y, 3))
∀i∀x∀y(P (x, i, y, 3) ∧ y > 0 =⇒ P (x ∗ y, i, y, 4))
∀i∀x∀y(P (x, i, y, 3) ∧ ¬y > 0 =⇒ P (y, i, y, 4))
Увеличивая счетчик Программы, мы гарантируем, что обещания следуют по порядку. Теперь мы можем определить, сделать доказательство, когда дана предпосылка для Входа, например, P(x,4,7,1).