Using design patterns to derive PAC architectures from Object-Z specifications

Interactor-based architectures for Graphical User Interfaces (GUIs) model an interface as a composition of interacting objects that each present internal state to the user and provide operations on that state. One such architecture is Presentation-Abstraction-Control (PAC). Architectures such as PAC can be described as a combination of design patterns. We use the patterns to derive a PAC architecture for a file browser application from a corresponding Object-Z specification