Specifications are necessarily informal or: some more myths of formal methods

(1)

Specifications

Are Necessarily

Informal

or: Some

More Myths of Formal Methods*

Baudouin Le Charlier

Znstitut d’lnfomtatique, University of Namur, B-5000 Namur, Belgium

Pierre Flener

Department of Computer Engineering and Information Science, Bilkent University, 06533 Bilkent, Ankara, Turkey

We reconsider the concept of specification in order to bring new insights into the debate of formal versus non-formal methods in computer science. In our view, the correctness of a useful program corresponds to an objective fact, which must have a simple, precise, and understandable formulation. As a consequence, a specification can (and must) only make precise the link existing between the program (formality) and its pur- pose (informality). Moreover, program correctness can be argued only by means of non-formal reasonings, which should be as explicit as possible. This allows us to explain why specifications cannot be written in a strictly formal language. Our view of specifications does not imply a rejection of all ideas put forward in the literature on formal methods. On the contrary, we agree with the proponents of formal methods on most of their arguments, except on those following from the assumption that specifications could (or should) be formal. Finally, we examine why the role and nature of specifications are so often misunderstood. 0 1998 Elsevier Science Inc.

1. INTRODUCTION

Gist specifications were near& as hard to read as those in other formal specification languages. We soon realized

Address correspondence to Dr. Pierre Flener, Bilkent University, Department of Computer Engineering 06533 Bilkent, Ankara, Turkey. E-mail: pf@cs.bilkent.edu.tr

*Contrary to previous papers of the ‘myths series” [4,19], we do not discuss industy-level myths on the uselessness of formal meth- ods, but rather ana&ze some academic myths on their usefitlness.

that the problem was not particular to Gist, but extant across the entire class of formal specification languages. In their effort to be formal, all these languages have scrubbed out the mechanisms which make informal lan- guages understandable, such as summaries and overviews, alternative points of view, diagrams, and examples.

