Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!tut.cis.ohio-state.edu!quanta.eng.ohio-state.edu!raksha.eng.ohio-state.edu!rob
From: rob@raksha.eng.ohio-state.edu (Rob Carriere)
Newsgroups: comp.std.c
Subject: Re: Denotational Semantics and Language Standards
Message-ID: <3508@quanta.eng.ohio-state.edu>
Date: 14 Nov 89 02:38:57 GMT
References: <11065@riks.csl.sony.co.jp> <2727@cbnewsl.ATT.COM> <1989Nov9.151708.3617@algor2.algorists.com> <11580@smoke.BRL.MIL>
Sender: news@quanta.eng.ohio-state.edu
Reply-To: rob@raksha.eng.ohio-state.edu (Rob Carriere)
Organization: Ohio State Univ, College of Engineering
Lines: 43

In article <11580@smoke.BRL.MIL> gwyn@smoke.BRL.MIL (Doug Gwyn) writes:
>In article <1989Nov9.151708.3617@algor2.algorists.com>, jeffrey@algor2.algorists.com (Jeffrey Kegler) writes:
>> I cannot say what r is after these two statements, but I can prove
>> theorems about it nonetheless.  The theorem "r is greater than zero,
>> or r has overflowed or a signal has been handled or the implementation
>> is not hosted" for example, can be shown to be true (if I remembered
>> all the appropriate conditions).
>
>Oh, I agree that theorems like that could be proved, but what would be
>the point?  You can already tell that much without a formal denotational
>semantics specification for C.

Hmmm....  You would sure hope so, or there's a bad problem with the Standard.
However, that seems to me a lot like the argument that we should all program
in assembly, 'cause it is Turing-complete.  The argument started with the
assertion that it would be _easier_ to show those things in a formal semantic
system.  I am not sure whether that is true, especially for denotational
semantics (I am still impressed by a calculation of the meaning of "if B then
goto L;" which took a full page of densely written math!), but it seems to me
whether or not one can with sufficient effort do something with the existing
methods is beside the point.

>Areas where formal semantics MIGHT be useful would include the effect of
>preprocessing, determining type compatibility, and applying conversion
>rules.  I'm not sure it would be easier to work those out using formal
>symbolism instead of the technical English rules, however.  

Possibly not.  However, there are very few people who agree completely just
what the rules of technical English are.  Also, having to express the intent
in a formalism where one cannot accidentely skip some details might make the
process of writing a standard more accurate.  I have at least personally found
that having to mathematize (sorry :-) my ideas is one good way to discover
what I don't quite understand yet.

>And it would
>seem that one needs the natural-language formulation anyway in order to
>write programs.

Very probably true.  However, a compiler writer with training in formal
semantics might well bless the standards commitee that comes out with a formal
definition (maybe she'd even send them flowers :-)

SR