Abstract dynamic data types: A temporal logic approach