Denotational Semantics and Language Standards

[Jeffrey Kegler]

DG> Article <11571 at smoke.BRL.MIL> gwyn at brl.arpa (Doug Gwyn)
JK> Article <1989Nov8.225008.793 at algor2.algorists.com>
    jeffrey at algor2.ALGORISTS.COM (Jeffrey Kegler)

JK> ...  A brave new world, where any question about dpANS could be stated
JK> as a theorem and proved or disproved ... would seem a vast improvement.

DG> An additional drawback that you failed to mention in your article is
DG> that C is deliberately "fuzzy" in many areas, to permit efficient
DG> implementation on a variety of architectures.  This makes it rather
DG> unsuitable to theorem proving, since useful theorems would have to be
DG> about C's behavior on entire classes of architectures.

I failed to mention it because I think denotational semantics deals
much better with "fuzziness" (if I understand what you mean by fuzzy)
than English.  I assume you mean the same as Scott Daniels
(daniels at cse.ogc.edu) who (in Email to me) give the order of
evaluation of function arguments as an example of such.

[ Aside: there is such a thing as fuzzy logic, which I assume Doug
knows about, and I assume that is not what he means, hence his use of
quote marks. ]

By "fuzz", I believe we mean indeterminacy.  [ Note that
implementation specific behavior is included in this concept of
indeterminacy. ] Even though the physical machine on which C runs will
probably be determinate (dpANS does not require it to be), the virtual
machine dpANS describes is not determinate.  Of course, all sorts of
results can be proved about indeterminate machines.

[ Definitions: "determinacy" means that give one state of an abstract
machine, we can uniquely determine the succeeding one.  Indeterminacy
means a given state of the virtual machine could result in any of one
or more succeeding states. ]

Take as an simple example of "fuzz":

r = rand();
r = r * r;

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).

For example, the result of

int f(int a, int b) { return a+b; }
...
i = 2; i = f(i = 3, i);

is indeterminate.  Variable i can be either 5 or 6, after this
(untested and unrecommended) code fragment.
-- 

Jeffrey Kegler, Independent UNIX Consultant, Algorists, Inc.
jeffrey at algor2.ALGORISTS.COM or uunet!algor2!jeffrey
1762 Wainwright DR, Reston VA 22090