PAT里面有一个trace的隐藏功能。如下面的例子：
P()=a->b->c->P()[]a->b->P(){b}; Q()=a->Q();
两个判断
#assert P() refines Q(); #assert Q() refines P();
判断结果：
