Доказательство основных арифметических свойств

Я пытаюсь использовать инструмент доказательства теорем TLA +, чтобы доказать свойства безопасности алгоритма. Но я обнаружил, что TLAPS не может вычислить очень "простые" математические факты.

Моя первая проблема была с:

EXTENDS Naturals
CONSTANTS x,y
ASSUME x \in Nat /\ y \in Nat
LEMMA x=y+1 => y<x
  OBVIOUS

TLAPS не может сделать это в одиночку с какой-либо серверной проверкой. Я также пробовал использовать определенные серверные программы проверки с другой тактикой:

LEMMA x=y+1 => y<x
  BY IsaM("blast")

Но тоже не удалось. Аналогичным образом нельзя проверить и другие простые факты, например:

LEMMA x<y => x<y+0

В прошлом я использовал некоторые из этих средств доказательства теорем, например Z Solver или Isabelle, и, насколько я помню, они очень мощные. Я думаю, мне что-то здесь не хватает ... или я не понимаю органайзер доказательства TLAPS, или мне все еще нужно загрузить какой-то другой модуль с аксиомами ?.


formal-verification tla+
person fulem    schedule 27.05.2019    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Кажется, вы столкнулись с ошибкой в ​​TLAPM - по крайней мере, в разрабатываемой версии на моей машине. Причина в том, что перевод SMT не соответствует второму предположению. Без ограничения домена ни одно из утверждений не должно быть доказуемым. В качестве оперативного исправления я добавил ограничения домена в локальную лемму. Теперь я могу доказать:

LEMMA ASSUME x \in Nat, y \in Nat
      PROVE x=y+1 => y < x BY SMT

Еще один способ обойти это на данный момент - иметь именованные предположения, которые вызываются всякий раз, когда это необходимо:

ASSUME DOM == x \in Nat /\ y \in Nat
LEMMA x=y+1 => y < x BY SMT, DOM

должен пройти. В обоих случаях вам нужно добавить EXTENDS TLAPS в начале вашей спецификации, чтобы включить ключевое слово SMT.

Я также сообщу об ошибке сопровождающим.

Обновление: кажется, что глобальные предположения обычно не принимаются во внимание TLAPM (afaik по соображениям производительности). Версия с именованными предположениями - предпочтительный путь.

person lambda.xy.x    schedule 28.05.2019
comment
Большое спасибо!. Возможно, вас интересует этот другой вопрос о TLA, который я задал здесь < / а> - person fulem; 31.05.2019