In this paper a formal model of menus for interactive systems is defined. The definition of such a formal model is an important addition to the engineering concepts that are generally stressed in papers dealing with user interfaces. The paper takes the simple concept of a menu and defines a mathematical model which allows rigorous mathematical handling of the concepts of menus, menu items and menu constructs. Even for such a simple and well-known concept in user interfaces, such rigorous handling is missing in much of the literature concerning user interfaces. As shown in the paper, the mathematical modelling of menus, while mathematically simple, allows insights into menu definition. The formal model allows the definition of a new concept of completeness which describes some minimum basic requirements for any menu design language. Based on this definition it is shown that certain menu constructs discussed in the literature do not explicitly meet these basic requirements and therefore may have limited value as building blocks for menu design. The model also provides dialogue designers with well defined terminology which allows simple definitions of the terms persistent menus, transient menus and user context. It also combines the benefits of other menu definition languages in the literature, and avoids their drawbacks. Finally, a menu design system based on these concepts is presented which allows easy definition of menu systems and their logic. © 1992 Butterworth-Heinemann Ltd.