[Prev][Next][Index][Thread]
Re: Nondeterminism / formal semantics of C

To: types@cis.upenn.edu

Subject: Re: Nondeterminism / formal semantics of C

From: martinb@dcs.qmul.ac.uk

Date: Sat, 29 Dec 2001 11:25:24 +0000 (GMT)

InReplyTo: <200112290304.fBT34eT12252@saul.cis.upenn.edu>

References: <200112290304.fBT34eT12252@saul.cis.upenn.edu>

UserAgent: IMP/PHP IMAP webmail program 2.2.6
> As for whether the semantics should be _mathematical_, well, currently
> structured English ("Standardese") seems in most cases to be more useful
> than mathematics for language definitions and programming language
> standards, because it can be more easily understood by a wider audience.
this may be correct at the moment but there is an important audience which
cannot understand structured english: verification tools!
> But currently the stateoftheart in tools for making use of formal
> semantics seems to be well behind that for grammars. Until we have
> better tools, and these tools become widely used and widely accepted,
> the advantages of mathematical specifications will be limited.
this is incorrect. there is a mathematically totally rigorous, yet also
conceptually simple tool for semantic specifications: adhoc operational
semantics, SOS, labelled transition systems and the like. i cannot
think of a single example where the adhoc semantics wasn't leaner cleaner
in comparison with alternative semantic specifications, be they gametheoretic,
picalculistic or functional (lambda calculi or domains).
of course there is a problem with adhoc operational semantics and that
is that they
* don't allow (or facilitate) technology transfer. by that i mean that
because of the lack of constraints on, say, rule formats, it is usually
not possible to reuse technology such as theorem provers
or controlflow analyses (developed for one adhoc semantical framework)
in another, at least not without having to do conceptually trivial yet
nevertheless substantial reworking of proofs
* in addition and for the same reasons there isn't a widely applicable
collections of reasoning methods for adhoc semantics.
nevertheless, the benefits (in precision) of adhoc semantics over informal
methods are so substantial that the reasons for refusing to do formal
specifications of programming languages can no longer be technical, just
social.
BUT of course it would be nice if it was possible to identify a
'universal' adhoc operational semantics that was
* expressive enough to allow precise and concise modelling of all
computational phenomena, but was
* small and constrained enough so that we can finally start (and hopefully
eventually succeed) to develop nontrivial and practically useful
mathematical theories of computing (comparable to the role of differential
equations in physics)
now the good news: such a universal adhoc semantics may already exist!
it is called the (asynchronous) picalculus.
martin