Abstract

		  Specifications Are Necessarily Informal
		   or: Some More Myths of Formal Methods

	    Baudouin Le Charlier (University of Namur, Belgium)
		 Pierre Flener (Uppsala University, Sweden)

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  purpose  (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.

Keywords:  specifications (of requirements & programs), program correctness,
           limits of formalisation.

Contact author: Pierre.Flener at it.uu.se