4.4.3 Abstraction with Static Localities