Tautologies and BIR variables

[guancio]

The presence of BIR variables in predicates makes a bit complicated the definition of tautologies. The current definition states:

tautology(P) = ! s. init_var(s, vars(P)) ==> eval(s, P) = true

In BIR, we usually say that a precondition P holds iff

hold(s,P) = init_var(s, vars(P)) /\ eval(s, P) = true

There has the problem that tautology(P ==> Q) is not equivalent to

!s. hold(s,P) ==> hold(s,Q)

For example, if Q = (x == x:int32) and P = true then tautology(P==>Q). However, for the states s={} and s1={x:int64}, property P holds while property Q does not hold.

This is problematic for the weakening rule. An option is to require in the weakening rule that tautology(P ==> Q) and vars(Q) \subseteq vars(P)`. However, I'm not totally convinced about this rule.