334 DESIGN BY CONTRACT:BUILDING RELIABLE SOFTWARE $11.3 In this chapter we will learn how to express such specifications through assertions, to help us assess the correctness of our software.But we will go further.It turns out (and only someone who has not practiced the approach will think of this as a paradox)that just writing the specification is a precious first step towards ensuring that the software actually meets it.So we will derive tremendous benefits from writing the assertions at the same time as we write the software-or indeed before we write the software.Among the consequences we will find the following: Producing software that is correct from the start because it is designed to be correct.[Mills 1975]. The title of an article written by Harlan D.Mills (one of the originators of "Structured Programming")in the nineteen-seventies provides the right mood:How to write correct programs and know it.To"know it"means to equip the software,at the time you write it,with the arguments showing its correctness. Getting a much better understanding of the problem and its eventual solutions. Facilitating the task of software documentation.As we will see later in this chapter, assertions will play a central part in the object-oriented approach to documentation. Providing a basis for systematic testing and debugging. The rest of this chapter explores these applications. A word of warning:C,C++and some other languages(following the lead of Algol W)have an "assert"instruction that tests whether a certain condition holds at a certain stage of the software's execution,and stops execution if it does not.Although relevant to the present discussion,this concept represents only a small part of the use of assertions in the object-oriented method.So if like many other software developers you are familiar with such instructions but have not been exposed to the more general picture,almost all the concepts of this chapter will be new. 11.3 EXPRESSING A SPECIFICATION We can turn the preceding informal observations into a simple mathematical notation, borrowed from the theory of formal program validation,and precious for reasoning about the correctness of software elements. Correctness formulae Let A be some operation (for example an instruction or a routine body).A correctness formula is an expression of the form P)AO denoting the following property,which may or may not hold:334 DESIGN BY CONTRACT: BUILDING RELIABLE SOFTWARE §11.3 In this chapter we will learn how to express such specifications through assertions, to help us assess the correctness of our software. But we will go further. It turns out (and only someone who has not practiced the approach will think of this as a paradox) that just writing the specification is a precious first step towards ensuring that the software actually meets it. So we will derive tremendous benefits from writing the assertions at the same time as we write the software — or indeed before we write the software. Among the consequences we will find the following: • Producing software that is correct from the start because it is designed to be correct. The title of an article written by Harlan D. Mills (one of the originators of “Structured Programming”) in the nineteen-seventies provides the right mood: How to write correct programs and know it. To “know it” means to equip the software, at the time you write it, with the arguments showing its correctness. • Getting a much better understanding of the problem and its eventual solutions. • Facilitating the task of software documentation. As we will see later in this chapter, assertions will play a central part in the object-oriented approach to documentation. • Providing a basis for systematic testing and debugging. The rest of this chapter explores these applications. A word of warning: C, C++ and some other languages (following the lead of Algol W) have an “assert” instruction that tests whether a certain condition holds at a certain stage of the software’s execution, and stops execution if it does not. Although relevant to the present discussion, this concept represents only a small part of the use of assertions in the object-oriented method. So if like many other software developers you are familiar with such instructions but have not been exposed to the more general picture, almost all the concepts of this chapter will be new. 11.3 EXPRESSING A SPECIFICATION We can turn the preceding informal observations into a simple mathematical notation, borrowed from the theory of formal program validation, and precious for reasoning about the correctness of software elements. Correctness formulae Let A be some operation (for example an instruction or a routine body). A correctness formula is an expression of the form denoting the following property, which may or may not hold: {P} A {Q} [Mills 1975]