public class DelegateAbstractDomain<LatticeAbstractStateT extends LatticeAbstractState> extends java.lang.Object implements AbstractDomain
AbstractDomain
operators to the LatticeAbstractState
.
Thus, we can keep the CPA algorithm generic without having to cast types in the domain specific code.
Abstract domains defined with LatticeAbstractState
should be passed as DelegateAbstractDomain
s
to the CPA algorithm.Constructor and Description |
---|
DelegateAbstractDomain() |
Modifier and Type | Method and Description |
---|---|
boolean |
isLessOrEqual(AbstractState abstractState1,
AbstractState abstractState2)
Compares two abstract states.
|
AbstractState |
join(AbstractState abstractState1,
AbstractState abstractState2)
Computes the join over two abstract states.
|
public AbstractState join(AbstractState abstractState1, AbstractState abstractState2)
AbstractDomain
join
in interface AbstractDomain
public boolean isLessOrEqual(AbstractState abstractState1, AbstractState abstractState2)
AbstractDomain
isLessOrEqual
in interface AbstractDomain