Event logic for specifying abstract dynamic data types