Как работает подстановка в логике Хоара?
На досуге пытаюсь самообразовываться, потянуло в логику Хоара с аксиоматическим доказательством (частичной)) корректности программ, но никак не могу понять принцип подстановки в ней, и объяснения толкового не нашлось.
То есть, рассматривается простой свайп значений переменных без доп.памяти на трёх присвоениях.
На первом шаге исходные значения переменных присваиваются к константам a и b:
I: X=a & Y=b
Потом выполняется операция S1:
S1: X := Y - X
После этого система приходит в любопытное состояние-предикат F1:
F1: Y=b & Y-X=a
И это дико странно, ведь после команды S1 у нас X = Y-X = b-a; как появляется и что значит выражение Y-X = a? Выглядит так, словно в левую часть выражения X := Y - X подставили исходное X=a, но какой в этом смысл??