Denotational semantics do while
Denotational semantics describes the meaning of a program as some mathematical object: this is the program's denotation. Typically, the denotation of a program is a function that maps states to states. Given a program , its denotation, [[ ]], is the function that takes a state as argument and maps it to the state that results from running in the state , provided that the program terminates in the state .
The syntax of our language is described by the following BNF definitions:
::= 'a | 'b | ... | 'z | 'A | 'B | ... | 'aa | ...
::= see the first hand-out for how to define numerals
::= | | - |
::= < |
true | false | not |
::= skip | := |
We first give a denotational semantics for arithmetic expressions, then for Boolean expressions, and finally for programs. Before all that, we first define what we mean by a state.
In any imperative language, assignment is the most basic form of program: the other linguistic constructs (conditionals and loops) are simply ways of organising assignments into series that are executed in a particular order. For example, think of how (according to our intuitions) the following program is evaluated:
'x := 0 ; 'f := 1 ; while 'x ZZ. This function is defined inductively as follows:
- For a number , clearly the value should just be , independent of the state: [[ ]](s) = n. (more precisely, we should distinguish between numerals and numbers: see the first hand-out).
- For a variable , the value should simply be the value in the given state: [[ ]](s) = s(x).
- When has the form e1 + e2, the value should be the sum of the values of e1 and e2: [[ e1 + e2 ]](s) = [[ e1 ]](s) + [[ e2 ]](s).
- The operations for "unary minus" and multiplication are treated similarly.
You might also like
Metadata and Semantic Research: Third International Conference, MTSR 2009, Milan, Italy, October 1-2, 2009. Proceedings (Communications in Computer and Information Science)
Charting the Topic Maps Research and Applications Landscape: First International Workshop on Topic Map Research and Applications, TMRA 2005, Leipzig, ... / Lecture Notes in Artificial Intelligence)
Leveraging the Semantics of Topic Maps: Second International Conference on Topic Maps Research and Applications, TMRA 2006, Leipzig, Germany, October ... / Lecture Notes in Artificial Intelligence)
Advances in Information Retrieval: 34th European Conference on IR Research, ECIR 2012, Barcelona, Spain, April 1-5, 2012, Proceedings (Lecture Notes ... Applications, incl. Internet/Web, and HCI)