Specifications Are Necessarily Informal or: Some More Myths of Formal Methods
B. Charlier, and P. Flener. Journal of Systems and Software, 40 (3):
275--296(March 1998)
Abstract
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.
- öur main thesis: that explicit informal reasoning is the essential pivot of any well-conducted programming activity"
- part of the problem with formal methods is that it suggests all requirements are formalizable. To validate something, one must have an explicitly defined understanding of what that something is. However, programs exist in a world, part of a process of a consensual domain (Maturana, constructivism).
- thesis kinda agrees with a concern I've had for a while, that more understanding of formal language comes from carefully chosen symbols than from the language itself eg. member(a,x) means nothing on its own, except I have a shared conceptualization of membership which defines that this means a is a member of x.
- some of their argument sounds like the ecological approach; that is, users/programmers should understand what the system is trying to do before arguing whether it does it or not.
- argue it is almost as hard to write a correct formal spec as the program itself.
- argues that Easterbrook et al., 1998 are not doing formal specs but merely elaborating a theory of the problem.
%0 Journal Article
%1 lecharlier98
%A Charlier, Baudouina Le
%A Flener, Pierreb
%D 1998
%J Journal of Systems and Software
%K 2106 formal requirements
%N 3
%P 275--296
%T Specifications Are Necessarily Informal or: Some More Myths of Formal Methods
%U http://scholarsportal.info.myaccess.library.utoronto.ca/cgi-bin/sciserv.pl?collection=journals&journal=01641212&issue=v40i0003&article=275_saniosmmofm
%V 40
%X 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.
@article{lecharlier98,
abstract = {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.},
added-at = {2006-03-24T16:34:33.000+0100},
author = {Charlier, Baudouina Le and Flener, Pierreb},
biburl = {https://www.bibsonomy.org/bibtex/26bce166baf4e66089490e6254b5fc2e6/neilernst},
citeulike-article-id = {266208},
comment = {- "our main thesis: that explicit informal reasoning is the essential pivot of any well-conducted programming activity"
- part of the problem with formal methods is that it suggests all requirements are formalizable. To validate something, one must have an explicitly defined understanding of what that something is. However, programs exist in a world, part of a process of a consensual domain (Maturana, constructivism).
- thesis kinda agrees with a concern I've had for a while, that more understanding of formal language comes from carefully chosen symbols than from the language itself eg. member(a,x) means nothing on its own, except I have a shared conceptualization of membership which defines that this means a is a member of x.
- some of their argument sounds like the ecological approach; that is, users/programmers should understand what the system is trying to do before arguing whether it does it or not.
- argue it is almost as hard to write a correct formal spec as the program itself.
- argues that Easterbrook et al., 1998 are not doing formal specs but merely elaborating a theory of the problem.},
description = {sdasda},
interhash = {f64ab2fa90c4c2f7d4e82e622c417a87},
intrahash = {6bce166baf4e66089490e6254b5fc2e6},
journal = {Journal of Systems and Software},
keywords = {2106 formal requirements},
month = {March},
number = 3,
pages = {275--296},
priority = {0},
timestamp = {2006-03-24T16:34:33.000+0100},
title = {Specifications Are Necessarily Informal or: Some More Myths of Formal Methods},
url = {http://scholarsportal.info.myaccess.library.utoronto.ca/cgi-bin/sciserv.pl?collection=journals\&journal=01641212\&issue=v40i0003\&article=275_saniosmmofm},
volume = 40,
year = 1998
}