🚀 go-pugleaf

In article <1954@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>That is an argument for higher-level programming languages (with
>dynamic typing, for instance), not an argument for adding another
>language (the specification language) to the process of implementing
>software.  If your specification is so great, why not make that your
>programming language?

If what I wrote about LOTOS was written well enough to be clear :-),
you would have noticed that this is what I recommend.  You can express
constraints in LOTOS and then use formal manipulations to generate a
state machine which meets those constraints.  I saw one conference paper
where an algorithm was presented whereby the network service is specified
in LOTOS and the algorithm slices and dices it into a finite-state-machine-based
protocol engine.

>]... experience has again and again shown that formal
>]specifications tend to have fewer bugs than informal specifications.

>I'll bet that is heavily dependent on the application.

Maybe.  The applications here were specifications of network protocols.

>When I try to implement an informal specification in any programming
>language I usually find "bugs" in the specification.  No win for
>formal specs there either, it is just the process of going into
>details that finds the problems.

I think there is a qualitative difference as well.  For example, it is possible
to formally subject the specification to "undefined reception" error tests.
(The equivalent, if you will, of "message not understood", except much
more common.) Using the right level of formalism lets you get away from
the nitty gritty details of storage management, timing, system dependencies,
and so on, while you are specifying what you want. 

If you are speaking about network protocol specifications, then getting rid
of the bugs in the specification instead of in the implementation makes
things more robust (as people tend to make the same implementation decisions)
and prevents people from having to bugfix things over and over with each
implementation.  

The real win is when you use a formalism so well suited to the task that
even the customer can understand it.  For example, if you are programming
life-insurance software (:-), using Lotus 1-2-3 (not LOTOS) for a specification
language makes a lot of sense, and even the underwriters can understand what
you are talking about. There's even a tool to test it :-)!   -- Darren




>--
>					David Gudeman
>gudeman@cs.arizona.edu
>noao!arizona!gudeman


-- 
--- Darren New --- Grad Student --- CIS --- Univ. of Delaware ---
----- Network Protocols, Graphics, Programming Languages, FDTs -----
     +=+=+ My time is very valuable, but unfortunately only to me +=+=+
+=+ Nails work better than screws, when both are driven with screwdrivers +=+