-R. Baker (19851.

Recently, there have been numerous papers advo- cating the use of formal methods in software development (e.g., [Bowen and Hinchey, 1995a, 1995b; Craigen et al., 1995; Fraser et al., 1994; Gerhart et al., 1994; Gibbs, 1994; Hall, 1990; Larsen et al., 19961, plus some of the opinions in Saiedian [1996]). Similar opinions were sporadically published before (e.g., [Fraser et al., 1991; Guttag et al., 1982; Hoare, 1987; Meyer, 1985; Wing, 1990]), plus some of the opinions in Denning (1989). In these papers, mem- bers of academe and industry describe formal methods as a key contribution to overcoming the chronic software crisis. Indeed, formal specification languages force specifiers to be absolutely precise about their intentions, since (internal) inconsistency and incompleteness can be mechanically detected. More- over, formal specifications can be used during vali- dation by the customer through animation or proto- typing, and can guide the actual development of the software, or at least be used in the formal verification of the developed software. All this is proposed at various degrees of formality, from fully formal to “formal light.”

However, fallacies in some assumptions underlying formal methods have been exposed, such as by J. SYSTEMS SOFTWARE 1998; 40~275-296

0164-1212/98/$19.00 PI1 80164-1212(98)00172-6

(2)

276 J. SYSTEMS SOFTWARE 1998; 0275-296

B. Le Charlier and P. Flener

pointing out essential differences between engineering and mathematics in general, and between computing and mathematics in particular (see other opinions in [Denning, 1989; Saiedian, 1996]), or by shedding some light onto the real nature of requirements and specifications, so as to identify minimum standards for languages allowing their representation (Jackson, 1995; Zave and Jackson, 1997). Some authors have been begging for caution about formal methods, by mentioning fundamental theoretical and practical problems, e.g., DeMillo, Lipton, and Perlis (1979), Fetzer (1989), Karp (in [Denning, 1989]), Parnas (119941, and in [Saiedian, 1996]), and Wino- grad (in [Denning, 19891).

A similar debate is going on about the teaching of computer science (Denning, 1989) should the cur- riculum include formal methods or not? To what extent?

Simultaneously, there is a debate on whether formal specification languages ought to be executable or not (Fuchs, 1992; Gravel1 and Henderson, 1996; Hayes and Jones, 1989). However, some researchers challenge the contention that specifications ought to be (fully) formal in the first place, e.g., Balzer et al. (Balzer, 1985; Balzer et al., 1986), Karp (in [De- nning, 1989]), and Pamas ([Pamas, 1994; Pamas and Madey, 19951, and in [Saiedian, 19961).

Our objective is to shed some further light onto these debates. We propose to go back to the very reasons that make the running of a program useful, i.e., the fact that its results can be straightforwardly interpreted as a statement about the real world. Starting from this simple observation, we draw the conclusion that the specification of a program only consists of (the statement of) the link relating the program (formality) and its purpose (informality). Since, as we will argue, the purpose of a program must be something directly understandable, specifications also are the essential tool for constructing, in practice, correct real-world programs through explicit but non-formal reasonings. Additionally, our discussion of specifications allows us to explain why formal specifications (i.e., specifications written in a formal specification language) are not really specifications, since this would be a contradiction in terms. Several researchers in formal methods have recently reported insights related to ours, namely that informal “comments” are inevitable adjuncts to formal specifications (Hoare, 1996; Jackson, 1995; Words- worth, 1992; Zave and Jackson, 1997), or the fact that the knowledge of the environment in which the program will be embedded is essential to the understanding and the writing of specifications (Johnson, 1988). But our reflection goes, in a sense, beyond

their conclusions, since we claim that specifications are, or ought to be, informal by their very role.

Our view of specifications does not imply a rejection of all ideas put forward in the literature on formal methods. On the contrary, we agree with the proponents of formal methods on most of their arguments, except on the fact that specifications had better be written in a formal, i.e., completely prede- fined and syntactically checkable, language. And, inevitably, we also disagree with other arguments that are a consequence of this assumption that formal specification languages are desirable.

Formal methods are in general introduced as being the use of mathematics in the process of constructing computer software (including the elaboration of specifications). We agree that mathematics are extremely useful in this context, but we disagree on reducing the concept of mathematics for computer science to the restricted framework of any formal specification language.

Program verification is advocated by most distin- guished computer scientists as the only way to improve the quality of software. We agree that program verification or, better, systematic program construction is the only way to build satisfactory computer software, but we disagree on the fact that program proofs must be automated, since, as we try to demonstrate, this would imply a vicious circle.

Requirements engineering is viewed by most authors as the most crucial stage in the development of a large software system. We agree on this viewpoint and especially on the importance of the elicitation process, but we disagree with the opinion that writing formal specifications is the best basis for the elicitation process: such a process is best achieved in a language as expressive as possible, i.e., a natural language enhanced with any desired notational conventions.

Finally, it is generally accepted that formal methods should be supported by corresponding software tools. We argue that formal descriptions of any kind (programs, finite-state automata, “declarative” descriptions, and the like) can be useful only because they can be the input of an automated process whose output provides directly understandable information that could not be realistically discovered by manual calculation. Nevertheless, the elaboration of any formal description (of whatever nature) requires a careful construction process that cannot be formal- ized in any way since this would entail a regressurn ad infinitum. Note that we do not say that such tools are useless, but only that the crafting of their inputs already is a programming activity whose mastering definitely requires explicit informal reasoning.

(3)

Specifications Are Necessarily Informal J. SYSTEMS SOFTWARE 277 1998; 40~2755296

We conclude this introduction by summarizing the articulation of our argumentation along the three main sections of the paper.

Section 2. Our main thesis, i.e., the fact that explicit informal reasoning is the essential pivot of any well-conducted programming activity, is the subject of Section 2. Such reasonings are best based on clear specifications of all sub-problems that are identified during the program construction process (including the requirements engineering phase).

Most of Section 2 (i.e., Sections 2.1 to 2.4) is devoted to demonstrating that such specifications should (and in fact can) be made extremely simple by clearly separating the statement of the purpose of the program (which should boil down to citing a well-known concept) and a set of representation conventions (whose role in informal reasonings is subordinate yet necessary since the concepts of the programming language are totally alien to the problem that the program must [help to] solve). Section 2.1 motivates our notion of specification by showing through some example problems that the results of a program are meaningless by themselves and should be interpreted in some way to allow the resolution of the problem that the program helps to solve. We also show that this interpretation necessarily takes place at an intuitive (problem-related) level. Finally, if the program is really convenient to use, it is necessary that the interpretation of the results be extremely simple. Section 2.2 draws an important conclusion from these observations, i.e., that a specification should only 1) state the purpose of the program (in a straightforwardly understandable way> and 2) state the representation conventions that one needs to know to use it properly. Section 2.3 explains why such specifications are essential to articulate the programming activity, while Section 2.4 argues that it is actually possible to craft such specifications even for “real-world” problems.

The intuitive knowledge necessary either to properly use a program or to construct it is generally not available at the beginning. In order to write good specifications of the program and of all its parts, one thus needs to build a “theory of the problem” that provides this necessary knowledge. Section 2.5 is devoted to this topic: we revisit a few classical problems in order to show that the main role of this theory is to identify useful properties of the actual, real-world problem, not of a more or less arbitrary and unreasoned redefinition of it; since the objective is to understand the problem as it is, we also dispute the idea that it is necessarily better to define con-

cepts as abstract data types or in nonexecutable style.

Section 2.6 summarizes our ideas by discussing the “general form” of specifications, while Section 2.7 draws a parallel between requirements specifications and our notion of “theory of the problem.”

Section 3 applies the ideas of Section 2 to a critique of the concept of formal specification. Since the concepts of a formal specification language are totally alien to those of any practical “real-world” problem, specifications in our sense cannot be written in such formal languages. Moreover, the correct construction of (what is usually called) formal specifications requires the use of (informal) specifications in our sense. In fact, all our argumentation of Sec- tion 2 applies as well to formal specification languages and to programming languages. This thesis is developed in Section 3.1. It allows us to discuss seven frequently asked questions about formal specifications, in Section 3.2.

Section 4. Finally, we try to explain why our view of specifications has not been largely accepted by computer scientists. The belief that all practical’ mathematics can be embodied in a single formal system is-we guess-a main reason of the importance given to formal specifications. Another important reason is the desire to find methods to measure the value of a program and the programmer’s pro- ductivity. In our opinion, such a goal is largely unreasonable.

This paper is based on the Ph.D. dissertation of the first author (Le Charlier, 1985) (and includes translations of tracts of this thesis). The first author has successfully used these ideas in several medium-sized projects (Le Charlier and Flener, 1997). The second author has used them for debunk- ing some of the myths on deduction-based and in- duction-based approaches to the (semi-jautomatic synthesis of (logic) programs (Flener and Popelinslj, 1994).

2. THE ROLE AND NATURE OF

SPECIFICATIONS

In this section, we more closely examine specifications of programs. Such specifications are the essen-

‘From a theoretical standpoint, this belief has been ruined by Giidel’s incompleteness theorem, but formalist mathematicians argue that the limitations pointed out by GGdel have no impact on mathematicians’ practice.

(4)

278 J. SYSTEMS SOFTWARE

1998; 40~275-296 B. Le Charlier and P. Flener

tial pivot of the whole programming activity: without good specifications, it is impossible to understand what the correctness of a program means and hence to reason rigorously while constructing it or constructing another program using it. In the software engineering literature, the word “specification” is used to designate many different kinds of things (such as requirements specifications, for an entire software, and detailed-design specifications, for its modules), and yet there is something in common to all of them. For the moment, we deliberately do not make precise the kind of specification that we consider, but we will come back to this issue in Sec- tion 2.7.

2.1 Why and How can a Program be Useful?

Despite all the doubts one might have about the purpose of computers for the resolution of real problems such as the creation of a more just and harmonious society, if one writes and uses programs then it is because one believes they are useful. This fact is so evident that one never wonders why and how a program can be useful. However, it is the answer to that question that leads to an understanding of what programming is and why specifications play a fundamental role in it.

If a program is useful, it is not because its execution results in displaying certain strings on the screen or in changing the contents of the computer memory in a certain way. It is because this execution yields useful information or provides substantial help in the realization of a task. But, to take advantage of the program, other things than its text and the format of its data need to be known. Even observing its behavior for some time does not suffice. It must be possible to interpret the produced results, but the knowledge necessary for this cannot be part of the program text nor of its results. It is relative to concepts totally alien to the objects manipulated by the program, and to the conventions according to which these objects represent these concepts.

Example: The Belgian National Lottery. Suppose all we know about a certain program is how to launch it on a certain computer and that its execution only results in displaying the string:

5,11,15,22,29,46

No information can be drawn from this; our lives are unaffected by the knowledge that the execution of a certain program gives exactly this result. Now suppose, to the contrary, that we know from an in- formed source that the execution results in display-

ing the next draw of the Belgian national lottery. This changes everything: everybody now sees how such a program can be used advantageously.. . .

This single example shows why a program is “not useful” by itself, but only in conjunction with some knowledge that is totally outside of it, of which neither its text nor its results can give the slightest clue. Some will now object that it is easy to change that program so that it exhibits its own purpose, say by displaying the following string instead:

5,11,15,22,29,46

is the next draw of the Belgian national lottery. But this objection is flawed for two reasons. First, it is not the simple observation of the result that allows us to understand it. The act of “seeing” the string above cannot possibly give the knowledge necessary to the understanding of the sentence it represents. This knowledge must be available before or must be acquired by other means. Second, it is not enough to be able to interpret the result of a program by an assertion in order to deduce from it whether it is true. To do so, there should be other good reasons to believe that an execution of a program can only produce outputs that represent true assertions.

Finally, if a program can be useful, even though its manipulated objects have by themselves no meaning, it is because it is possible to use these objects to represent useful information so as to be able, first, to write the program so that it computes the representations in a correct way (according to chosen conventions), and, second, to “easily finish the job” by interpreting the results.

Example: A payroll program. Let us now consider the payroll program of a company. It is useful to the extent that it is easier to (correctly) solve the payroll problem with it than without it. In any case, it is not the running of the program that solves the problem. The problem is solved if and only if the whole personnel gets their due salary at the deadline. This happens or does not happen independently of the existence of a payroll program and its results. The responsibility of the solving of the payroll problem belongs to the corresponding accountant. The program can only help her as an intermediary and is only really useful if it noticeably reduces the amount of work the accountant has to do to solve the problem. The accountant’s task is, on the one hand, to prepare the inputs to the program, and on the other hand, to exploit its results so that all employ- ees get their salary. So she must know how to use the program. This also means that she must be able

(5)

Specifications Are Necessarily Informal J. SYSTEMS SOFTWARE 279

1998; 40~275-296

to make a reasoning by which, knowing the inputs, knowing the usage she made of the outputs, and knowing “sufficiently many things” about the program itself, she can conclude that everybody’s exact salary is paid at the deadline. Nowadays, the accountant may have almost nothing to do to complete her task, but some verification (of whether the program performs its task) has to be done nevertheless.

Example: A search sub-program. Let us finally consider a sub-program that locates a value in an array. It is useful because one can use it as a primitive for writing a larger program, and this without worrying about how the search is done. How- ever, to use it properly, some supplementary information must be available: how to call the sub-program and how the results are represented. One might think this example is fundamentally different from the first one. In this case, some will say, to understand the purpose of the program it suffices to know the programming language and to have the text of the program. Indeed, the latter would be so simple that one will “immediately see” what the program does. The text would define the purpose of the program. This opinion is incorrect: to understand the purpose of the program, the concept of membership in an array must be known in advance, but it is not a concept of the programming language because otherwise it would not have been necessary to write a sub-program representing it. The opinion above stems from the fact that one might recognize quite easily an array search in the program text provided one has already done some programming beforehand, hence one already knows what an array search is, for what it can be used, and what form one generally gives to programs performing it. But this does not mean that this knowledge can be derived from the program text.

This example has been chosen on purpose among the most simple and “classical” ones, It is clear, however, that in general one does not write programs solving known problems. Therefore, the knowledge of some programming concepts and methods is totally insufficient for understanding not only the purpose of a “large” program but also the one of most of its components. To understand the use of a program computing sin(x) according to given representation conventions and a given preci- sion, trigonometry and analysis notions must be known. Pretending that the program defines the corresponding approximation is only a pleasant joke, because it is not the scrutiny of this text that can give the slightest idea about trigonometry to somebody who does not already have it.

Finally, it often happens that the concepts necessary to understanding the purpose of a (sub-)program cannot be found in our “preliminary knowledge” but must be invented ad hoc. It is well-known that the resolution of a simple problem may necessi- tate the introduction of completely new ideas. Such invention is done via definitions. But there would be a vicious circle to try and explain the purpose of a program by referring to concepts only known by their definitions: this would almost amount to saying that this purpose can be understood by examining another program. To leave this vicious circle, it is necessary to give these newly defined concepts an intuitive and objective “substance,” by shaping them into a theory allowing their understanding without any definitions. These ideas will be further developed in Section 2.5.

Note that there is an important difference between our notion of specification and the notion of requirements specification, which consists of a description of the problem to be solved. In our view, this notion should essentially coincide with what we call the “theory of the problem.” Again, we refer to Section 2.7 for more details on this issue.

2.2 What is a Specification?

“Definition.” A program specification is a statement whose role is to say (1) what purpose the program serves and (2) how the program can be correctly used.

This “definition” is not a mathematical one, but the previous discussion will help us to understand it in detail. The definition means that the specification of a program is the necessary link between what the program computes and the information that we can deduce from its results. This link is exactly what we need to use the program or to construct it.

A specification must be simple and directly under- standable. The objective of a specification is to transmit information. So there is a parallel between the notions of specification and program output. The output is meaningless by itself: it must be interpreted in order to extract the information it carries. This does not mean the particular form of the outputs is irrelevant as long as the representation conventions are known. For instance, if the task of a teller machine in Belgium is to display the balance of a bank account, then not all representations are equivalent: a decimal representation of the amount expressed in Belgian Francs is acceptable, but a

(6)

280 J. SYSTEMS SOFTWARE 1998; 40:215-296

B. Le Charlier and P. Flener

binary representation of the square root of the amount expressed in Turkish Lira is not. The good representation is the one that minimizes the work that remains to be done to transform the output into the desired information. In the example above, the first representation is the only acceptable one because the customer immediately knows how much money can be withdrawn from the account, whereas a long and tedious computation would be necessary from the second representation. Similarly, the “good” specification of a program is the text that can be transformed as directly as possible into a correct understanding of the purpose of the program and of the way of using it.

Besides this analogy, there also is a fundamental difference between a specification and the results of a program. The principal role of the specification precisely is to state how to interpret the results, but there is no need for a text explaining how to interpret the specification, as otherwise one would need a specification of the specification, and a specification of the specification of the specification, ad infinitum. Therefore, unless one completely denies the pertinence of this notion, one has to admit that a specification is a text that must be comprehensible by itself. Hence it must be written in the only language adapted to this end: natural language. We do not say that specifica- tions ought to be written in pure natural language. It can be a technical language including problem-specific concepts and notations. But it cannot be a formal language, in the strict sense of the word (i.e., whose syntax and semantics are defined a priori). Indeed, statements in a formal language are incomprehensible by themselves (also see Section 3.11, because the problem concepts are always totally alien to those of the formal language. Hence, formal statements always need to be accompanied by explicit representation conventions, i.e., informal specifications. To the contrary, informal (natural language) statements are comprehensible by themselves because they directly refer to the problem concepts.

A specification need not be correct, but only cor- rectly understandable. Since the role of a specifica- tion is to communicate the purpose of a program, the only correct means of judging the quality of a specification is to ask whether it allows every poten- tial reader to understand conveniently and in the most direct possible way the purpose of the program.

The notion of “correctness” of a specification is thus less important than the one of “being correctly understandable.” A specification can perfectly play its role, even if it lacks style, or has unorthodox

phrases, if not even mistakes and contradictions.* A reader may well have understood it even though she estimates it to be “incorrect” or poorly written, because it does not follow her own stylistic criteria or contains some obvious mistakes. But how is it possible to correctly understand a specification while judging it incorrect? The answer lies in the observation that the role of a specification is not to define everything that ought to be known to understand the purpose of the program, but only to state this purpose. Where is the difference? According to the first viewpoint, one would suppose that the knowledge necessary to use the program is entirely inside the specification (i.e., would be derivable from the specification). It would, then, be evident that an incorrect, specification cannot be satisfactorily understood by itself because it would be the only reference. Ac- cording to the second viewpoint, one supposes that the reader already knows almost everything on what makes the program interesting, the role of the specification being somehow to say “this is the program that you needed.” In this case, the presence of some errors or quirks in the specification would not really be an insurmountable obstacle to its understanding, because the enormous quantity of things already known allows the reader to fill the gaps.

All this does not imply that specifications can be written carelessly, but only that the quality of specifications cannot be judged according to hypothetical correctness criteria. The key issue is that they communicate “the message” in the most direct way. This entire argument holds of course for all consumers of specifications, be they end-users, or programmers, or whoever. Correctness is relative to an external truth criterion, and the objective is to make a software correct with respect to a fact, but not with respect to a statement in a formal theory.

2.3 Why are Adequate Specifications Necessary? The specification of a program is an indispensable aid for remembering details. After close considera- tion, it is even only such an aid, as it only has to

‘In our view, whenever a program addresses a meaningful problem, there is a model in the real world for any “correct” theory of the problem. If we fail to build this correct theory, this does not mean in any way that the model does not exist, since it is preexisting (unless we deny that the world exists). That is why we dispute the importance of self-contradiction in a theory. A theory can be self-contradictory because of a single fortuitous mistake and yet one can be able to “see” the intended model underlying it. Self-contradiction can be problematic for technical reasons in formal theories, but of course we also dispute the idea that the theory of the problem must be a formal one.

(7)

Specifications Are Necessarily Informal J. SYSTEMS SOFIWARE 281 1998: 40:275-296

state the purpose of the program but not all the knowledge necessary to understand its meaning. The customer must thus already know, before reading the specification of a program for the first time, everything that makes the program useful to her. She will then know that a program with this purpose exists and how it can be used. Later, she can occa- sionally re-read the specification, not because she has forgotten its purpose, but because she does not recall with certainty some representation details that are too arbitrary to be possible (or useful) to re- member.

Specifications are not only absolutely necessary for documentation of already existing programs, but also before and during construction of programs, for three reasons.

First, one can only construct small programs at a time. The difficulty observed in the rigorous construction (a la Dijkstra, Gries, etc.) of small programs is inherent to programming (and there is no way such techniques can ever be scaled up to constructing “real” programs), so small programs exactly represent the limit that should not be crossed if the programming activity is ever to be mastered. The only realistic approach is thus to build “large” programs from “small” ones that are constructed independently of each other, and recursively so on (no matter whether one proceeds top-down or bottom- up). This is possible only because the specifications attached to programs allow us to consider them as new primitives of the programming language, no matter how large these programs are.3 All specifca- tions should be of the same level of complexity, namely of the utmost simplicity.

Second, intermediate specifications, i.e., specifications of sub-problems perceived as potentially useful during the design of the system’s architecture, are necessary as a basis for the discussion between the computer scientist and the customer, because they are, in general, of too different backgrounds for coming up with the good specification the first time. Starting from the specification, the computer scientist must be able to make a reasoning to convince herself that she can construct the required program, whereas the customer must be able to make a reasoning to make sure the program will provide the expected service. The specification thus takes the role of a contract.

3Note that we do not assume a pure hierarchical organization of programs. For concurrent programs, for instance, a specification could (essentially) consist of a global invariant and some fairness properties.

Third, intermediate specifications are necessary during the design of an architecture for the program. Strictly linear top-down design is difficult, and the implementation of certain sub-problems may reveal inadequacies in earlier choices, forcing backtracking in the design, if not the deletion of already written code. Since programming is costly, there is a risk of trying to preserve at all cost what has already been done, even if this means going into blind alleys. A more reasonable approach is thus to write all specifications of all sub-programs before writing the first line of code. This requires mental persuasion that the program can be written using all and only the specified sub-problems. Designing such an architecture may still require backtracking, but it is less tedious to rewrite specifications than programs, and easier to persuade oneself that a program can be written than actually writing it.

2.4 Can there be Adequate Specifications (for Real-World Problems)?

We think that adequate specifications, according to our criteria, can be written, even for real-world prob- lems. We know that most examples in this paper are small-scale-and space reasons prevent us from cov- ering real-world problems-but our considerations do scale up, by their very nature. The first author has successfully applied them to rather complex medium-scale problems, as reported in (Le Charlier and Flener, 19971, and he believes that he was successful precisely because of this mind-set.

A specification is not meant for everybody. Only a program with a precise purpose should have a specification. Saying that a program has a precise purpose amounts to saying that somebody is able to exactly understand this purpose. So the specification of a “useful” program will always exist because somebody must be able to say what its purpose is. But this does not mean that everybody can understand this specification. It is only comprehensible by somebody having the “same background” as its author, at least as far as the application domain is concerned. The existence of satisfactory specifications is thus only possible because they are only meant to be read and understood by people already knowing almost everything of the application domain in which the program has its purpose. This does not imply that only the specifier will be able to understand it or that this privilege is reserved for a select few. It simply means that every user of the program must

(8)

282 J. SYSTEMS SOFTWARE

first make a careful and sufficiently long study of its application domain.

Remark. In practice, it is unfortunately rare that a person understanding the purpose of a program can express it simply. Programmers, for instance, tend to give incomprehensible technical gibberish about the implementation technique and run-time behavior when prompted to explain what their programs do, instead of talking about the essen- tials. The absence of specifications for many actually used programs stems from an inability of many people to express themselves clearly. (As already said by others before:) Instead of includ- ing specification rules or formalisms in computer science curricula, it would be much better to teach students how to correctly use their natiue language (or natural language, in general).

Another reason for the absence of convenient specifications is that programs are often constructed by successive approximations, by trial and error, so that there cannot possibly be a convenient specification, because nobody is able to understand how to use it. But it is precisely because the programmer was unable, or thought it useless, to write a specification that she, not knowing what to do and hoping to find it out progressively, constructed a mysterious program to which no specification can be attached.

A specification should have an objective meaning. Some will object to our notion of specification by saying that two different people never understand things in exactly the same way, so that we can never be sure whether a specification is correctly understood by all concerned people. However, it is not necessary that the programmer and all users of a program understand its specification in the same way. Note that such a condition is insufficient anyway, because it does not matter whether all people have understood exactly the same thing, but rather whether everybody has understood what is needed to do their job. And this new condition can be fulfilled because the specification of a program must express a property that has an objective meaning. It is true that nobody understands this meaning completely and in the same way as their neighbor, but everybody should understand that the question of correctness of the program with respect to its specification corresponds to a fact, and not to personal interpretation. The programmer must be able to construct the program by making a reasoning to persuade herself that it has the desired property;

whereas the users must be able to derive other facts from it, such as the possibility of doing their job using the program.

For instance, consider a program computing the sine function under certain precise conventions. The programmer need not completely know the “es- sence” of this function, but only sufficient properties for constructing a correct program. The users need not understand the function in the same way as the programmer, but only other properties allowing them to solve their problems. So it is because of its objective nature that the specification of this program will be satisfactory: it expresses a fact, the same for everybody, even though they may understand it differently. Hence the specification should act as the “ultimate” reference, i.e., the last thing to be doubted about and hence the central pivot of any reasoning about the program.

A not completely unfounded objection to the previous example is that it is not realistic because the sine concept has been studied for such a long time that it would be foolish to deny its objective nature, but that not all specifications can be expressed in terms of such well-established concepts. Indeed, this objection pinpoints one of the fundamental diffi- culties of programming compared to, say, mathematics: one never has the time to polish all the needed concepts for a specification, because the program is needed urgently.

Nevertheless, the objectivity condition for specifications seems absolutely necessary for the correct communication of the purpose of programs, and, hence, for mastering the programming activity. Ac- cording to us, without this condition, one would have to admit that the usage of programs for achieving a certain activity amounts to redefining that activity as being the exploitation of the results of the program without giving a satisfactory link between this redefinition and the initial concrete problem. Moreover, to us, this condition seems largely achievable, if one admits that the objectivity of the concepts necessary to the writing of good specifications can be founded on the creation of a “theory” of these concepts, with more or less detail according to the imperatives of the problem, a theory that can be studied by all concerned people until each of them has convinced themselves personally that it really corresponds to the intended object.

This perception of course has the “disadvantage” of founding the mastery of programming and its usage on the competence and responsibility of people, whereas some would prefer to found them on rules that are easy to apply and verify.

(9)

Specifications Are Necessarily Informal J. SYSTEMS SOFTWARE 283

1998; 40:275-296

2.5 Role and Content of the “Theory of the Problem”

The intuitive knowledge necessary either to properly use a program or to construct it is generally not available at the beginning. In order to write good specifications of the program and of all its parts, one thus needs to build a “theory of the problem” that provides this necessary knowledge. In this section, we revisit a few classical problems in order to show that the main role of this theory is to identify useful properties of the actual, real-world problem, not of a more or less arbitrary and unreasoned redefinition of it; since the objective is to understand the problem as it is, we also dispute the idea that it is necessarily better to define concepts in an abstract data type or in non-executable style.

Since a program is normally constructed in order to help solve a practical preexisting problem, the concepts and objects of such a theory can be classi- fied into two main categories: those whose identity was determined before and independently of the program, and those that are defined (or, better, identified) especially for the construction of the program. They should all have the same final status, namely to be known not by their definitions but by a sufficiently rich set of properties linking them to numerous other concepts. They thus have their own individuality, equivalent to an objective status. The theoretical development necessary for achieving this status is different and more or less long and difficult according to the category of concept. We elaborate on these issues in Sections 2.51 and 2.5.2. In Sec- tions 2.5.3 and 2.5.4, we discuss some aspects of definition construction, stressing that there is no purely abstract way to define a concept and that the non-executability of definitions is not necessarily a desirable objective.

2.5.1 On the Study of “Long-Established” Con- cepts. Defining once again preexisting concepts is common practice in formal methods of program design. It is however unwise to start the study of a predetermined concept by defining it. Indeed, what is necessary is to study the concept as it is, but not another concept given the same name through a definition. Even if a “predetermined” concept can be considered completely determined by a certain property (i.e., all other properties useful to the problem at hand can be derived from that property), one cannot consider it a definition of the concept. On the contrary, one would have to ensure that the concept really has that property. The objective of the theory to be built is to ensure that things are

sufficiently well-understood by all involved people. If one started redefining all the fundamental concepts of the problem, nothing would be known about the relationship between the (preexisting) problem and what has been done. In any case, all involved people have a preliminary understanding of the problem. The role of the theory is to make things precise, if not to correct them, but not to reconstruct everything from nothing. It is thus more important to stress the difficult or delicate issues than to try and found everything already known.

The case of mathematical concepts. Suppose the concept of “greatest common divisor” is needed in the resolution of a programming problem. It is not the following redefinition of this concept that makes its role in the problem more precise:

Definition 2.1. The greatest common divisor of two natural numbers m and n is a natural number p, denoted by gcd(m, n), such that p divides m and IZ, and, for every natural number i, if i divides m and n, then i divides p.

Indeed, if one does not already know the concept of greatest common divisor (gcd) and its applications, this definition will not, by itself, help one understand its purpose. But let us consider a person who already has a good idea about it. The only information she can draw from this definition is that it probably is the definition of the notion of greatest common divisor that she already knows. Therefore, the only immediately useful part of this definition is the only word that is theoretically arbitrary! Indeed, one could define the same concept by naming it “foo” or “Nabuchodonosor.” Two things are possible from here. Either this person is satisfied with her conclusion, and then the definition has not brought any new information, or she wants to verify this first impression by examining whether the definition is compatible with her existing knowledge of the concept of gtd. In this case, she might not be able to do so immediately, because her definition rather says that gcd(m, n) is the greatest of the divisors of m and n, according to the usual ordering relation. To show that the two concepts coincide, she actually has to make a long reasoning, which should by the way conclude negatively, because they do not coincide when m = n = 0 (where the greatest common divisor is usually considered undefined, but the definition above gives gcd(O,O) = 0). Anyway, at the end of this superb intellectual effort, she will still not know whether this definition was introduced for the fun of scrambling the message or for some better

(10)

284 J. SYSTEMS SOFTWARE

1998; 40:275-296 B. Le Charlier and P. Flener

reason. To conclude, it would have been better to admit that the concept of gcd is predetermined beyond all definitions and to show why the very close concept of greatest common divisor according to the “divides” ordering relation was substituted for it. For instance, it could have been because one wanted to be able to apply, in all cases, the formula gcd(m, g&z, p>) = gcd(gcd(m, n>, p). (For m = n

= 0 and p # 0, only the left-hand side of this equal- ity is defined according to the usual definition.)

The case of “non-mathematical” concepts. The preceding precept applies unchanged to any kind of problem. It is not because the program to be written has its purpose in, say, an accounting setting, that one has to start by defining all involved concepts in order to understand its purpose.

For instance, in the payroll program, the “theory” of the problem should not start with definitions of employees, salaries, companies, etc. What is necessary is to arrive at a sufficient understanding of these concepts (which are perfectly determined, even if they might be poorly understood at the beginning) in order to solve the problem. It would not be acceptable either to define the effect of the program by the rules of computing the salaries in terms of the employee database. One should study the legisla- tion, the structure of the company, etc., in sufficient detail so as to be able to deduce (i.e., to justify, by a rigorous reasoning) an adequate structure for said database as well as valid computation rules. The user of the program (i.e., the accountant) need not have studied all the details of the “theory” that the programmers have had to elaborate, but she should understand it sufficiently for correctly using the program. It would be hard to say where the limit is: it is her responsibility to decide herself how far to go in order to reach a sufficient understanding.

2.5.2 On the Study of Concepts “Tailored for the Problem”. The writing and understanding of “good” specifications of programs nearly always requires using concepts especially tailored for the problem, discovered or created especially for constructing the program. Such concepts can only be introduced by definitions, but those definitions must be validated explicitly against our perception of the problem in order to ensure that the concepts adequately relate to the “real” problem.

The case of simple concepts that are close to known ones. One often has to deal with concepts that can be considered already implicitly known and

understood by all people who have to use them, but whose relevancy is insufficient for having been given a name that is universally admitted. It is then necessary to have recourse to a definition for naming the concept and making everybody agree on some important details whose identification is necessary for correctly using it. When reading such definitions, it should be possible to “immediately see what they are about.” The concept-specific theory then reduces to only a few things, because the concept “naturally takes its place” among already known ones.

Let us illustrate this with a specification of the classical plateau problem.

Definition 2.2. Let S = (sl, s2,. . . , s,J be a finite non-empty sequence of integers. A plateau of S is an interval4 (i : j) such that:

1. lliljln

2. si = si+l = **- = Sj

3. (i : j) is not strictly included in any other interval with properties (1) and (2).

Problem: Given a non-empty initialized array a[1 . . n] of integers, construct a program that as- signs to integer variable np the number of plateaus of the sequence (a[ 11, a[2], . . . , a[ nl>, and to integer variable maxZp the maximum of their lengths (the length of a plateau is the number of its elements).

The definition in the specification above is sufficient for a satisfactory problem statement, for two reasons. First, the “technical” concept of plateau is not brand-new, but rather a particular and precise oc- currence of a more general concept that we already know (the choice of the name “plateau” is thus not arbitrary). Second, this definition is sufficiently simple for linking this particular concept to the general one, that is for verifying whether the chosen termi- nology really corresponds to something intuitive. Moreover, the definition is necessary, because the intuitive notion of plateau is too vague for being able to rule out, in its absence, a misunderstanding of the notions of number and length of the plateaus of a sequence.

On the usefulness of examples. Specifications may be accompanied by carefully chosen examples, so as to facilitate their understanding. Since the role of a

4We assume the concept of interval is already known: (i: j) = (n Ix is an integer and i s n I j}, where i, j are integers.

(11)

Specifications Are Necessarily Informal J. SYSTEMS SOFTWARE 285

1998; 40:275-296

definition, as considered here, is not to be formally irreproachable (i.e., non-contradictory, for instance), but to help understand something, there is no reason to reject other means of communication that might have other qualities. Some well-chosen examples often provide an intuitive understanding that no definition could achieve. The latter then only makes more precise the exact contours of the concept. Other examples could help eliminate certain risks of ambiguity in the definition by illustrating delicate issues that are likely to be misunderstood for whatever reason.

As far as the risk of contradiction between definition and examples is concerned, note that this kind of contradiction would only be a real disaster if it were the non-contradiction of a definition that would lend value to a concept. There is a confusion here between truth and non-contradiction. What is important is to make known what one wants to say, not to escape contradiction. One could even argue that the discovery of a contradiction between an example and a definition is the best thing that can happen in some cases, because it carries an undeniable message: something is wrong somewhere!

Personal experience5 shows that a “poorly defined” concept can be perfectly understood thanks to examples, especially when the concept can be considered already implicitly known. Definition and examples are thus complementary means of desig- nating the concept. And one may well conclude that there is only one concept corresponding to both the definition and the examples, even if one has spotted an apparent contradiction between them. What one already knows helps understand the error. Finally, note that the error risk is much higher in a definition than in an example, because it has to cover all cases. Examples are more reliable, because more “local,” and are thus an ideal means of getting things straight.

Let us illustrate this on the plateau problem. Assume condition (3) was omitted from the definition above, but that the following example was added:

Example 2.1. If S = (1, 1,3,3,3,2,3,5,5), then there are 5 plateaus of S, namely (1: 2>, (3 : 5), (6: 6),

5A few examples: as a student, the lirst author had to use the PL/I language and found it completely impossible to understand the manuals except from the examples. As teachers in program proving, both authors always give examples to support program specifications. In a few cases, we eventually discovered errors in our specifications, although the students had understood them perfectly well.

(7 : 7), and (8 : 9). Also, its longest plateau is (3 : 5), its length being 3.

Starting from the definition and the example, one easily understands that plateaus are the longest non-empty intervals (i : j) included in (1: n > such that (2) holds. One could even have understood this without noticing that the definition is incomplete.

On the usefulness of remarks, or, better, of a “reasoned” presentation of definitions. All this shows that it is difficult to correctly define a concept in order to explain it to somebody else. In a sense, writing the definition is already a programming act. A definition is thus always the product of a more or less explicit reasoning process. So if one wants to facilitate the correct understanding of a definition, one could point out delicate issues in remarks, or, better, one could make explicit this reasoning process.

For the plateau problem, one might want to point out that the notion of plateau only makes sense with respect to a sequence S, that a plateau of S is always a non-empty interval, and that the set of plateaus of S partitions the interval (1: n), where II is the number of elements of S.

To do even better, one might show how the given definition was reached from a “reasonable” intuition of the concept of plateau of a sequence. This could go as follows.

Let

s =

(s1,s2,..., s,J be a finite non-empty se-

quence of integers. Let us draw a coordinate system, and mark the points at coordinates (i, si), for 1 I i I II. Let us now draw, from each of these points, a horizontal segment of unit length. Some of these segments can be merged, giving rise to disjoint segments of integer length, called plateaus of the sequence:

6

i

I

I I I I I,,,,,,

1 I 3 4 5 6 7 8 9 10 II

(12)

286 J. SYSTEMS SOFTWARE

The objective is to write a program for computing the number of plateaus of a sequence and the maximum of their lengths. It is obvious that to each plateau corresponds an interval verifying conditions (1) to (3) [included here’as above], and vice-versa. Moreover, the length of a plateau is the number of elements of such an interval. This leads us to the following redefinition of the plateau concept, for our problem: [here follows the definition above].

This presentation clearly allows one not only to understand the definition more quickly, but also to “verify” it according to one’s own criteria. We even claim that such an intuitive presentation is self-sufficient and even preferable to the definition, as the latter is only a property of plateaus that one might discover by oneself.

A final remark: in practice, it is not always useful, nor possible (for “financial” reasons), to discuss all introduced “simple” concepts in this much detail. An acceptable compromise between the quality of the presentation and the time invested to its tuning must be found. Only experience shows where to situate this compromise. The most important thing is to understand that the objective is always the same: to capture the posed problem as well as possible, as it is.

The case of more complicated or “new” concepts. Sometimes, the solving of a programming problem requires the invention of relatively original concepts that one cannot pretend having known before tack- ling the problem. They can thus not be imagined from nothing, but only constructed in small steps after comparing the problem to what is already known. The role of a definition is then to anchor some ideas for further investigation: one must be able to deduce many other properties from it, estab- lishing thus the usefulness of the concept for solving the problem at hand. The concept thus offers economies of thought and reveals ways of solving the problem. The choice of a definition is guided by an intuition, i.e., the impression of having perceived an analogy with something already known, This definition is, in general, not the good one, because it may later turn out that not all the “desirable” properties can be derived from it, so that it does not play an efficient role in the problem solving process. The definition then has to be modified, in the light of these first conclusions, and so on, until the “good” concept has been obtained, namely the one that holds the key to the solution, or part of it. At the

end of this process, whose essential steps must be reconstituted by all “clients” of the concept, the latter is known beyond the finally adopted definition. It is known by numerous properties linking it to other concepts. It has become “intuitive and well- known” and its definition is only one of its properties, among many others.

Remark. The distinction made here between “sim- ple, implicitly known concepts” and “complex, new concepts” is of course too crude. They are only the extremes between which intermediates can be found, corresponding to a gradation of the effort to be done in order to construct a theory.

2.5.3 Only Representations of Concepts Can Be Defined, not the Concepts Themselves. To justify even more that the definitions introduced during the analysis of a problem are not the ultimate reference point for judging the value of a “solution,” but only (imperfect) means of communication or “transient” starting points that can be (or actually should be) forgotten once the concept is well-understood, it is interesting to remark that a definition never really defines a concept, but only a certain representation thereof. This remark ruins, by itself, the “absolute” character of definitions by showing why they can be “wrong”: whereas a concept cannot be something else than itself, its representations can be incorrect, i.e., can fail to respect the (implicit or explicit) rules according to which they are supposed to represent the concept.

In our opinion, a concept worthy of this name must have a real and original identity that makes it indivisible, distinct from every more or less complex combination of “simpler” concepts. A concept is an atom of thought. Therefore, an interesting concept will always escape any particular definition, because one can define, from given concepts, only combina- tions thereof, i.e., nothing really new.

All this is particularly clear for “old,” universally known concepts: for instance, whatever effort is undertaken to define natural numbers must be arbitrary. A natural number is what it is and cannot be reduced to anything else. Any definition thereof rests on representation conventions that had better be fixed very explicitly if one wants to wind up with a satisfactory definition.

But all this is still true for “new,” problem-tailored concepts. For instance, the concept of plateau of a sequence introduced above by a definition corresponds, in fact, to an intuitive concept that is very precise, but impossible to communicate as it is. This