🚀 go-pugleaf

In article <130200018@p.cs.uiuc.edu> johnson@p.cs.uiuc.edu writes:
>
>Research in formal verification has had many influences on CS.  One of
>the most important is that it has taught us what is difficult.  For
>example, it showed that goto statements were hard to think about.
>It also shows that pointers are hard to think about.  This is why
>lots of modern languages, especially the symbolic ones, don't have
>explicit pointers.  However, the effect is for programming language
>designers to borrow good ideas from the specification people.  I
>think that the future will lie in that direction.

I have been interested and rather surprised to read the articles by
Ralph Johnson which seem to be saying there is no place for formal
specification as distinct from programming in today's software
technology.

My own experience with Smalltalk-80 is that much of the time
I need to ask the question "what assumptions, exactly, does
this method make about the current state of affairs?".

In many cases this question is hard to answer. Nevertheless, if
for example I wish to alter a method, in the hope that my modification
will be a proper generalization and thus not break any
current clients of the method, I must get the answer exactly right.
Therefore I would greatly value some formal assertions which
would enable me to know the assumptions exactly.  A system of
verifying the assumptions statically would be very helpful too.

A first step towards this would be a type-checking scheme, and of
course Ralph himself has done a great deal of work in this area.
An obvious further step would be a more powerful system of static
assertions, such as the preconditions, postconditions and
invariants provided in the Eiffel system.  A step from there
would be automated support for verification of these
assumptions, and a range of more expressive constructs.

The notion of software contracting surely requires this kind of
support to make sense.  An effective contract says exactly what
is agreed without unnecessary verbiage: just like a formal
specification.  Surely Ralph Johnson is not saying that the
contract between the supplier and user of a software component
must be based on the source code?

Once the need for a language, or sub-language, of assertions
has been acknowledged, the possibility of reusability in this
domain itself emerges.

In summary I claim that formal declarations of program
properties (i.e. specifications) do play a very
important role, as statements of contract between suppliers and
consumers of software components.  Smalltalk itself in my
experience is not well-suited to this task.


-- 

Mr Steve Cook              JANET: steve@cs.qmc.ac.uk
Research Fellow             ARPA: steve%cs.qmc.ac.uk@nsfnet-relay.ac.uk
Dept of Computer Science
Queen Mary and Westfield College, London E1 4NS.       01 975 5236