48
IMPLEMENTATION OF DENOTATIONAL SEMANTICS	INFORMATICA 1/91
M. MERNIK, V.ŽUMER Technical Faculty of Maribor
Keywords: formal methods, semantics, rapid prototyping,	University of Maribor
functional languages	Smetanova 17,62000 MARIBOR
ABSTRACT : In the paper formal methods for semantics definition and reasons for their appearance are briefly described. Denotatlonal approach to semantics definition Is more detail explained in next chapter. Implementation of denotatlonal semantics lead us to operational approach and to rapid prototyped interpreters. We represent one of the possible implementation of denotatlonal semantics using functional language LISP.
KEYWORDS : formal methods, semantics, rapid j languages
1. INTRODUCTION
A programming language is a notation for describing computations and Is defined with syntax, semantics and pragmatics. The structure of statements is given by syntax. The area of syntax has been intensively studied and Backus -Naur form ( BNF ) Is widely used for defining syntax, because there exists a close correspondence between the BNF definition and parser. The meaning of statements is given by semantics and language Implementation on specific computer is described by pragmatics. In this paper we briefly describe semantics definition methods. Unfortunately, the semantic area is not as well developed as the syntax area, because semantic features are much more difficult to define and describe. Semantics of early developed programmmlng languages were described In natural languages. This description has the advantage that semantics was easily understood but also many disadvantages such as: ambiguity, inaccuracy, misunderstanding, etc. So we need formal semantics definitions which, ensures us :-precise standards for a computer Implementation, which guarantes that the language Implementation is exactly the same on all machines ;
-	usefull user documentation ;
-	a tool for design and analysis ;
Input to compiler generator, which maps
., functional
semantic definitions to a guaranted correct implementation of the language.
The effort, on formal methods for semantics definition,. done In 70-ties have brought us three distinct and complementary description methods : operational, denotatlonal and axiomatic semantics [3,4,6,8].
The operational semantics method uses an Interpreter to define a language. The meaning of a program is the evaluation history that the interpreter produces when It Interprets the program.
The denotatlonal approach to semantics makes use of mappings, which are called semantlo valuation functions. These map syntax constructs into their abstract mathematical counter part ; thus numerals are mapped Into numbers, procedures are mapped Into mathematical functions, and so on. The denotatlonal definitions are more abstract then operational.
With the axiomatic semantics method, the meaning of program Is not explicitly given at all. Instead, properties about language constructs are defined. These properties are expressed with axioms and inference rules. Axiomatic definitions are more i abstract then denotatlonal and operational.
All three methods together provide a set of
tools for language development. Designers might first define properties that they wish the system
49
to have, so axiomatic definition Is constructed first. Next, a denotatlonal semantics Is defined to give the meaning of the language. Finally, the denotational definition is implemented using an operational definition. These complementary semantic definitions of a language support systematic	design,	development	and
implementation. In thé paper ue describe denotational approach and one of its possible Implementation using functional programming language LISP.
2. DENOTATIONAL SEMANTICS
Denotational semantics (1,2,3) Is a methodology for giving mathematical meaning to programming languages. To make things more understandable an example of denotational semantics for a simple language of binary numbers is given first. Its syntax is defined with :
v : : = i> S | S S ::= 0 I 1
The language of binary numbers is composed by sequence of digits 0 and 1. To define the meaning of statement a valuation semantic function V which maps sequence of digits into their meaning is constructed. We say that the domain of V Is a sequence of digits and the codomaln are Integers which represents meanings of digits. Mathematical notation for the function V Is :
V : Bin -> Integer
We must define an instruction, which maps the domain into the codomaln for each BNF rule :
V[0] = 0
Vtl] = 1
v[i>s] = 2 • vit/] ♦ via]
The next example, shows the semantic valuation function V on work :
V11001] = 2 * VI100J + V[l]
= 2 • 2 • V[10)V[0] + 1 = 2 • 2 • 2 • Vtl] + V[0] * 0 * 1 = 2*2*2*1*0*0*1 = 9
Therefore the denotational approach to languages définition must make clear several sets of quantities :
- the syntax rules,
-	the definition of the various semantic functions,
-	the syntax domains,
-	the semantic domains.
For describing syntax 'rules the abstract syntax is used. It specifies the relations between logical parts of the language and can be simpler than concrete syntax, and may not contain enough Information to parse the language unambiguously. On contrary, concrete syntax contains sufficient information to parse a language.
A-notations is used for describing semantic functions. To show the advantage of a A-notatlon following definitions must be stated first. Function f(x) = y Is equlvalently described in A-notation with f = Ax.y . In this notation all functions usually have only one argument or one parameter. Consider a function f with two variables x and y. A function g with the property g(x)ty) = f(x,y) can be defined and Is in some sense equivalent to f. The-function g Is called the curried version of f. Function which produced another function on its output is called the high order function. A-notatlon has following advantages :
-	a high order function is easier to describe ;
example :
add : N -> N -> H standard notation :
add(n) = f , where f(m) = n+m A-notatlon :
add = An. Am. n+m
-	a function can be defined without giving It a name. Such function Is called the anonymous function.
Several additional notations may be used in expressions of semantic equations, such as "update" expressions of the form (a h-» b]f, which denotes a function f which is the same as the function f except, that it maps the argument a into the value b. Conditional expressions are written In the form "t -> et □ e " where the value of the expression e) is evaluated If and only If the boolean expression t is true and the
value e is evaluated otherwise.
2
Syntax domains of imperative languages are usually identifiers, expression, commands and definitions. Semantic domains are most conventionally described with an environment and a store. The environment is a finite set of associations of identifiers with values they denote ( denotable values ) and the store is a
50
finite set of locations with values they contain ( storable values ). The store will be sufficient for simple languages where equal identifier can not be used for different objects.
And now, let us define the meaning of identifiers. Identifiers may stands for location, label, procedure and theirs meaning are represent by semantic domain environment which Is a function from identifiers to denotable values. If identifier stands for location , a second semantic domain is used to get value they contain. The store is therefore a function from locations to storable values.
The meaning of commands is to change the store, the meaning of a definition is to change the environment and the meaning of an expression is to produce a value (expressible value).
3. IMPLEMENTING DENOTATION*!. SEMANTICS USING LISP
A great advantage of the denotatlonal approach Is that can be mechanized and Interpreted on a computer [1,2,7], In this chapter a snail and a simple example is described with the denotatlonal semantics first and then Implemented using functional language LISP. LISP Is selected because high order functions are relatively simple to express using It.
The abstract syntax for a simple Imperative language Is given first :
P e Program B € Block D e Declaration C € Command E e Expression I 6 Identifier N s Numeral
P :: = B.
B ::= begin D & C end
D : : = D & D I var I 1 2
C : C & C2 I I:«E I
If E then C^ else C2 I B
E : : = E + E I I I N l 2
Program is a block of statements and each block consists of a declaration part and a command part. Commands are : assignment statement, if statement and block of statements. Expressions are : identifiers, numerals and composed expressions. Delimiter symbol between statements is a character 8..
Semantics are described as follows : Domains and operations on it are :
I.	Natural numbers n 6 N
II.	Identifiers	1 € Id
III.	Location	1 e Loc
reserve_loc : Loc reserve_loc » random 1000
IV.	Denotable values d e D_values « Loc
V.	Environment e 6 Env = Id -> D_values
emptyenv : Env emptyenv » A1.0
accessenv : Id -> Env -> D_values accessenv = Al.Ae.e(l) updateenv : Id -> Value -> Env -> Env updateenv = Ai.Ad.Ae. [1 h» vie
VI.	Storable values v e S_value = N
VII.	Store s 6 Store = Loc -> S_value
emptystore : Store
emptystore = XI.0
access : Loc -> Store -> S_value
access = Al. As. st 1)
update : Loc -> S_value ->
Store -> Store update = Al.Av.As. [1 v|s
VIII.	Expressible values x e Exp_vaules = N
Semantic valuation functions Is given next : P: Program -> Store P[B] = BIB] emptyenv emptystore
The meaning of a program Is defined with a store, which is the output ftom function B. The function B needs environment and store on the Input. The function B is applied on initialized environment and store first.
B: Block -> Env -> Store -> Store BCbegln D & C end] = Xe.As.CIC] (DID] e) s
The meaning of a block is the meaning of commands, which Is evaluated on environment and store. The environment Is changed by function D first.
D: Declarations -> Env -> Env
D[D] & D2J = Ae.D(D2] (DlD^l e)
Dlvar I] ■ Ae. updateenv II] reserve_loc e
The meaning of a declaration is to change the environment. When an identifier declaration is evaluated, new location is produced first and then new updated environment is returned. This updated environment has a property that it maps an Identifier to a new location.
51
C: Command -> Env -> Store -> Store
CIB] = Ae.As. BIB] e s
C[C & C ] = Ae.As.ClC ] e (CIC ] e s) 12 2 1
C11:=E] = Ae.As.update (accessenv (I] e)
(ElE) e s) s CI if E then Cj else C2) = Ae.As.EIEls = 0 ->
CIC ]e s o
1
CIC )e s
2
The meaning of a command is to change the store. The meaning of an if statement is to evaluate the expression E first and then appropriate command is selected and evaluated. The meaning of an assignment statement Is :
-	a location for an Identifier is evaluated ( accessenv [I] e ) ,
-	an expression E is evaluated ( EIE] e s ) ,
-	a location is updated with value produced by the function E
(update (accessenv II] e) (E[E]e s). s) .
E: Expression -> Env -> Store -> Exp_value E[E +E ] = Ae.As.ElE^e s + EIE^e s EI I] = Xe.As.access (accessenv II] e) s EIN] = N[N]
The meaning of an expression is to produce a new value. Semantic valuation function N Is similar to function V , which is Introduced In chapter 2.
Now, we can apply syntax semantic valuation
j
functions to syntax construct to gel their meaning.
Example :
Plbegln var 1; i:=10; begin var 1; 1:=20 end;
1:=1+1 end] = Blbegln var 1; 1:=10; begin var 1; i:=20 end;
1:=1+1 end] emptyenv emptystore = CI 1: =10; begin var i; i:=20 end; i:=i+l]
(Dlvar ilemptyenv) emptystore = CI 1: =10; begin var 1; 1:=20 end; i:=i + l] (updateenv (1] reserve_loc emptyenv) emptystore = CI 1: =10;. begin var i; 1:=20 end; i:=i+l]
[1 i- Ilemptyenv emptystore = C[begin var 1; i:=20 end; l:=i + l]
Hi- Ilemptyenv tCt i: =101 II ► Ilemptyenv emptystore) = Clbegln var 1; i:=20 end; 1: =1+11
[in Ilemptyenv (update (accessenv [1] [i i- 1] emptyenv) (El 10] [in Ilemptyenv emptystore) emptystore) = Clbegin var 1; 1:=20 end; i:=i+l] [ih Ilemptyenv (update 1 10 emptystore) =
Clbegin var i; 1:=20 end; 1:=1+11 Ilh Ilemptyenv
11 i- lOlemptystore =
let e = I 1* Ilemptyenv
let s = (1 ^ lOlemptystore
Ct1:=1+11 et (Clbegin var 1; l:=20 end) e4 st ) =
CI 1:=1+1] ef (Blbegln var 1; i:=20 end] et st ) =
CI1: =i + l ] (CI 1: =20] (D Ivar i] e^ s^ =
C[i:=1 + 1J et (CI 1; =20]
(updateenv ll] reserve_loc e) st ) =
Cli: =i+l ] et (Cll: =20] [1 i- 2^ Sf ) =
Cli:=1+1] et (update (accessenv 11] (1 h 2^)
(E(20] s^ Sj ) =
Cli:=1+11 ej (update 2 20 sj ) =
Cli: =1 + 11 12 i- 20]si =
let e = I Ik 2]emptyenv 2
let s2= U f- 10, 2 h 201emptystore update ( accessenv (1] e] ) (Etl+1] ej s^ s2 » update 1 ((acess (accessenv II] e( )s2) + 1) s2 = update 1 (access 1 S2)+l S2 = update 1 10+1 s^ = update 1 11 is = 11 h 11, 2 k 20)emptystore
The meaning of the above program is the store, which map location 1 to value 11 and location 2 to value 20.
Implementation of semantic valuation functions is shown In appendix . Now, we can analyze any semantic valuation function.
Examples :
(setq new_env (funcall (D '(var i & var J & var k)) emptyenv))
=> ( is evaluated to ) ( (1 599) (J 41) (k 855) )
Function D changed the environment. The new environment maps Identifier 1 to location 599, Identifier J to location 41 and identifier k to location 855.
(funcall (funcall (C 1( ( 1	: = (1)) &
( J	:= (2)) &
( k	:= ((1) + (J)))
)
) new_env	) emptystore) => ( Is evaluated to )
( (599 1) (41 2) (855 3)	)
52
Function C changed the store. The new store maps location 599 to value 1, location 41 to value 2 and location 855 to value 3.
(setq prog '(begin (var 1 & var j & var k) & ( (1 := (1)) & (j :« ((1) + (1))) & ( begin (var 1 & var 1 & var in) 8.
( (1 (m (1 )
end ) & (k := ((I) + (2))
= (20)) & » ((1) ♦ (1))) & = ((J) ♦ (1)))
)
end ))
( P prog )
=> ( is evaluated to )
( (599 1) (41 2) (784 20) (503 21) (981 3) (855 3) )
We can understand the store only with the environment. The environment for that example Is :
((i 599) (J 41)(k 855)(1 7841(1 981)(m 503))
3.	Tennent R.D., "Principles of Programming Languages", Prentice Hall International, London. 1981.
4.	Horowitz E.. "Fundamentals of Programming Languages". Computer science press. Rockville, 1983.
5.	Agrestl W.W.."New paradigms for software development",IEEE Computer society press. New York, 1986.
6.	Mernik M., Kokol P., 2umer V.,"Formalne metode za opis semantlke programskega Jezika". XIV. Slmpozljum o Anformaclonim tehnologijama, Sarajevo - Jahorlna 1990, pp. 181-1 - 181-.10.
7.	Mernik M., Kokol P., Žumer V., "TI-B0SS: A new rapid prototyping paradigm for language design", Proceedings of International Conference on Computing and Information, Niagara Falls, pp. 504 - 507, 1990.
8.	Marcotty M. , Ledgard H.F. , Bochmann C. V. , "A Sampler of Formal Definitions", Computing Surveys. Vol. S.. No. 2., 1976.
APPENDIX : SEMANTIC VALUATION FUNCTIONS IN LISP
Env = Id -> D_value
Environment is modeled with association list
( (id loc ) ... (Id loc ) )
11	n n
4. CONCLUSION
The implementation of semantic valuation functions has many advantages [1,2,5,71 :
-	each semantic valuation function can be separately tested and analyzed,
a rapid prototyped Interpreter for the language is produced
-	all advantages of prototyped systems such as :
-	greater user participation.
-	early detection of errors,
-	better user - developer commui ications,
-	early delivered executable systems to the users,
-	help by suppressing uncertainties In user requirements (I'll know what I want,
when I see it ! ).
;; accessenv: Id -> Env -> D_values (defun accessenv ()
tt' (lambda (1) «'(lambda (e) (cadr (assoc i e)))
i; updateenv: Id -> D_value -> Env -> Env (defun updateenv () r (lambda (i) U" (lambda(d) It'(lambda (e) (putassoc e 1 d)))))
Store = Loc -> S_value Store Is modeled with association list ( (loc value ) ... Hoc value ) )
11	n	n
;; access : Loc -> Store -> S_value (defun access () »'(lambda (1) «'(lambda (s) (assocl 1 s))))
S. REFERENCES
1.	Schmidt D.A., "Denotatlonal semantics". Allyn and Bacon. Neuton. 1986.
2.	Allison L., "A practical introduction to denotatlonal semantics", Cambridge university press, Melbourne, 1986.
;; update : Loc -> S_value -> Store -> Store ( defun update () 11'(lambda (1) It'(lambda (v) It'(lambda (s) (putassoc s 1 v)))))
;; reserve_loc Is modeled with random numbers (defun reserve_loc () ( random 1000 ))
;; environment Initialization (defun emptyenv () nil )
;; store Initialization . [defun emptystore () nil )
;; P: Program -> Store ( defun P (Program)
(funcall (funcall (B Program) (emptyenv)) (emptystore)))
;; B: Block -> Env -> Store -> Store ( defun B (Block) r ( lambda ( e ) «' (lambda ( s ) (funcall (funcall (C (cadddr Block)) (funcall (D (cadr Block)) e)) s))))
; ; D: Dec -> Env -> Env (defun D (Dec) #'(lambda (e)
(cond ((equal (caddr Dec) '&) ;; composed declaration (funcall (D (cdddr Dec)) (funcall' (D (list (car Dec) (cadr Dec))) e))) ;; identifier declaration (t (funcall (funcall (funcall (updateenv) (cadr Dec)) (reserve_loff)) e ))))) ;; C: Comra .-> Env -> Store -> Store (defun C (Comm) #•(lambda (e) (lambda (s) (cond ((not (equal (cdr Comm) nil)) ;; composed commands (funcal1 (funcall (C (cddr Comm)) e) (funcall (funcall (C (list (car Comm))) e) s))) ;; if statements '((equal (caar Comm) 'IF)
(cond ((equal (funcall (funcall ,	(E (cadar Comm)) e) s) 0)
(funcall (funcall (C (list
(cadddr (car Comm))))-e) s)) (t (funcall (funcall (C (list
(cadddddr (car Comm)))) e) s)))) ;; block statements ((equal (caar Comm) 'BEGIN)
(funcall (funcall (B (car Comm)) e) s)) ; ; assignment statement (t (funcall (funcall (funcall. (update) (funcall (funcall (accessenv) (caar Comm)) e)) (funcall (funcall (E
(caddar Comm)) e ) s)) s)) ) I))
; ; E: Exp -> Env -> Store -> Exp_value (defun E (Exp) «'(lambda (e) «'(lambda (s) ;; number
(cond ((numberp (car Exp)) (car Exp))
:; Exp * Exp
((equal (cadr Exp) +)
(+ (funcall (funcall (E (car Exp)) e) s) (funcall (funcall (E (caddr Exp)) e) s))) ;; Identifier
(t (funcall (funcall (access)
(funcall (funcall (accessenv ) (car Exp)) e)) s))))))