jwb@cepmax.ncsu.EDU (John W. Baugh Jr.) (03/23/90)
In article <19255@megaron.cs.arizona.edu>, gudeman@cs.arizona.edu (David Gudeman) writes: > In article <4869@vanuata.cs.glasgow.ac.uk> jack@cs.glasgow.ac.uk (Jack Campin) writes: > >[about C style pointers] > >Thirdly, the aliasing it enables is a semantic mess. If anyone claims > >different, let's see your denotational model of ANSI C. > > Sure, but first show me your denotational model of Ada. > > [C semantics isn't all that complex] With the recent thread on program proving, I'm wondering if anyone has given (a subset of) C an axiomatic definition, a la Hoare-style inference rules. If there's anything in the literature I'd like a pointer to it. Thanks, John Baugh