What are denotational semantics, and what are they useful for?
Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Ask questions, find answers and collaborate at work with Stack Overflow for Teams. Explore Teams
The semantics of a language can be specified either by denotational semantics or operational semantics. These are sometimes summarised as:
The latter seems straightforward, and there are obvious reasons why we would want to specify what programs in our language do when we run them ─ such a specification in some sense tells you how to implement the language.
But what does it mean to mathematically specify what a program means, as opposed to what happens when you run it? And is such a specification useful for language designers or implementors?
Suppose you want to know if some property about a program or a programming language holds. For example, you might wish to know whether a static analysis you’ve come up with provides a runtime guarantee. You could just write some tests to verify it empirically, but you can’t exhaustively test all possible cases, so this isn’t enough to say for certain there aren’t corner cases where it fails.
