Path: utzoo!attcan!uunet!cs.utexas.edu!mailrus!ncar!mephisto!ncsuvx!news
From: jwb@cepmax.ncsu.EDU (John W. Baugh Jr.)
Newsgroups: comp.lang.misc
Subject: C semantics (was Re: Relationship between C and C++)
Message-ID: <1990Mar22.162912.19536@ncsuvx.ncsu.edu>
Date: 22 Mar 90 16:29:12 GMT
References: <19255@megaron.cs.arizona.edu>
Sender: news@ncsuvx.ncsu.edu (USENET News System)
Reply-To: jwb@cepmax.ncsu.edu
Organization: North Carolina State University
Lines: 19

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