Object-oriented formal specifications

Recent developments in research on formal methods made formal specification languages to be widely used in industrial applications. In particular, formal specification languages are mainly used to understand and/or to analyze requirements of software systems, though they can be used at all stages of software development. When combined with object-oriented approach, formal specification languages have cumulative advantages such as analyzing properties of objects in isolation and supporting reusability. In this tutorial, I describe the object-oriented formal specification language Object-Z and how it can be used to capture requirements of a software system. Object-Z is an object-oriented extension of the formal specification language Z.