Formal Specification

We identify both the mathematical structures and the logic that underpin the main approaches to the formal specification of systems. Our aim is to present a theoretical framework for system specification that is built on precise mathematical foundations. Being faced with the syntactic details of particular specification languages can be confusing for someone who lacks mathematical experience. For this reason we prefer to present the important theoretical concepts that underlie system construction in the familiar notation of logic and mathematics. Once an understanding of these concepts is achieved, the notations that are currently in use can be mastered without difficulty. We see an analogy with the need to understand the fundamental principles of programming before becoming too involved with the fussy, and often confusing, syntactic details of concrete mechanical codes. Understanding is best achieved when an abstract programming language is used.