Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!usc!rutgers!njin!uupsi!rodan.acs.syr.edu!wotan.top.cis.syr.edu!greeny
From: greeny@wotan.top.cis.syr.edu (Jonathan Greenfield)
Newsgroups: comp.sys.transputer
Subject: Re: re proving programs correct
Message-ID: <1991May21.110138.16049@rodan.acs.syr.edu>
Date: 21 May 91 16:32:27 GMT
References: <4202.9105202128@prg.oxford.ac.uk>
Reply-To: greeny@top.cis.syr.edu (Jonathan Greenfield)
Organization: CIS Dept., Syracuse University
Lines: 40

In article <4202.9105202128@prg.oxford.ac.uk> HALLAM@physics.oxford.ac.uk ("Phillip M. Hallam-Baker") writes:
>
>When they say
>that occam programs may be proven correct they mean that an exact definition
>of the occam language exists.

I suspect that the assertion would not be made solely on the basis of a
denotational semantic definition of the language.  There must also be a
complete set of proof rules that have been developed on the basis of those 
semantics, in order for one to reasonably claim that programs may be proven
correct.

>Because occam is a simple language this is
>possible. Most computer languages are defined imprecisely using English,
>occam may be defined exactly (here comp scientists start muttering the
>cabalistic incantations denotational semantics, CSP ...). This is the basis
>of the claim that modern languages such as occam, modula, (perhaps C - it
>is small enough but the pointers screw things up) are better than old
>fashioned languages such as FORTRAN, COBOL and ADA.

I disagree.  Arguments that languages such as Pascal or Modula-2 are better
than languages such as FORTRAN or COBOL are usually based upon syntax and
structure.

It is interesting to see Ada classified as an "old-fashioned" language when
it is considerably more recent than Modula or Modula-2.  It would appear that
the distinction is between language that rely upon standard libraries, and
those that do not.  While, aesthetically, such a distinction may make a
significant difference, it doesn't appear to make a whole lot of difference
in terms of developing semantics and proof rules.

It is probably more appropriate to classify occam along with FORTRAN, seeing
as how they both lack modern data abstraction and recursion, not to mention
their syntax...

Likewise, for all its faults, it is probably more appropriate to classify
Ada with Modula-2 and Pascal.


Jonathan