Swinging UML: how to make class diagrams and state machines amenable to constraint solving and proving
Peter Padawitz · 2000
. Swinging types (STs) provide a specification and verification formalism for designing software in terms of many-sorted logic. Current formalisms, be they set- or order-theoretic, algebraic or coalgebraic, ruleor net-based, handle either static system components (in terms of functions or relations) or dynamic ones (in terms of transition systems) and either structural or behavioral aspects, while STs combine equational, Horn and modal logic for the purpose of applying computation and proof rules from all three logics. UML provides a collection of object-oriented pictorial specification techniques, equipped with an informal semantics, but hardly cares about consistency, i.e. the guarantee that a specification has models and thus can be implemented. To achieve this goal and to make verification possible a formal semantics is indispensable. Swinging types have term models that are directly derived from the specifications. The paper takes first steps towards a translation of...