Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!iuvax!purdue!haven!adm!smoke!gwyn
From: gwyn@smoke.BRL.MIL (Doug Gwyn)
Newsgroups: comp.std.c
Subject: Re: Denotational Semantics and Language Standards
Message-ID: <11580@smoke.BRL.MIL>
Date: 10 Nov 89 19:12:02 GMT
References: <11065@riks.csl.sony.co.jp> <2727@cbnewsl.ATT.COM> <1989Nov9.151708.3617@algor2.algorists.com>
Organization: Ballistic Research Lab (BRL), APG, MD.
Lines: 17

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.

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.  And it would
seem that one needs the natural-language formulation anyway in order to
write programs.