用符号执行证明加法交换律

将已证明的fact放在Path Condition里。

inductive nat {
	0,
	S(nat prev),
}
 
nat add(nat a, nat b) {
	if (a == 0) return b;
	else return S(add(a.prev, b));
}
 
void add_zero(nat a)
requires True
ensures  add(a, 0) == a
{
	// a |-> ?a, True
	if (a == 0) {
		// a |-> ?a, ?a == 0
		nat x = add(a, 0);
		// a |-> ?a, x |-> add(?a, 0), ?a == 0
			nat add(nat a, nat b) {
				// a |-> ?a, b |-> 0, ?a == 0
				if (a == 0)
					// a |-> ?a, b |-> 0, ?a == 0
					return b;
					// a |-> ?a, b |-> 0, ret |-> 0, ?a == 0
				else
					// a |-> ?a, b |-> 0, ?a == 0 /\ ?a != 0
					return S(add(a.prev, b));
				// a |-> ?a, b |-> 0, ret |-> 0, ?a == 0
			}
		// a |-> ?a, x |-> 0, ?a == 0 /\ add(?a, 0) == 0
	} else {
		// a |-> ?a, ?a != 0
		nat b = add(a, 0);
		// a |-> ?a, b |-> add(?a, 0), ?a != 0
		@open add;
		// a |-> ?a, b |-> S(add(?a.prev, 0)), ?a != 0 /\ add(?a, 0) == S(add(?a.prev, 0))
		nat c = add(a.prev, 0);
		// a |-> ?a, b |-> S(add(?a.prev, 0)), c |-> add(?a.prev, 0), ?a != 0 /\ add(?a, 0) == S(add(?a.prev, 0))
		@induction; add_zero(a.prev);
		// a |-> ?a, b |-> S(add(?a.prev, 0)), c |-> ?a.prev, ?a != 0 /\ add(?a, 0) == S(add(?a.prev, 0)) /\ add(?a.prev, 0) == ?a.prev
		assert(S(c) == b);
		// a |-> ?a, b |-> S(add(?a.prev, 0)), c |-> ?a.prev, ?a != 0 /\ add(?a, 0) == S(add(?a.prev, 0)) /\ add(?a.prev, 0) == ?a.prev /\ S(?a.prev) == S(add(?a.prev, 0))
	}
}

需要自动化解决的：

• ?a == 0 /\ add(?a, 0) == 0 |- add(?a, 0) == ?a
• ?a != 0 /\ add(?a, 0) == S(add(?a.prev, 0)) /\ add(?a.prev, 0) == ?a.prev /\ S(?a.prev) == S(add(?a.prev, 0)) |- add(?a, 0) == ?a

循环不变式与递归的对应性？