Specification of Abstract Dynamic-Data Types: A Temporal Logic Approach