This does not work for a current state like this: (a:float /\ b:int /\ x:float /\ y:str). Why? Because it would lead to the conjunction (T?1 <= float) /\ (T?1 <= int)), which means that both T?1 |-> int and T?1 |-> float occur, which results in T?1 |-> bot, which generates an invalid state. And this means that the specification cannot be applied.
This is actually what happens in this case. What is needed for this approach is to have (a, b) and (x, y) in the current state. Therefore, the current state must be modified as follows:
func spec
func call:
current instantiation:
This does not work for a current state like this:
(a:float /\ b:int /\ x:float /\ y:str)
. Why? Because it would lead to the conjunction(T?1 <= float) /\ (T?1 <= int))
, which means that bothT?1 |-> int
andT?1 |-> float
occur, which results inT?1 |-> bot
, which generates an invalid state. And this means that the specification cannot be applied.desired instantiation:
This is actually what happens in this case. What is needed for this approach is to have
(a, b)
and(x, y)
in the current state. Therefore, the current state must be modified as follows: