Conference rusure::math

    The subject of using formal methods for writing the specifications of a
    program could generate a lot of intersting discussion, Some say it is
    not a pratical approach to use "pure" formal methods, I've taken a
    gradute course with an authority on the subject, Dr Laski of Oakland
    university, Rochester, MI. he has the idea that formal specifications
    could be used for  prototyping, to see if you specs are correct, there
    are translators that would use this specs with some user "action
    routines" to let you test you specs early on.
    I think formal specs are more suitable for some types of programs than
    othors. example for scientifc, maths, or fields where the states of the
    program is not too fuzy, i.e. I dont think these methods would work
    too well in Real time specification or Communications etc..
    but that is only an opinion..
    Good luck,
    /naser
    

    Several minor points:

    - More or less formal specifications are executed all the time -- at
      least hardware specifications are.

    - There are two general forms of specifications: assertional and
      procedural.  A procedural specification says "do something which has
      the same effect as this code, but don't necessarily do it the same
      way."  To an optimizing compiler, or to a program transformation
      system, an ordinary programming language is a procedural
      specification language.

      Programming languages which are good for "pure" procedural
      specification have ways of being indeterminant about things so that
      they don't over specify.  For example, it is difficult to state
      procedurally in a standard programming language "find an element
      in this vector which matches this condition", because you usually
      end up specifying "find the first element ..." or whatever.  You need
      to access the elements in an indeterminant order.

    - There is a technique called "symbolic execution" which can turn
      procedural specifications into assertional ones -- but it needs help
      with loops and recursions.

    - There was a project quite a while a go at the Information Systems
      Institute (I think that is what ISI stands for) in LA.  It was a
      system for programming by incremental assertions.  You would start
      making assertions about the desired behavior of your final program.

      In the earliest stages of specification, the system could only check
      consistency of your assertions.  When there was enough information
      it would attempt to execute the specification by making additional
      assumptions.  Those assumptions could be examined and either accepted
      as permanant or rejected by the developers.  At some point, further
      assertions would be added to steer the system to developing efficient
      implementations.  At some point, there would be a sufficiently
      efficient program and you could quit.

    - It isn't hard to write specification interpretters -- the trick is
      writing them so that they are efficient with relatively few details
      specification.  You can always do a brute force search for sets of
      values which conform to the constraints imposed by your assertions --
      it just may take a few million years.

					Topher

    Having posted my "Z anyone" note in several conferences I did get a
    reply from Gary (TLE::) Feldman that they have a Larch technology
    transfer going on.

    In general the hardware world, Europe, and Japan are way out in front
    in use and apparent application of  formal methods for design
    specification and implementation.  If "Software Engineering" is to mean
    anything we'd better get our house in order.  How many Electrical
    Engineers can do their jobs without the fundamental basics of circuit
    theory, differential equations, etc.?  

    To answer Seig's (.0) questions directly; my knowledge of the current
    state of the world follows according to Seigs original question
    numbers.  Since I'm sure I'm not omniscient there are sure to be
    omissions and errors...(no "flaming arrows" please! 8^) )

    Here it goes...!

    (0) No.  Most of the symbols can be created in any WYSIWYG editor.  I
    have a set of ASCII di-tri-quadgraphs for the symbols in Z.  Any system
    that allows manipulation of these symbols has some control/compose key
    sequence.  The world is not text-cell anymore...  The symbols should
    not seem strange to you if you have done much reading.  A good book is
    C.A.R. Hoare's "Communicating Sequential Processes," J.C.P Woodcock's
    "Software Engineering Mathematics" and, for a brain-teaser, Fred
    Kr�ger's "Temporal Logic of Programs."
    
    (1) No.  Digital is *way* behind IBM on this one.  Dr. J.C.P. Woodcock
    has done work with Z (pronounced "Zed") and if I remember right has
    done extensive work using Z with CICS.

    (2) All projects should use formal methods.  An analogous question to
    ask is "When does an aeronautical engineer not use fluid dynamics?" 
    The software world has been filled with super-hackers who memorize a
    language, all its quirks, and then hack until they get it right. 
    But to answer Seig's question here are the criteria I've assimilated.
    If the answer is yes to any or all, use formal methods:
    	1) Is it a life-at-risk system? (flight control, medical control,
    	   machine control, etc.)
    	2) Is it a high security system? ( Military, Banking, Open network
    	   --a.k.a. public access attacks--, etc.)
    	3) Is it a high reliability system? (Databases, Operating Systems,
    	   File Systems, see 1) and 2) above)
    	4) Will the customer sue you for flawed merchandise? (The Japanese
    	   have sued HP for electronic CAD software that didn't work right)
    It is interesting to note that the Japanese use a high degree of rigor
    in their system design.  While it isn't strictly formal methods, it's
    the next best thing.  Quality is where it's at!

    (3) I know VDM and Z fairly well.  Larch I am learning.  Here is my
    best concise answer.

    Differences between:

    	VDM: Monolithic proof, reasoning from fist principles for all
    	     statements.  No ALGOL based language translation.

    	Z: Schema based proof, reasoning from a rich set of axioms,
    	   modularity with generics, promotion of proved subsystems to
    	   a total system. No ALGOL based language translation.

    	Larch: Two tiered approach.  Language independent portion with a
    	       language dependent portion to make ALGOL based language
    	       translations. (See opening statement above).

    	Prototyping: Rigor in human understanding of system, no
    	             mathematical basis for correctness of system.  Very
    	             human opinion oriented.

    (4) I haven't found one yet.

    (5) We have a CMP with Quintus Prolog.  There are better Prologs out
    there, but Digital doesn't have any in-house with a corporate license. 
    I don't know of any in-Digital implementations of theorem checkers, I
    know that Larch is the nearest to being done.  Don't over emphasize the
    compiler aspect of such notations.  There is one hell-of-a learning
    curve out in the general software industry.  Take a quick quiz in your
    office on set theory, temporal logic, etc. and see if anyone can work
    the trivial examples by hand.
    
    
    Regards,
    
    Richard

           <<< TURRIS::TURRIS$DUA18:[NOTES$LIBRARY]DECSPEC.NOTE;1 >>>
                                  -< DECspec >-
================================================================================
Note 1.0                          Introduction                        No replies
TLE::WILD "Joe Wild"                                 37 lines  23-APR-1991 14:55
--------------------------------------------------------------------------------
This notes conference, TURRIS::DECSPEC, is for discussing issues related to
the DECspec Project, the Larch Formal Specification Methodology, and other
aspects of formal methods, especially those related to software.  This is
an unrestricted conference.  Its contents are for Digital Internal Use
Only.

The DECspec project is developing a toolset to support the Larch
Methodology (for the formal specification of module interfaces).  Our
intentions are to provide a toolset that will be useful in a production
environment.  See note 2.0 for more detailed information.

We will post information on the availability of the DECspec Toolset,
project status, Larch/C examples, and other general information related to
the DECspec Project and Larch.  Feel free to post comments and questions on
Larch and DECspec, or on other Formal Methods.  Please to not post toolset
bugs here.  We will open up another conference for that purpose.

We are particularly interested in hearing about other work and interest in
Formal Methods.  Please introduce yourself in note 5.0.

This conference is organized as follows.

    1.0         Introduction (this note)
    2.0         What is DECspec.  (further explanation)
    3.0         Larch Examples
    4.0         Kit Information (where to get the DECspec toolset)
    5.0         Introductions (please introduce yourself)
    6.0 - 20.0  Reserved for future use
   20.0 and on  Open for discussion 
 

We are looking for people who are interested in using and evaluating
our tools and methodology.  If you or anyone you know is interested in
learning Larch and using the DECspec toolset to specify C modules, please
let me know.  We hope to have our tools available in May.

Joe Wild, DECspec Project Leader 

People interested primarily in mathematics per se are unlikely to be
interested in "formal methods". I am probably mistaken, but I do not
think the mathematics involved is either amusing, or deep: bread
and butter, not cake.

However, people who are interested in how mathematics is applied,
especially in a field of engineering where we do *not* have an established
repetoire of modelling techniques would certainly find plenty to
think about.

For what it may be worth, I think the mathematics involved is
(roughly speaking) the study of trajectories in a discrete state-space,
and classification of sets of such. Leslie Lamport is someone who seems
to have thought harder and better than most about the mathematical basis
of discrete systems, and I'd highly recommend looking at his SRC reports
(e.g. 66,57,29).

The formality of formal methods is more a matter of logical hygiene,
Leviticus style, and likely to appeal to moralists rather than
mathematicians. Still, Leviticus served a very real purpose.

The modelling relation between, say, a transmission line, and the
differential equations (or whatever) with which the electrical engineer
describes it, is (I believe), unproblematic. On the other hand, the
relation between a pile (or piles!) of high voltage iron, screen phosphors,
and ferrous oxide, and whatever we should use to describe its behaviour
when running a program is a bit more obscure. We don't have the cliches yet.
Although lots of people say "its easy, you just ...". The temptation to
believe in easy answers is quite natural.