A111D7 3TDDTD

PUBLICATIONS

NBSIR 83-2740

Specification and Interpretation of

Data Model Semantics: An

Integration of Two Approaches

US. DEPARTMENT OF COMMERCE

National Bureau of Standards

Center for Programming Science and Technology

Institute for Computer Sciences and Technology

Washington, DC 20234

July 1983

-QC

100

.1156

33-2740

1983

C , 2

S. DEPARTMENT OF COMMERCE

kTIONAL BUREAU OF STANDARDS

NBSIR 83-2740

SPECIFICATION AND INTERPRETATION OF

DATA MODEL SEMANTICS: AN

INTEGRATION OF TWO APPROACHES

AUb 8 1983

rsCrV G-CjO- cUfC

o~o ^ oC>

vU

^3- 3740

Winfried Lamersdorf

U S. DEPARTMENT OF COMMERCE

National Bureau of Standards

Center for Programming Science and Technology

Institute for Computer Sciences and Technology

Washington, DC 20234

July 1983

U.S. DEPARTMENT OF COMMERCE, Malcolm Baldrige, Secretary

NATIONAL BUREAU OF STANDARDS. Ernest Ambler. Director

SPECIFICATION AND INTERPRETATION OF DATA MODEL SEMANTICS :

AN INTEGRATION OF TWO APPROACHES

Winfried Lamersdorf

Universitflt Hamburg

Fachbereich Informatik

SchlOterstrasse 70

D-2000 Hamburg 13

West-Germany

November 1982

This work was done, in part, while in residence at the

Data Management and Programming Languages Division,

Center for Programming Science and Technology,

Institute for Computer Sciences and Technology,

National Bureau of Standards,

Washington, D.C. 20234
.
TABLE OF CONTENTS

Page

1. INTRODUCTION 1

2. TWO APPROACHES TO DATA MODEL SEMANTICS SPECIFICATION .. 4

2.1 CONCEPTS OF A SEMANTIC SPECIFICATION METHOD 4

2.2 THE VIENNA DEVELOPMENT METHOD 5

2.2.1 Structural Tools 6

2.2.2 Operational Tools 6

2.2.3 Constraint Mechanisms 7

2.3 THE POSITIONAL SET NOTATION 7

2.3.1 Structural Tools 8

2.3.2 Operational Tools 8

2.3.3 Constraint Mechanisms 9

2.4 AN EXAMPLE 9

2.4.1 The VDM Specification 9

2.4.2 The PSN Specification 13

2.5 COMPARISON OF THE TWO SPECIFICATION METHODS 15

3. FORMAL SEMANTICS OF THE DATA MODEL PROCESSOR 18

3.1 INTRODUCTION TO THE FORMAL MODEL 18

3.2 STRUCTURE SPECIFICATION 19

3.2.1 Abstract Syntax 19

-i i i-
3.2.2 The Global State 20

3.2.3 Structural Constraints 20

3.2.4 Auxiliary Functions 21 3.3

OPERATION SPECIFICATION 24

3.3.1 Abstract Syntax 24

3.3.2 Operational Constraints 26

3.3.3 Operation Semantics 28

3.3.4 Auxiliary Functions 31

4. INTERPRETING DATA MODEL SPECIFICATIONS 34

4.1 OVERVIEW 34

4.2 INTERPRETING A VDM MODEL ON THE DMP 34

4.2.1 Structure Specification 34

4.2.2 Operation Specification 36

4.3 INTERPRETATIONS FOR THE META DATA STRUCTURES 38

4.3.1 Elementary Data Types 38

4.3.2 Composite Data Types 39

4.4 USE OF THE INTERPRETABLE SPECIFICATIONS 46

4.4.1 Specifying an Object System's Semantics 46

4.4.2 Analyzing the Interpretable Specifications .. 47

5. CONCLUSIONS 49

6. REFERENCES 51

-iv-
SPECIFICATION AND INTERPRETATION OF DATA MODEL SEMANTICS :

AN INTEGRATION OF TWO APPROACHES

Winfried Lamersdorf

Two different approaches to database model semantics

description and evaluation are presented, compared, and

integrated: a formal semantic specification method as

originally developed for programming languages, and a computer-based data model interpreter to be used as a rapid

prototyping system. Both ways to specify database model

semantics are applied to a common example.

Two alternatives to combine the advantages of both

methods are analyzed in detail: First, it is shown how the

semantics of the data model processor can be precisely

described in terms of the formal semantic specification

method. Then, it is demonstrated how the abstract metalanguage of the specification method can be mapped to the

executable commands of the data model processor. Thus,

database semantics can both be specified in an abstract and

high-level way and still be analyzed and evaluated

automatically.

Key words: databases; data models; data model processing;

data model prototyping; data model semantics; denotational

semantics; formal semantic specification; relational

database; relational data model; semantic model interpreter.

1. INTRODUCTION

De sig

appl ica t io

af f e cts no

appl ica tio

of a ppr opr

mode 1 s

ning the software tools for major d

ns has become an increasingly complex task

t only the development of special purpose d n programs, but also the design and specif

iate query languages as well as adequate, n

atabase

. This

atabase

icat ion

ew data

- 1 -
To assist in the process of designing, specifying, and

evaluating the semantics of data models and software

components, new tools have been developed recently. Two

major directions can be separated: first, formal methods for

the precise specification of programming language semantics

have been successfully applied to the design and

specification of, e.g., a database query language [7], and a major data model [9]. On the other hand, methods derived

from recent developments of 'rapid prototyping' systems can

be applied to design problems in the database area as well.

The design and evaluation of new systems (or models) can be

guided automatically at a very early stage of their

development

.

This paper, in essence, introduces, compares, and tries

to integrate two such methods for database software

development, analysis, and evaluation: The 'Vienna

Development Method' (VDM) [1] as a more theoretically

oriented semantic specification technique, and the

'Positional Set Notation' (PSN) [3] as the 'meta-language'

for an automatic data model specification interpreter, the

'Data Model Processor' (DMP) [4]. The paper is divided into

three major parts (chapters)

The second chapter introduces the basic semantic

specification tools of both methods. It compares both metalanguages by applying them to a common object system, a subset of the relational data model (RDM) as specified in

[9] and [5]. The basic result is that both methods have

different objectives, and, thus, different advantages:

PSN is oriented towards automatically interpretable

specifications, VDM, on the other hand, provides the more

complete and comprehensive specification meta-language.

The following chapters explore two approaches to

combining the advantages of both methods:

In chapter 3, VDM is applied to specify the semantics

of PSN in a completely formal way. The resulting formal

model provides PSN and the specification language of the DMP

with a concise and precise description of both their

structures and operations. Based on this specification, a very detailed insight into the semantics of the metalanguage can be obtained, an essential pre-condition for the

use of the describing (meta-) language tools of any semantic

specification method.

Chapter 4 describes the alternative approach of using

the DMP directly as an interpreter for a subset of the

formal semantic specification tools of VDM. The intended

- 2 -
goal is to combine the advantages of a high-level, abstract

semantic specification meta-language with the ease of

analyzing its specifications by automatic means. It is shown

in detail, to what extent PSN and the DMP commands can

provide a machine executable interpreter for a substantial

subset of VDM . Such an interpreter for high-level semantic

models is especially well suited for simulating semantic

specifications in the database area.

- 3 -
2 . TWO APPROACHES TO DATA MODEL SEMANTICS SPECIFICATION

2.1. CONCEPTS OF A SEMANTIC SPECIFICATION METHOD

A semantic specification method provides the tools

to describe the semantics of a given 'object system'. The

set of all tools is called the 'meta-' or 'specification'

language, the resulting description a 'semantic model' or a 'meta system'. Compared to the object system to be

described, the meta system is expected to be considerably

clearer, easier to understand, more concise, precise, and

less ambiguous. This leads to certain requirements for the

meta language. The appropriate choice of its tools and

language constructs is the most important prerequisite for

any specification technique. The set of tools provided

should be, on one hand, as formal, concise and theoretically

well based as necessary, and, on the other hand, as well

understood and understandable for the intended user as

possible. Experiences with natural language descriptions

seem to indicate that formal ways of expressing semantics

are more appropriate for that purpose than informal. (Formal

specifications of complex systems, however, tend to be

difficult to understand for untrained users.)

In any case, the meta-language tools should reflect the

most important parts of the object system in a suitable way.

Considering a data model as the system to be described, its

main components can be characterized as

- a set of obj ects which may have a complex inner

structure and different subcomponent relationships,

- a set of operations which are applicable to these

kinds of objects, and (possibly)

- a collection of restrictive ('consistency' or

'integrity') constraints and conditions which have to

be fulfilled by all 'well formed' objects and for all

operations 'well applied' to their respective

operands

.

So, an appropriate meta language has to provide at

1 east

- a mechanism to specify the structural aspects of an

object system with respect to both its subcomponents

as well as its subcomponent relationships.

- a mechanism to express the semantics of the

operational aspects of an object system with respect

to both their abstract syntax (operation name.

- 4 -
parameter types) as well as their semantic meaning,

and

- ways to specify constraints which may apply to both

the structural and the operation aspects of the

object system.

well

In addition,

defined set

the meta language should be based on a of primitives whose semantics can be

derived from well known (preferably

These primitives should be expressive

object system in an adequate way

should be 'comprehensible' enough

automatic use (or even both)

mathematical) objects,

enough to reflect the

and the semantic model

for either human or

2.2. THE VIENNA DEVELOPMENT METHOD

The 'Vienna Development Method' (VDM) [1] is a specification method based on the denotational

Besides several applications to programming

semantics, it has been successfully applied to

specifications in various database areas, rangi

specific database language [7], to a complete

system [8], and a major data model [9].

semantic

approach

language

semantic

ng from a database

VDM's corresponding meta-language, 'Meta IV', uses

high-level, abstract, mathematical objects to 'denote' the

semantic properties of an object system to be specified. An

important aspect of the abstract 'meta' objects of Meta IV

is that they express only a logical view of the structures,

operations, and constraints of the object system without any

impl ementational details. At the same time, they do not hide

important structural aspects of the described system as some

other semantic specification methods do. This makes a method

like VDM especially well suited for specifications in the

database area. Meta IV provides a very rich set of abstract

modeling tools both for the specification of structures and

operations as well as for constraints which may be imposed

on them. The syntax of the meta-language tools was designed

with special consideration to ease of understanding by users

who are familiar with the (concrete) syntax of a common

high-level programming language.

- 5 -
2.2.1

STRUCTURAL TOOLS

2. 2. 1.1 Elementary Objects

Meta IV provides (in principle) an unlimited set of

elementary data types for the definition of semantic

objects. These data types are well known from the usual

programming languages: Boolean (value set BOOL), Integer and

Real (also comprised of Numeral, value set NUM) , and

Quotation (for indivisible character strings, value set

QUOT) . The set TOKEN contains all those elementary objects

whose inner structure is not considered any further in the

fo rmal model

.

2. 2. 1.2 Structuring Mechanism

Additionally, the meta language provides a standard set

of composite, higher-level abstract data types to describe

the structural aspects of an object system. These types

include

- simple sets of elementary or higher-order elements,

- ordered tupl es or lists of elementary or higher-order

elements

,

- labeled or unlabeled trees of elementary or higherorder objects,

- finite maps between (finite) sets of abstract

objects, and

- total, partial, or bijectional functions between any

abstract sets within the model.

Using these data types in an abstract VDM model, more

complex meta-language structures are composed out of named,

simpler ones in an (in general recursive) BNF-like style.

2.2.2

OPERATIONAL TOOLS

As VDM is based on the ' denota t ional ' approach of

formal semantics, the meaning of each object system's

operation is defined in terms of a 'semantic meaning

function' which represents the abstract 'denotation' of that

particular operation. These so called 'elaboration

functions' describe the meaning of each operation by

specifying its effects on the semantic objects as given in

the structural part of the formal model. In pure

denotational semantics, the semantic meaning functions are

- 6 -
represented by Lambda expressions. To improve the

readability of the specifications, however, Meta IV provides

alternative, but semantically equivalent means of writing

certain classes of Lambda expr<

notations are chosen to be similar to

of modern high-level programming

constant and variable declaratioi

conditional and iterative control s

1

In addition, the usual operal

abstract data structures may be

2.2.3 CONSTRAINT MECHANISMS

For abstract objects as well

operations, certain 'consistency

formulated by use of the ' is-well-f

functions) of the meta language Meta

- 'static' consistency constra

classes of abstract objects to

ones, and

- 'dynamic' consistency

abstract operations to

i.e. to those which

operands only.

only

are

lions

.

The al ternati ve

' well known construe ts

languages

they include

i, (meta) statements

,

ucture s, etc.

ons of the higher-level

used in the function

tive meanings are well

st-ord er predicates.

as for the abstract

constr aints ' may be

ormedpred icates (i.e.

IV:

ints

,

to restrict the

only the well formed

aints

,

to restrict the

ie wel 1 applied ones,

ippl ied to well formed

2.3. THE POSITIONAL SET NOTATION

[3] provides a objects. PSN

way to define

The 'Positional Set Notation' (PSN)

powerful notation for specifying data modeling

uses 'positional sets' (p-sets) as a unified

various aspects of data model structures formally.

Furthermore, there exist a software system, the 'Positional

Set Processor' (PSP) [4] which consists of about 40 powerful

commands to define and manipulate PSN structures (i.e. psets) . Thus, the specification language of the 'data model

processor' (DMP) [5], i.e. PSN combined with the PSP

commands, can be used as a well defined method to express

data model semantics formally. The DMP provides an

executable ' meta ' -language which is based on p-sets, PSP

commands, and some additional C-code extensions to specify

behavioural properties which cannot be expressed completely

by PSP operations. The main advantage of the formal semantic

- 7 -
specification tools is their ability to be executed

automatically on the DMP. Compared to VDM, however, the

specification meta-language is somewhat more restricted,

less abstract, and more difficult to understand and to use

for an inexperienced user.

2.3.1 STRUCTURAL TOOLS

2. 3. 1.1 Elementary Objects

The basic elements of PSN are called 'atoms'. In this

context, an atom is either a number (real or integer), a string, or 'null', as denoted by the special character '#'.

Some character strings (namely 'indexes' or 'position

identifiers') are constrained to begin with an alphabetic

character

.

2. 3. 1.2 Structuring Mechanism

In PSN, the basic mechanism to specify str uc tur es is

the 'pos i tional set

(p-set) . P-sets are ( indexed) set s of

o rdered pairs in wh ich the first element of each pair is an

atom or a po s i t ional set, the second, cal led the ' index ' or

' posit io n iden ti f ie r', a (restricted - see above) char ac ter

string , a numbe r , or the special charac ter '#'. So , the

essence of PSN i s th e recursive definitio n of a p- set

s = [ x_i @ p_ i . . . ] where the x i (e lements) are e i ther

atoms or p-sets , and the p i (posTtion identi

f

iers) are

e i ther atoms or the special characte r '#' - the null

position ident if ier which denotes the index for each

' classic al ' set e lement. A pair x i @p i is called a 'duplex', i.e. each p-set consists of a (unordered) set of

duplexes. It is demonstrated in [6] that p-sets are powerful

enough to describe all structural properties of the main

database models.

2.3.2 OPERATIONAL TOOLS

In PSN, the mechanism to specify operations is based on

a set of 'primitive' or standard operations. They can be

executed on a software system called the 'Positional Set

Processor' (PSP) [4]. These ' PSP-commands ' include the

classical set operations, special operations to create,

delete, and modify p-sets, so called 'sequence' operations,

and auxiliary 'utility' operations. (See [4] for details.)

Whenever there is no such (in general complex) application

of PSP-commands to express the semantics of a data model

operation completely, further semantic descriptions are

- 8 -
added by use of 'concrete', plain C code. So all the

semantics of an object systems operation is specified in

terms of PSP operations, usually imbedded in some additional

C code, i.e. all specifications are machine executable on

the DMP.

2.3.3 CONSTRAINT MECHANISMS

The two possible kinds of consistency constraints may

be specified in PSN as follows:

- structural constraints, i.e. restrictions to the

structural contents of the p-sets are expressed using

a special ' WHERE-clause ' of the p-set 'CREATE'

operation or the 'TEMPLATE' definition which define

the build-up of new p-sets (See details in [6] and an

example in 4.2.1.),

- operational constraints, i.e. restrictions to the

data model's operations and their 'legal' operands,

are expressed using predicates and/or Boolean

expressions as provided by the programming language

C

.

So, PSN provides a meta language which is based on

(indexed) p-sets, primitive PSP-operations , and C-codeextensions. As all these tools are formal and even machine

executable, their semantics is well defined with respect to

any software system which 'understands' p-sets, PSPcommands, and C-code. The Positional Set Processor was

developed for that purpose.

2.4. AN EXAMPLE

In order to compare the two specification methods, we

will now apply both of them to a common object system. As a small example we choose a subset of the relational data

model as formally specified in two alternative ways in [9]

and [ 6 ]

.

2.4.1 THE VDM SPECIFICATION

2. 4. 1.1 Structures

The abstract structures are specified in VDM in the

'semantic domains' of the formal model. In this example, we

- 9 -
introduce the basic concepts of a relational database,

relations, tuples, elementary values, and relation- and

attribute-identifiers.

In the first line of the semantic domain definitions

(1), we 'denote' the set of all possible relational

databases (RDB) by an abstract VDM (meta) data structure

'map' which maps each relation identifier (from RELID) to

its corresponding relation variable (from REL) . Relation

variables, in turn, are denoted by the abstract set of all

tuples which they contain (2) . Each abstract model of such a tuple (from TUPLE) maps its set of attribute identifiers

(from ATTRID) to their respective values (3). Values may be

taken from one of the three predefined VDM (meta) value

sets: numeral (NUM, i.e. integer or real). Boolean (BOOL),

or 'quotation' (QUOT) which represents the set o f

und iv isible character strings (4). Finally, both kinds o f

identifier sets are not considered any further in this

semantic model, therefore being regarded as j ust ' tokens

(from the predefined VDM set TOKEN, see lines 5 and 6) .

SEMANTIC DOMAINS

RDB = (RELID > REL) (1)

REL = TUPLE - Set (2)

TUPLE = (ATTRID > VAL ) (3)

VAL = NUM | BOOL | QUOT (4)

RELID = TOKEN (5)

ATTRID = TOKEN (6)

As the consistency or integrity constraints can be

classified as either structural (or 'static') or operational

(or 'dynamic'), we will now present each set together with

the corresponding (structural or operational) part of the

formal model.

STATIC CONSISTENCY CONSTRAINTS

In VDM, the semantic domains define sets of abstract

objects denoting the structural components of the system to

be described. The static consistency constraints restrict

the sets of all possible abstract objects to only their

'well formed' elements. All consistency constraints are

expressed as predicates (i.e. Boolean functions), mapping

the well formed objects to true , all others to false . As all

abstract VDM functions, the predicates have their respective

types listed in the last line of the corresponding formal

function specification.

- 10 -
So, in our example, it is stated as a static

consistency constraint in [9] that all tuples within each

database relation have the same set of attribute identifiers

(i.e. their denotations have the same domain, dom ) . For

instance, this constraint (and, maybe, further additional

constraints) is formally specified by the following

predicate. It maps any relational database (from RDB) to

true (from BOOL) if it is 'well formed', and to false

otherwise

is-wf-RDB (rdb) =

( V relid 6 dom rdb )

( V tuplel, tuple2 G rdb (relid) )

( dom tuplel = dom tuple2 ) and ... (further constraints) ... type : RDB > BOOL

2. 4. 1.2 Operations

In VDM , the abstract structure

specified in the 'syntactic domain'

model. As an example, we describe

(from the abstract set 'Insert')

tuple into a relation. First,

of the oper

part of th

the 'insert'

which inserts

the operation's

syntactical structure is defined: The insert oper

based upon an identifier (from RELID) for the relat

altered, and on the new tuple (from Newtuple) which

inserted into the relation. This new tuple is, o denoted by an element of the abstract set TUPLE as

in the semantic domains above.

ations is

e formal

operation

a single

abstract

ation is

ion to be

is to be

f course,

defined

SYNTACTIC DOMAINS

Insert :: RELID Newtuple

Newtuple = TUPLE

Similar to the static consistency constraints,

abstract denotations for the operations (described in

syntactic domains) are usually constrained too. Th

operational or dynamic restrictions are

'dynamic consistency constraints' which

operation is 'well applied' to well formed

defined in

state whether

operands or no

the

the

ese

the

an

t

- 11 -
For instance,

relation whose decla

( 1 ) . Furthermore

relation variable m

identifiers as the n

a new tuple may only be inserted into a ration already exist in the database

tuples in the content of such a selected

ust have the same set of attribute

ew tuple to be inserted (2).

These constraints.

Boolean function (is-wf

representation of the

together with a model of

Boolean value.

again, are expressed in VDM by a -Insert) which maps an abstract

insert operation (from Insert)

the database (from RDB) to a

DYNAMIC CONSISTENCY CONSTRAINTS

is-wf-Insert (insert) (rdb) =

s-RELID ( insert) 6 dom rdb (1)

and ( V tuple 6 rdb (s-RELID (insert)) )

( dom tuple = dom s-Newtuple (insert) ) (2)

type : Insert > ( RDB > BOOL )

The semantic meaning of each operation is denoted by a function in the 'elaboration functions' part of the formal

model. This function describes the transition from one

database state (from RDB) to a new, altered one. Its type is

given by an abstract map which relates a database state

change (from the abstract set of maps (RDB >RDB) ) to the

execution of each given insert operation (from Insert). So,

for each insert operation and an actual database state, the

elaboration functions yields a new database state.

ELABORATION FUNCTIONS

elab-In ser t ( inser t) (rdb) =

let mk-Insert ( rel id ,newt upl e) = insert in (1)

let set 1 be rdb (relid) , (2)

set2 be { newtuple } in (3)

let newset be setl u set2 in (4)

rdb + [ relid > newse t ] (5)

type : Inse rt —-> ( RDB > RDB )

- 12 -
The specification of the elaboration function for the

insert operation ( eval-Inser t ( . . ) ) starts with making

available the two parts of its input parameter ('relid' and

'newtuple') for the scope of the function specification

(1). Then, two set-constants are defined to contain the old

relation value and the new tuple to be inserted into it

(2,3). A third set constant is declared to contain the union

of the first two sets (4). The result of this elaboration

function is the denotation of the altered database state,

denoted by a map, rdb, which is updated with respect to one

element, relid, of its domain (5).

2.4.2 THE PSN SPECIFICATION

The whole interactive software environment to define,

test, and evaluate data models specified in PSN is the 'data

model processor' (DMP) [5]. The DMP is divided into several

parts, describing the different human roles which a user may

play in the process of specifying, initializing, and

evaluating a data model and its applications. The most

important part he has to play is that of a 'data model

definer'. In this role, a user defines the semantics of an

intended data model by providing a complete specification of

its semantics using PSN.

2. 4. 2.1 Structures

In a data model specification in the DMP framework, the

data model definer first uses PSN to define the structures

that can be expressed and manipulated in the data model to

be described. All abstract data structures are defined in

the 'p-set definition' part of the formal model. In its

'concept definition section', the new concepts are

introduced together with the p-sets which represent them in

the model

We demonstrate

models by applying it

the PSN specification method for data

to the same example as above: In [6],

a relational database is viewed

different relation occurrences. So,

concept 'RELATIONS' is declared

structure' (using the DMP command

represented by the p-set 'REL-OCC'.

also be a 'definition-structure', declared by

type definitions. This concept, however,

mentioned in this example.)

(in part) as a set of

in this example, the new

as a PSP 'occurrenceREP-OCC) and will be

(In addition there might

REP-DEF , for

will not be

- 13 -
CONCEPT DEFINITION SECTION

> REP-OCC RELATIONS WITH REL-OCC

In the following 'p-set definition section' , the p-sets

declared in the previous section are defined in detail using

other DMP operations. First, in a command file (1-3), a range declaration (RG) associates all later used range

variables with their respective p-sets (2). Then, the

'TEMPLATE' command provides a description for each p-set

without actually enumerating its elements explicitly (4-10):

a p-set skeleton lists the configuration of position

identifiers (4); the following 'WHERE' clause further

constrains the set of all possible duplexes which may

appear in such a p-set (5-10).

Again, we concentrate on the specification of relation

occurrences (REL-OCC) only:

P-SET DEFINITION SECTION

> BEGIN <range-def ini tion-command-f ile> (1) —> RG RO IS REL-OCC (2) —> END <range-def ini tion-command-f ile> (3)

> TEMPLATE REL-OCC = [[RNgName,

RR-TPL@Relat ion] # ...] (4)

WHERE (5)

ISA -C RN, (6)

CD REL-OCC = CD (CR WITH (RO.Name)), (7)

TEMPLATE RR-TPL = [ [V@P ( J ) . . J] @# . . .

(8)

WHERE (9)

I SIN P(J) ATTF(RN) (10)

• • •

STRUCTURAL CONSTRAINTS

In PSN , the structural consistency constraints are part

of the p-set definition. In the example given above, for

instance, it is stated that all relation names (RN) have to

be of type 'character' (-C) (6), relation names have to be

unique within the set of all relation occurrences (7), and

the tuple attribute identifiers have to match those of the

relation's type definition (as derivable by an auxiliary

function ATTF) (8-10)

- 14 -
2. 4. 2. 2 Operations

In the DMP framework, the semantic specification of the

operations is based on the set of executable PSP commands.

In the environment of a C program which emulates the

specified operations, the execution of a PSP command is

invoked by a procedure call to the PSP ( expsp(...) ) - similar to a system call.

In this example, one temporary p-set is created (CR)

for the argument relation's value (3), another one for the

tuple to be inserted (EN) (9); then, the union (UN) of both

p-sets is established as the new relation value (10). Prior

to its use, each new range (RG) variable (declared in 2,5,7)

is released (RL) from any prior association with another pset (1,4,6)

insert-T (REL, NEWTUP)

char *REL, *NEWTUP;

{

• • • expsp ( "RL XI") ; (1

expsp ("RG XI IS REL-OCC" ) ; (2)

expsp ( st ringf (buf f 1," CR TMP1 WITH \"(X1.ALL)\"

WHERE \" (xl. Name = ' %s ' ) \"

" , REL) ) ; (3)

expsp ("RL Q"); (4)

expsp ("RG Q IS TMP1 " ) ; (5)

expsp ("RL R"); (6

expsp ("RG R IS Q. Relation" ) ; (7)

expsp ("CR TMP2 WITH \" (R.ALL)\" n

) ; (8)

expsp ( st ringf (buf f 2 ("EN \"[[%s]@#]\" NEWTUP",

NEWTUP)); (9)

expsp ("UN TMP2 NEWTUP INTO TMP3" ) ; (10)

• • •

}

2.5 COMPARISON OF THE TWO SPECIFICATION METHODS

Most of the differences between VDM and PSN stem from

the d if ferent purposes for which each of them was originally

designed

VDM is a specification method which is intended to be a tool for a more systematic approach to (in essence) manual

development of software. It uses a meta-language

incorporating the modeling power of first-order logic to

- 15 -
ease the appropriate modeling of more complex object systems

(such as programming languages as well as database models) . Its formal tools are very rich, high-level, and applicable

in a flexible way. VDM emphasizes comprehensiveness of its

abstract semantic models for a broader set of users. VDM '

s

semantic models, however, are not machine processable.

PSN is designed as a basic, but yet sufficiently

powerful formal notation to support data modeling. It is

based on a small set of well defined mathematical concepts.

Its meta-language does not emphasize comprehensiveness for

the (mathematically inclined) human reader. The notation is

simple, unambiguous, and straightforward for modeling the

structural aspects of a (data model) object system. Abstract

formal PSN models are machine processable for a computer

based interpreter, the DMP.

The specification of the operational/behavioural

aspects of an object system is based on denotational

semantics in VDM. That is, the specification is based on

sound mathematical concepts and the semantics of the metalanguage is well defined. Meta IV is powerful enough to

express completely all semantic aspects of any object system

(with the exception of concurrency).

In the PSP, the specification of the operational

aspects of an object system relies on an extensive (but not

totally comprehensive) set of PSP commands. All of them are

implemented to be machine executable. However, the semantic

meaning of this kind of meta-language is basically defined

by its implementation only. Some parts of the operational

aspects of a PSN-based model still have to be expressed in

terms of their implementation in C code. Whether the PSN

primitives could be extended to avoid the necessity of Ccode augmentations is still an open and debatable question.

In VDM however, the full and extensive use of the metalanguage may lead to many different, complex, or even

inconsistent abstract semantic models. All analyses, tests,

and interpretations have to be performed 'manually', because

aids to any kind of automatic interpretation of the model do

not exist - and may be subject to human error. (As mentioned

above, the sheer volume of a complex specification can make

it quite difficult to ensure its consistency.)

The two specification methods compared in this report

have different objectives and, thus, different properties.

An important objective of PSN is to provide automatically

treatable formalizations of data model semantics. But this,

on the other hand, leads to some lack of richness and

formally sound foundations of the meta-language (especially

- 16 -
with respect to its ability to specify operations).

Contrarily, VDM emphasizes a rich, powerful and more easily

understood meta-language. But Meta IV has no automatic aids

to analyze and/or interpret the semantic models (although

they tend to be rather complex when specifying non-trivial

object systems)

In order to overcome some of the deficiencies of the

two methods in consideration, two major solutions arise:

The first one would be to provide the PSN meta-language

(i.e. the PSP commands) with a semantically sound formal

definition. This could be expressed using any formal

semantic specification technique, an appropriate one being,

e.g., VDM. This approach is further elaborated in chapter 3.

In addition, the meta-language should be extended in order

to avoid the use of C-code in its behavioural

specifications.

The other alternative would be to make VDM's abstract

models treatable by some kind of automatic analyzer and/or

interpreter. This seems to be more difficult to apply to the

whole extent of meta-language features in Meta IV. But a semantic specification that uses the full set of 'Meta IV'

language constructs could be transformed into one that uses

only a certain subset. It should then be possible to

interpret the constructs of such a (slightly restricted)

specification automatically using an appropriate processor.

Choosing the PSP for this task would mean integrating the

advantages of both methods in a quite natural way. The

second approach is further addressed in chapter 4.

- 17 -
3. FORMAL SEMANTICS OF THE DATA MODEL PROCESSOR

3.1. INTRODUCTION TO THE FORMAL MODEL

This chapter provides a completely formal semantic

specification of PSN and major parts of the corresponding

PSP operations as described in [5] and [6]. The 'object

system' to be modeled here consists of the structured

objects (p-sets) as defined in PSN, accompanied by a set of

(PSP) commmands to manipulate these structures.

As an appropriate semantic specification method, VDM is

choosen. According to VDM, the formal semantic model of PSN

is divided into the following major components:

- the ' semantic domain ' definitions (3.2.1) specify the

denotations for all structural aspects of PSN upon

which the operations of the PSP are based,

- the ' syntactic domain ' definitions (3.3.1) list the

abstract syntax of all operations (i.e. PSP commands)

and describe the structure of their respective

operands

,

- the ' elaboration functions ' (3.3.3) specify the

meaning of the operations; their semantics is denoted

by semantic functions on the abstract sets of

structure denotations as defined in 3.2.1 and 3.2.2,

and

- the ' consistency constraint ' definitions state

additional restr ic tions on both the structural (or

'static') (3.2.3) and the operational (or 'dynamic')

(3.3.2) aspects of the model.

In the following subsections, shor

introductions precede the formal specifications o of the semantic model. These introductions are no

be part of the semantic model, but should rathe

explanatory hints for readers who are less famili

meta-language of VDM.

in fo rmal

eac h part

meant to

g iv e some

wi th the

In the informal

concepts are abbreviated

their denotations are

specifications.

introductions

,

(in brackets)

ident i f i ed

newly introduced

in the same way as

in the formal

- 18 -
3.2. STRUCTURE SPECIFICATION

3.2.1 ABSTRACT SYNTAX

The PSP provides an interpreter for a set of high-level

operations which can be applied to p-sets. The meaning of

the 'PSP commands' is based upon two auxiliary structures

which have to be specified in a formal semantic model:

- A 'range variable table' (RVTABLE ) contains all

declared range variable identifiers (RVID) , together

with their corresponding ranges (RANGE). These ranges

may be defined either by a positional set identifier,

or by a 'term' (TERM), i.e. a selected element of

another range variable's range.

- A 'freeze table' (FRTABLE) contains at all times the

actual bindings for each range variable to one

particular duplex out of its respective range.

All identifiers used in this model are regarded as

being just 'tokens' which have no further semantic content.

SEMANTIC DOMAINS

PSN • • • • PSETS RVTABLE FRTABLE

PSETS = (PSID -—> PSET)

PSET = DUPLEX: - Set

DUPLEX • •• • ELEM POSID

ELEM - ATOM | PSET

POSID = £ I NUM | CHAR

ATOM sz NUM | CHAR

CHAR = QUOT+

RVTABLE = (RVID - —> RANGE)

RANGE ss PSID | TERM

TERM • •

• • RVID POSID

FRTABLE = (RVID -• —> DUPLEX)

PSID — TOKEN

POSID = TOKEN

RVID = TOKEN

- 19 -
3.2.2 THE GLOBAL STATE

Later on, we specify the constraints and some PSP

operations for the PSN structures defined above. Formally,

all their semantics is 'denoted' by semantic functions based

on these structures. Thus, nearly all semantic functions

would have to contain the PSN structure definitions as part

of their parameters. To make these function definitions more

readable, VDM provides a way to declare the main structural

parts of a semantic model as 'global' (meta-) variables,

i.e. to make them globally 'accessible' for each semantic

function. In our case, for example, the 'global state' for a PSN model consists of three components which are declared

and initialized in the following way:

GLOBA L S T ATE

del PS : = [...] type PSETS

del RV : = [...] type RVTABLE

del FR : = [...] type FRTABLE

All global variables are initialized with the component

values of the corresponding semantic domain objects. Thus,

for any given psn € PSN, the global variables refer to the

contents, c, of its respective subcomponents at any time:

c P£ = s-PSETS (psn) , c RV = s-RVTABLE (psn)

c FR = s-FRTABLE (psn)

and

The whole state is referred to as in the 'type'

declarations of the following semantic functions.

3.2.3 STRUCTURAL CONSTRAINTS

In addition to the structural properties defined above,

each 'well formed' PSN model is constrained (at least) by

the following requirements:

1. p-sets and range variables have to have different

identifiers,

2. all 'frozen' range variables from the freeze table

have to be declared in the range variable table,

- 20 -
3. all p-sets have to be 'well formed' , i.e. all their

position identifiers have to begin with a letter,

4. the range variable table has to be 'well formed',

i.e. it may contain only well defined p-sets as the

range of each range variable, and

5. the freeze table has to be 'well defined' too, i.e.

each range variable can only be frozen to a duplex

from its correct respective range.

These constraints are specified by a Boolean function

(predicate), is-wf-PSN, with auxiliary functions used

whenever the readability can be improved. (The numbers in

brackets refer to the list above.)

STATIC CONSISTENCY CONSTRAINTS

is-wf-PSN () =

dom c PS n dom c RV = {

}

(1)

and dom c FR < dom c RV (2)

and ( V pset 6

( is-wfrng

PSET

c PS ) (pset) ) (3)

and is-wf-RVTABLE 0 (4)

and is-wf-FRTABLE 0 (5)

type : S > BOOL

3.2.4 AUXILIARY FUNCTIONS

Auxiliary functions are used either to specify common

parts of different functions of the formal model, or to

express certain properties in more detail at a separate

place to improve the readability of the specifications.

Here, the auxiliary functions for the specification of

the static consistency constraints first define in detail

which p-sets, range-variable-, and freeze-tables are well

formed :

- 21 -
A p-set is well formed, iff it is structured as

described in the semantic domains, and, in addition, the

position identifiers of all duplexes in the p-set begin with

a letter, if they are character strings:

is-wf-PSET (pset) =

( V duplex G pset )

( let posid b£ s-POSID (duplex) iji

is-CHAR (posid) ===>

posid [1] G {A, ... , Z } ) type : PSET > BOOL

A range-variable-table is well formed, iff for all

declared range variable identifiers their corresponding

ranges are well formed. (Note: As the parameter, RV, to

this function is part of the global state, S, the function

specified here has no explicit parameters.)

is-wf-RVTABLE () =

( V rvid G dom £

RV )

( is-wf-range (£ RV (rvid) ) ) type : S > BOOL

What is meant by a well formed 'range' is then

specified formally by another auxiliary function which

states the well-formedness conditions for both possible

kinds of ranges (PSID or TERM)

- either the position identifier is an actually

declared p-set which is part of the content of the

global state variable PS, or,

- if the range

variable identif

an actually ex

range variable'

another auxiliar

is defined in terms

ier, the position id

isting duplex out o

s range (which is

y function, get-rang

of another range

entifier selects

f that particular

determined by

e) .

- 22 -
is-wf-range (range)

cases range of : (mk-PSID (psid) > psid G dom c PS

mk-TERM (rvid, posid) > rvid G dom c RV

and ( V duplex G get-range (rvid) )

( is-PSET (s-ELEM (duplex))

and ( duplex' G s-ELEM (duplex) )

( s-POSID (duplex') = posid ) ) ) type : RANGE > BOOL

The freeze-table is well formed, iff each range

variable identifier in its domain is 'frozen' to a duplex

from the corresponding range.

i S-wf-FRTABLE () =

( V rvid G dom c FR )

( c FR (rvid) G get-range (rvid) ) type : S > BOOL

The next two auxiliary functions formally define the

range of a range variable identifier and specify how to

select a set of duplexes from a p-set identified by a given

position identifier.

The corresponding range for a range variable identifier

is a set of duplexes which is determined by the auxiliary

function 'get-range':

get-range (rvid) =

cases £

RV (rvid) £f : (mk-PSID (psid) > £ PS (psid) , mk-TERM ( rvid ', posid) > { duplex | duplex G dot ( dupl ex ', posid

)

and duplex' G get-range (rvid 1 ) } ) pre : rvid G dom c RV and is-wf-range (c RV (rvid)

)

type : RVID > PSET

- 23 -
Given a position identifer, the aux

'dot' selects the corresponding duplex f

Because, in general, position identifiers in

necessarily distinct, the result is a se

duplexes, i.e. a p-set.

il iary

rom a a p-se

t of

function

p-set

.

t are not

selected

dot (pset,posid) =

let duplex € pset be £.t,.

s-POSID (duplex) = posid _in

s-ELEM (duplex)

pre : ( duplex € pset )

( s-POSID (duplex) = posid ) type : PSET POSID > PSET

Both of

only if some

parameters are

stated in the

specifications,

functions has

satisfied prior

the last two functions a additional (pre-) condi

satisfied. These pre-cond

1 pre 1 predicates at the

Each environment which

to make sure that al

to a function applicatio

re applied correctly

tions on their input

itions are formally

end of the function

uses any of these

1 pre-conditions are

n

.

3.3. OPERATION SPECIFICATION

3.3.1 ABSTRACT SYNTAX

The PSP is a software tool for interpreting and

manipulating p-sets. With the PSP commands, it provides a set of powerful operations which can be applied to the PSN

structures as defined above.

In this subsection, the abstract syntax of the PSP

operations is analyzed, i.e. their names are declared, and

the structure of their respective operands is described in

an abstract way wi thout considering any details o f the

syntactic notion • Not all PSP commands will be considered in the

semantic model . As an example, only some of the more

important operations are defined formally. Those PSP

commands (Psp-cmd) specified here include: the 'rangevariable' declaration (Range_dcl) , the 'release' command for

range variables (Release), the command to 'enter' a p-set

expression into a p-set (Enter), the 'delete' (Delete),

- 24 -
'freeze' (Freeze) and 'thaw' (Thaw) commands for p-sets, and

the more complex 'create' (Create) command to build up and

store new p-sets.

P-set expressions (Ps-expr) describe all possible ways

of creating new sets of duplexes (i.e. p-sets) from existing

structures: from a p-set-identif ier (PSID) , a whole p-set

(PSET) , a classical set (C-set) , a union of two other p-set

expressions (Un-expr) , or a p-set 'create' expression (Pscr-expr )

,

etc.

SYNTACTIC DOMAINS

Psp-cmd Range-del | Release | Enter 1 Delete I Freeze | Thaw | Create | Range-del RVID RANGE

Release RVID

Enter PSID Ps-expr

Delete PSID

Freeze RVID Cond

Cond = (DUPLEX > BOOL)

Thaw • • • • RVID

Create • • • • PSID Ps-cr-expr

Ps-cr-expr • • • • A-list Cond

A-list = Attribute - Set

Attribute = TERM | Attr-asgn

Attr-asgn • • • • POSID Phrase

Phrase = ATOM | Ar th-expr | TERM

Ar th-expr =s • • • Ps-expr = PSID | PSET | DUPLEX | C-set

| Un-expr I Ps-cr-expr 1 . .

C-set = ELEM - Set

Un-expr • • • • Ps-expr Ps-expr

- 25 -
3.3.2 OPERATIONAL CONSTRAINTS

The operations are basically constrained by the kinds

of arguments they can take. In the previous subsection, some

of those constraints are expressed through the structural

definition of the operations's operands. But there are

further 'operational constraints', e.g.: not only must the

first argument of the 'Range' command be a range variable

identifier (rvid), but also must all mentioned range

variable identifiers be declared previously, i.e. be part of

the domain of the range variable table referred to by RV.

Similarly, the second argument (range) of this command is

restricted with respect to the structure definitions given

in the 'semantic domains', etc.

In the same way as the structural constraints,

operational constraints are defined as Boolean functions,

i.e. predicates, over the set of abstract operations as

listed in the syntactic domains. Here again, only some

operational, or 'dynamic' constraints will be defined

exemplar ily.

DYNAMIC CONSISTENCY CONSTRAINTS

The dynamic consistency constraints check whether the

operations are applied to well formed operands. Here, the

whole (Boolean) function to check the well-formedness of the

PSP commands is divided into different cases according to

all listed alternatives for the operations. An (is-wellformed) predicate is specified for each PSP command which is

described in the syntactic domains:

i s-wf-Psp-cmd (psp-cmd) =

cases psp-cmd of : (mk-Range (rvid, range) > is-wf-range (range)

and rvid € dom c RV , mk-Release (rvid) •> rvid G dom c RV

mk-Enter ( psid ,ps-expr ) > is-wf-Ps-expr (ps-expr)

and psid € dom c PS , mk-Delete (rvid) -> rvid G dom c RV , mk-Fr ee ze (rvid,cond) -> rvid G dom c RV

and ( V duplex G get- range (rvid) )

( dupl e'x G dom cond ) ,

- 26 -
mk-Thaw (rvid) > rvid 6 dom c RV f mk-Create ( psid ,ps-cr-expr ) ---—

let mk-Ps-cr-expr (a-list ,cond)

be ps-cr-expr jji

psid G dom c PS

and is-wf-Ps-expr (ps-cr-expr)

and ( ¥ duplex 0 max-pset (a-list) )

( duplex 0 dom cond ) , ... ) type : Psp-cmd > BOOL

The next auxiliary function defines which p-set

expressions are well formed. It is mainly used in the

previous specification of the well formed operations

(operands). Note that no additional restrictions are imposed

on p-set expressions from the abstract sets PSET, DUPLEX, or

C-set. Note also, that the predicate for the p-set 'create'

expression, ps-cr-expr, makes sure that the condition, cond,

in this expression is defined for all possible duplexes

which may conform to its attribute list. This 'maximum' pset conforming to the specified attribute list can be

derived by the auxiliary function 'max-pset' which is

formally defined in 3.3.4.

is-wf-Ps-expr (ps-expr) =

cases ps-expr <Df : (mk-PSID (psid) > psid 0 dom c j?S , mk-PSET () > true , mk-DUPLEX () > true , mk-C-set () > true , mk-Un-expr (psel,pse2) > is-wf-Ps-expr (psel)

and is-wf-Ps-expr (pse2)

mk-Ps-cr-expr (ps-cr-expr) > let mk-Ps-cr-expr ( a-1 i st ,cond ) b£ ps-cr-expr

( ¥ duplex 0 max-pset (a-list) )

( duplex 0 dom cond ) , ... ) type : Ps-expr > BOOL

in

- 27 -
3 . 3 . 3 OPERATION SEMANTICS

In the last part of the semantic

finally define the semantics of the operat

syntactic domains. The semantic meaning of

denoted by an 'interpretation function' wh

mapping of one instance of the global

operation's execution) to a new one (after

execution)

model for PSN, we

ions listed in the

each operation is

ich describes the

state (before the

the operation '

Thus, the interpretation function for PSP-commands

specifies a state change for each different PSP operation.

In case the operation is a range variable

declaration/release, the global state component RV is

updated with respect to that particular range variable” The

meaning of entering/deleting a p-set in the model is denoted

by a change of the global state component PS.

The semantic description of the 'freeze' command is

divided into two different alternatives. In the first

case, the range variable to dp frozen (according to a given

condition, cond) is not defined in terms of another

range variable identifier. Then, a duplex satisfying the

condition is chosen out of its respective range, and the

global £R state component is updated with respect to that

range vaTiable identifier. The other alternative is that the

range of the argument range variable identifier is defined

by (in general) a list of 'ancestor' range variable

identifiers (via 'dot' selection). In this case, the list is

derived (ancestorl) , all corresponding duplexes are chosen

(duplexl) , and then the FR-table is updated with respect to

all ancestor range variable identifiers.

The 'thaw' command releases a given range variable

identifier together with the elements of its list of

'descendent' range variable identifiers (derived by the

auxiliary function ' descendents ' ) from the FR-table in the

global state. In the denotation of the 'create' command,

the p-set expression, cr-ps-expr (as specified later) is

evaluated first, and then the result is entered into the set

of all defined p-sets referred to by PS.

The interpretation

global state change.

of each PSP command results in a

- 28 -
ELABORATION FUNCTIONS

int-Psp-cmd (psp-cmd) =

cases psp-cmd £f : (mk-Range (rvid, range) > RV : = £ RV + [rvid —> range] , mk-Release (rvid) > RV := c RV \ {rvid} , mk-Enter (psid ,ps-expr) > let pset b£ eval-Ps-expr (pset) rn PS := c PS + [psid —> pset] , mk-Delete (psid) > P£ := c _PS \ {psid} , mk-Freeze (rvid,cond) >

if parent (rvid) = undefined

then let duplex € get-range (rvid)

be £.t_. cond (duplex) rn FR := £

FR + [rvid —> duplex] , else let ancestorl be ancestors (rvid) in

let duplexl be < dx[i] I dx[i] G get-range (ancestorl [i])

and s-ELEM (dx[i]) G dot (s-ELEM (dx[i-l]),

s-POSID (£ RV (ancestor [i])))

and cond (s-ELEM (dx[n]))

and 2 < i < n=len ancestorl > in

FR := £FR + [rvid [i] —> duplexl [i] | 1 < i < n and

rvTd [T] = ancestorl [i] ] , mk-Thaw (rvid) > let descendentl be descendents (rvid) rn FR := £ FR \ elems descendentl , mk-Create (psid , ps-cr-expr) > let p-set be eval-Ps-expr (ps-cr-expr) in_

FR := £

FR + [ psid —> p-set ] ,

. . ) type : Psp-cmd > ( S > S )

-29-
Th e eval uation of al 1 different kinds of

1 isted in the syntactic doma ins is denoted by

f unc t io ns 11 whi ch map an expr ession and an actual

the sta te into a particular ( in general compl

Here f we cone entrate on the evaluation of p-set

only •

If > P" set expression is given by a p-set

expressions

' evaluation

instance of

ex) value,

expressions

it is evaluated by deriving its corresponding p-set from the

global state component P£. If a p-set is given, that p-set

is simply returned. A duplex is evaluated as a singleton pset that contains the duplex, and a classical set is mapped

into a p-set of duplexes with null position identifiers. A

'union' command creates a p-set from the union of its

evaluated argument p-set expressions. A p-set 'create'

expression first creates the set of all possible duplexes

conforming to the given attribute list (using the auxiliary

function 'max-pset'), and then selects only those duplexes

which satisfy the specified condition.

The evaluation of each p-set expression returns a pset

.

eval-Ps-expr (ps-expr) =

cases ps-expr of : (mk-PSID (psid) > mk-PSET (pset) > mk-DUPLEX (duplex) > mk-C-set (c-set) >

£

PS (psid) , pset ,

{ duplex } ,

{ mk-DUPLEX (elem,_#)

elem G c-set f mk-Un-expr ( pset 1 , pset 2 ) >

let p-setl be eval-Ps-expr (psetl) , let p-set2 be eval-Ps-expr (pset2) j_n

psetl u pset2 , mk-Ps-cr-expr ( a-1 i st ,cond ) >

let m-pset be max-pset (a-list) rn select ( m-pset ,cond ) ,

. • ) type : Ps-expr > PSET

- 30 -
3.3.4 AUXILIARY FUNCTIONS

The first

specification of

what is meant by

a range variable

three auxiliary functions for the

the operations' semantics formally describe

'parent', 'ancestors', and 'descendents' of

identifier

.

parent (rvid) —

if_ is-PSID (c RV (rvid))

then undefined

else s-RVID (RV (rvid))

pre : rvid

type : RVID

€ dom c RV

RVTABLE > RVID

ancestors (rvid) =

< rvid [i] |I parent (rvid [1]) = undefined

and rvid [i] = parent (rvid [i+1])

and rvid [n] = rvid and 1 < i < n > pre : rvid

type : RVID

€ dom c RV

> RVID+

descendents (rvid) =

< rvid [i] |I rvid [1] = rvid

and rvid [i] = parent (rvid [i+1])

and is-PSID (c RV (rvid [n] )

)

and 1 < i < n > pre : rvid

type : RVID

€ dom c RV

> RVID+

The auxiliary function 'max-pset' derives for any given

attribute list (from A-list) the (maximum) set of all

possible duplexes which conform to that particular attribute

list. It does this by first determining the ancestor

'chains' for all dependent and independent range variable

identifiers. (A range variable identifier is regarded to be

'independent' if it is not defined in terms of any other

range variable identifier.) Then a ' produc t ' -set (similar to

a relational 'join') is built up for all independent range

variable identifiers. This set is finally 'projected'

(and/or augmented) according to the given attribute list.

- 31 -
max-pset (a-list)

let rvid-chains be

get-rvid-cKains (a-list) in

let independent-rvids Ise { rvidl fl] I rvidl G elems rvid-chains } in

let product-pset be

product (independent-rvids) _in

project (product-pset, a-list)

type : A-list > PSET

The following auxiliary functions specify in detail the

semantics of the mentioned steps in the previous semantic

f unc ion

get-rvid-chains (a-list) =

let rvids be { rvid | attr G a-list and

( ( is-TERM (attr) ==> rvid = s-RVID (attr) ) or ( is-Attr-asgn (attr) ==>

( is-TERM (s-Phrase (attr)) and

rvid = s-RVID (s-Phrase (attr) ) ) ) ) } in

let independent-rvids be^ { rvid | rvid G rvids and

not ( ] rvid' G rvids )

( rvid' G elems ancestors (rvid) ) } in

{ rvidl | rvidl [1] G independent-rvids

and rvidl [i+1] G elems ancestors (rvidl [i])

and ( V rvid G rvids ) (5- rvidl, j)

( rvidl [ j] = rvid ) and 1 < i,j < len rvidl }

type A-list > ( RVID+ ) - Set

product (rvids) =

{ mk-DUPLEX (elem,#.) I elem = mk-PSET (pset)

and pset = { mk-DUPLEX (elem', rvid) | elem' G get-range (rvid)

and rvid G rvids } }

type : RVID - Set > PSET
project (pset ,a-list) =

{ mk-DUPLEX (elem, posid) | duplex € pset and

attr € a-list and

cases attr c^f : (mk-TERM ( rvid , posid ' ) > posid = posid' and

elem € dot (dot (s-ELEM (duplex) , rvid) , posid) , mk-Attr-asgn ( posid phrase) > posid = posid' and

cases phrase of :

type

(mk-ATOM (a) > mk-Ar i th-expr (ae) >

mk-TERM ( rvid , posid" ) —

s-ELEM (duplex)

PSET A-list > PSET

elem = a , elem = eval-Ar i th-expr

elem € dot (dot

,rvid)

,

posid”

)

(ae)

(

) )

9

}

select (p-set,cond) =

{ duplex | duplex € p-set

and cond (duplex) }

type : PSET Cond > PSET

The evaluation of arithmetic expressions will not be

specified in this context. For all possible kinds of

arithmetic expressions it yields an atom.

eval-Ar i th-expr (arith-expr) =

type : Arith-expr > ATOM

- 33 -
4. INTERPRETING DATA MODEL SPECIFICATIONS

4.1. OVERVIEW

The main goal of this chapter is to combine the

advantages of both VDM and PSN in a different way as

proposed above

.

This can either be looked at as making VDM's

abstract model

s

treatable by some kind of automatic

interpreter, or, from the other side, as providing PSN with

a more abstract, flexible, and more readable meta-language

on top of PSN and its already implemented PSP commands.

Then, the database model specifications can be expressed in

an abstract, high-level, and convenient way, and, on the

other hand, the specified systems can be automatically

emulated for machine supported testing and analysis at a very early stage of the design process.

The chapter proceeds

mapping a slightly restri

corresponding representat

PSP operations. Then, for

their respective operati

terms of PSN and the PSP c Finally, it is outlined

model can be constructed

analyzing and testing the

with an outline of

cted, formal VDM

ion in terms of PSN

all VDM (meta) data

the process of

model into a structures and

structures and

ons, executable interpretations in

ommands are defined in detail,

how an interpr etable VDM semantic

, and some automatic means of

specifications are suggested.

4.2. INTERPRETING A VDM MODEL ON THE DMP

The process of 'translating' a formal VDM semantic

model into its executable PSN/PSP representation can be

divided into several steps according to the main components

of the VDM specification.

4.2.1 STRUCTURE SPECIFICATION

4. 2. 1.1 Semantic Domains

In VDM, the object

'semantic domains' part of

each structure is repre

structures are specified

command. (The upper case

to their respective abbrev

structure definition i corresponding template d

str uc tur e the fo rmal

se nted by

in detail

1 etter s in

ia t ions in

n the VDM

ef ini ti on

s are defined in the

model. In the PSP,

a p-set, and the p-set

by a PSP 'TeMPl ate

the PSP commands refer

the DMP.) So, for each

semantic domains, a with the same name is

34
specified in the PSP interpreter. This template def

describes all possible p-sets which can represe

elements of that respective domain. How the right ha

of a semantic domain definition translates into the

(template) representation, depends on its abstract structure

and will be explained in detail in the following section.

If the VDM semantic domain definition makes use

BNF-like (bar) to specify different alternativ

possible structures of its elements, this defini

translated into as many alternative p-set t

definitions. Thus, each actual p-set representation

such domain element has to 'conform' to one

corresponding templates at all times.

Then, for all abstract object types defi

semantic domains, an (in general recursiv

Cob j ect-type> ' function is automatically genera

system. It yields true for any object (i.e. p-set)

conforming to that type, and f al se for all othe

may be based on other ' is-<obj

the particular abstract object

terms of other semantic domain

' is-<object-type> ' function makes

to test the membership

ini t ion

nt the

nd s ide

P- set

rue ture

ion

.

o f the

es for

t ion is

empl ate

l of any

o f the

i in the

1 isby the

to

This function

functions, if

specified in

Finally, the

' I S IN ' PSP command

ned

e)

instance

r objects.

ect-type>

domain is

ob j ec ts

.

use of the

of an

el ement/dupl ex

an abstract VDM

instance

domain.

in an actual p-set which represents

4. 2. 1.2 Static Consistency Constraints

The restrictions to valid ('well formed') semantic

domain objects are expressed in VDM by Boolean 'is-wellformed' functions in the static consistency constraint part

of the formal model. If these ' is-well-formed ' functions are

expressed in a way such that each of them can be related to

the specification of exactly one semantic domain object, the

respective predicate is included in the 'WHERE' clause of

the corresponding template definition in the PSN/PSP

representation. Other static consistency predicates or

auxiliary functions should not be used in this part of the

VDM semantic model. (This does not restrict the

expressiveness of the formal model.)

4. 2. 1.3 Global State

To ease the interpretation of its semantic functions,

the VDM semantic model should be based on an explicit global

state. Then, for each database variable which is part of the

global state in the VDM semantic model, a corresponding pset variable is declared in the PSN/PSP representation. The

initial p-set value is either created by a p-set 'CReate'

command, or the PSP 'POPulate' operation may initiate a

- 35 -
dialog session to provide the initial duplex instances to

the system. In either case, the interpreting system has to

make sure that all values of the global variables conform at

all times to the template definitions which represent their

respective semantic domain object definitions.

4.2.2 OPERATION SPECIFICATIONS

4. 2. 2.1 VDM Model of the Operation Semantics

The abstract syntactic structure of the operations and

their operands is specified (in a similar way as the object

structures) in the 'syntactic domains' of the VDM semantic

model. Restrictions to the operands are defined by is-wellformed predicates in the 'dynamic consistency constraints'.

Each operation's semantics is then denoted by a semantic

'interpretation' function in the 'elaboration functions'

specification of the formal semantic model. If necessary,

there are also semantic 'evaluation' functions defined which

denote the meaning of any expression evaluation.

In the PSN/PSP interpretation of the operation

semantics model, the semantic functions are represented by

equivalent procedures and functions. How to derive these

procedures and function from the corresponding VDM semantic

functions will be explained in the next two paragraphs.

4. 2. 2. 2 Interpretation Functions

For each (operation) interpretation function of the

'elaboration functions' part of the VDM model, a procedure

is defined for the PSP according to the following

description

:

- the name of the procedure is given by the name of the

left-hand side of the corresponding rule in the

syntactic domains of the VDM model;

- the argument types for the procedure are given by the

p-set representations of the right-hand side of the

corresponding rule in the syntactic domains of the

VDM model; either these object types are already

defined in the semantic domains, or they (and their

p-set representations) are derived from such object

types in the same way as described for the semantic

domains objects in 2.1.1.

- the procedure bodies start with checking the

restrictions to the arguments as specified in the

dynamic consistency constraints of the VDM model. For

each operation, the corresponding ' is-well-formed

- 36 -
predicate is applied to check the validity of the

actual arguments of the procedure representing the

operation. If this check yields false, the operations

will not be interpreted, and some form of exception

handling takes place instead.

- Otherwise, the procedure body is built up by the PSP

representation ol the corresponding interpretation

function of the VDM model. How this representation is

derived from the VDM interpretation function will be

described later.

The executions of the 'semantic' procedures defined so far, can (and usually do) access components of the global

state. All these procedure executions result in sideeffects, i.e. changes to variables of the global state.

'Auxiliary' functions may be used, whenever it is

convenient, in the same way as in the VDM semantic model.

4. 2. 2. 3 Evaluation Functions

For each evaluation function which in VDM models the

semantics of evaluating expressions, a corresponding

function is defined in the following way:

- its name is

correspond ing

given by the left hand side of the

rule in the syntactic domains;

- its argument (type)s are given by the right-hand side

of the corresponding rule in the syntactic domains;

- restrictions to the arguments as possibly specified

in VDM ' is-well-formed ' functions (in the dynamic

consistency constraints) are checked at the very

beginning of each function evaluation;

- the resul

t

of a function call is (in general) a complex value as specified by the VDM evaluation

function definition, or, in case an

- error occurs during the

result is undefined , and

handling procedures may be

function eval

some special

triggered

;

uation, the

exception

- the function body is made out of the

restr ic ted ) VDM function specification. It

result value from the • function input

and/or additional components of the global

( si ightly

derives a parameters

state

.

No function evaluation does at any time change the

global state; i.e. functions do not have side effects. All

function definitions may be based on additional auxiliary

- 37 -
functions; but note that all necessary pre-conditions for

the application of these auxiliary functions have to be

checked as (possibly) specified in the respective 'prepredicates' at the end of each corresponding VDM function

specification.

4. 2. 2. 4 Interpreting the Semantic Functions

The specification meta-language of VDM uses a set of

abstract (meta) data structures to denote object structures,

and semantic function specifications to express the

semantics of the object systems' operations. Basically, the

VDM representations for semantic functions are expressed in

terms of a set of (meta) operations which are predefined for

all VDM meta data structures. Some (meta) control structures

may be used in a way known from usual high-level programming

addition, first-order predicates add to the

of the semantic functions' specifications,

alternative (and easier to use) means of

expressing certain parts of the function specifications are

provided. This (meta) syntactic 'sugar', however, does not

add to the specification power of the meta-language.

languages. In

expressiveness

Finally, some

In order to interpret the VDM semantic function

specifications on the PSP, we first have to provide

interpretations for (meta) data structures and their

respective operations. This will be shown in detail in the

next section. The VDM (meta) control structures can be

interpreted directly by the corresponding control structures

of the programming language environment of the PSP (as given

in the DMP and augmented by the programming language C)

.

The use of first-order predicates has to be restricted to

only those which can be represented in the 'WHERE' clauses

of the PSP 'CReate' commands. The 'syntactically sugared'

notations in the semantic functions' specifications can

either be interpreted after transformation into their

'unsugared', basic VDM equivalents, or, as they are in most

cases similar to usual programming language constructs,

directly by the PSP programming language environment.

4.3. INTERPRETATIONS FOR THE META DATA STRUCTURES

4.3.1 ELEMENTARY DATA TYPES

Meta IV,

three different

definition of

predefined sets

the meta-language of VDM basically provides

'elementary' (meta) data types for the

semantic objects. They are interpreted by

of atomic values in PSN as follows:

- 38 -
- the abstract VDM data type Boolean with its

corresponding value set BOOL and the set of Boolean

operations will be interpreted by usual Boolean data

type as available on the interpreting machine;

- the VDM data type Numeral (whose value set, NUM,

comprises INTEGER and REAL values) is interpreted by

the usual data types INTEGER and REAL combined;

- the VDM data type Quotation (value set QUOT) is

interpreted by the ( indivisible) character strings

CHARACTER in PSN/PSP.

All operations (i.e. all ways of deriving expressions)

in the elementary data types are interpreted by the

respective usual operations of the programming language

environment of the PSP.

4.3.2 COMPOSITE DATA TYPES

4. 3. 2.1 Sets

Any VDM abstract set, s, of elements, e_i , is

interpreted by the following p-set:

- in case the set was explicitly defined by the VDM

set specification, {e_l , . . . ,e_n} , it is interpreted

by the (classical) p-set { e_l@# , . . . ,e_n@# }

,

- in case the set was implicitly defined by the VDM

set specification, { e | e € E and P(e)}, it is

interpreted by the p-set-create expression

CR WITH e .all WHERE p(e) , provided a range variable, e, is declared to range

over the (p-set) interpretation of the set E.

The common set operators, union, intersection,

difference, cardinality, complement, membership, and subset

predicate are interpreted in a straightforward way by the

corresponding classical (p-) set operations, UN, IN, SY, CD,

ISIN , RC, and SB. However, application of the PSP commands

should be restricted to operands representing classical sets

only. Whether a p-set represents a classical set can be

checked by the PSP predicate CS.

All set operations are interpreted in terms of their

respective PSP commands, and, in addition, possibly some

high-level programming language constructs from the

programming language environment of the PSP. In this

section, the operation interpretations will be expressed in

a way similar to usual programming language function

- 39 -

l
definitions, stating first each function's name, its

parameters, possibly the type of its result (only if other

than p-set) , and then, as the function's body, the PSP

interpretation for the respective ( VDM) operation. As nearly

all parameters are p-sets, parameter types will be given

explicitly only if other than p-set.

So, the abstract VDM set operations can be interpreted

in the PSP in following way:

f unction

If

set union (pset l,pset 2) = CS (pset 1) and CS (pset 2)

then UN pset 1 pset 2

else undefined

function

if_

set intersection (pset l,pset 2) = CS (pset 1) and CS (pset 2)

then IN pset 1 pset 2

else undefined

function

i_f

set difference (pset l,pset 2) = CS Tpset 1) and CS (pset 2)

then SY pset 1 pset 2

else undefined

function

TF

set cardinality (pset) : INTEGER = CS (pset)

then CD pset

else undefined

function

n

set element (elem,pset) : BOOL = CS (elem) and CS (pset)

and CD elem = 1

then ISIN elem pset

else undefined

function

TF

set complement (pset l,pset 2) = CS (pset 1) and CS (pset 2)

then RC pset 1 pset 2

else undefined

function

TF

set subset (pset l,pset 2) : BOOL = CS (pset 1) and CS (pset 2)

then SB pset 1 pset 2

else undefined

- 40 -
4. 3. 2. 2 Tuples

Abstract tuples of the VDM meta-language consisting of

a list of components, c_i , are interpreted by the following

p-sets:

- an explicit tuple specification <c_l , . . . ,c_n> is

represented by the p-set [ [c_l@component , l@index] @#

,

. . . ]

,

and

- for an implicit tuple specification < f(i) I 1 < i < n >, where f is a function mapping integers

to components f: INTEGER > COMPONENTS, the

corresponding p-set representation is created by the

PSP-commands

RG c IS <p-set representation of COMPONENTS>;

RG i IS <p-set representation of INTEGERS l...n>;

CR WITH (component : =c , index:=i) WHERE (f(i)=c).

To assure the correctness of the operands for tuple

operations, we have to provide ways to test whether a given

p-set represents a tuple or not. Therefore, a 'tupletemplate', Tpl_tdef, has to be predefined in the PSP:

TMP Tpl_tdef = [ [c@component , i@index]@# ... WHERE (i € {1, . . . ,n} )

Based on this template definition, we can test whether a given p-set 'conforms' (CNF) to it or not.

Now, the selection of a single tuple component, indexed

by an integer value, i, can be interpreted by

function tpl select (tpl, i : INTEGER) = if CNF tpl TO Tpl_tdef and i < CD tpl

then { RG d IS tpl;

CR WITH (d .component) WHERE (d.index=i) }

else undefined

The other VDM tuple operations, len (number of

components), hd (first component), tl (tuple without first

component) , elems (set of components) , ind (index set)

,

update (change of a component as given by its index), and

concatenate (concatenates two tuples), are interpreted as

follows

function tpl len (tpl) = Tf CNF tpl TO Tpl_tdef

then CD tpl

else undefined

- 41 -
function

TI

function

IT

function

Tf

function

if

function

Tf

function

Tf

tpl_hd (tpl) = CNF tpl TO Tpl_tdef

then tpl_select (tpl,l)

else undefined

tpl_tl (tpl) = CNF tpl TO Tpl_tdef

then { RG d IS tpl;

CR WITH (d .component , index : =d . i ndex-1

)

WHERE (d. index * 1) }

else undefined

tpl_elems (tpl) = CNF tpl TO Tpl_tdef

then { RG d IS tpl;

RG c IS d. component;

CR WITH (c .all) }

else undefined

tpl_ind (tpl) = CNF tpl TO Tpl_tdef

then { RG d IS tpl;

RG i IS d. index;

CR WITH (i .all) }

else undefined

tpl_update ( tpl , i : integer , new) = CNF tpl TO Tpl_tdef and CNF new TO Tpl_tdef

and i £

CD tpl_elems (tpl)

and tpl_ind (new) = [i@#]

then { RG e IS tpl;

CR temp WITH (e .component)

WHERE (e. index 4 i)

UN temp new }

else undefined

tpl_concatenate ( tpl_l , tpl_2 ) = CNF tpl_l TO Tpl tdef and

CNF tpl_2 TO Tpl_tdef

then { RG e IS tpl_2;

CR temp WITH (e .component , i ndex :

e. index + tpl_len ( tpl 1 ) )

UN tpl_l temp }

else undefined

- 42 -
4 . 3. 2. 3 Maps

A VDM map, m, mapping domain elements, a_i € A, to

corresponding range elements, b_i € B, is represented in the

PSP by one of these methods:

- in case it is specified explicitly as m = [ a_l —> b_l, ..., a_n --> b_n] by the p-set

[ [a_l@argument , b_l@resul t] @# . . . ], or

- in case it is specified implicitly in terms of a predicate, p: (A,B) >BOOL, m=[a—>b | p(a,b)], its

p-set representation, m' , is created by the following

PSP commands:

RG a IS A; RG b IS B;

CR m' WITH (argument : =a , resul t : =b)

WHERE ( p ( a ,b) )

For type checking purposes, again, a ' map_templ ate ' is

defined in the PSP as

TMP Map_tdef = [ [a@argument ,b@resul t] @#. . .

]

WHERE CD Map_tdef = CD ( CR WITH (mtd .argument) ) provided 'RG mtd IS Map_tdef'.

The VDM operations defined for maps, rng (range), dom

(domain), apply (application of a map to an argument),

restrict (restriction of the domain of a map to a subset),

exclude (exclusion of a subset of a map's domain), alter

(extension and updating of a map by another map) , compose

(functional composition of two maps), and union (union of

two maps with disjunct domains) are interpreted by the

following functions:

function map dom (map) =

l

f

CNF map TO Map_tdef

then { RG p IS map;

CR WITH (p. argument) }

else undefined

function map rng (map) =

i

f

CNF map TO Map_tdef

then { RG p IS map;

CR WITH (p. result) }

else undefined

- 43 -
1

function

If

function

Tf

function

nr

function

Tf

function

IT

function

IT

map_apply (map,arg)

CNF map TO Map_tdef and

CS (arg) and CD (arg) = then { RG p IS map;

CR WITH (p. result)

WHERE (p.argumen =arg) }

else undefined

map_restrict (map, set) = CNF map TO Map_tdef and CS (set)

then { RG p IS map;

CR WITH (p.all) WHERE

( I S IN p. argument map_dom (map) ) }

else undefined

map_exclude (map, set) = CNFmap TO Map_tdef and CS (set)

then { RG p ISmap;

CR WITH (p.all) WHERE NOT

( ISIN p. argument map_dom (map) ) } else undefined

map_alter ( map_l ,map_2 ) = CNF map_l TO Map_tdef and

CNF map_2 TO Map_tdef

then { RG p IS map 1; “ CR temp WITH (p.all) WHERE NOT

( ISIN p. argument map_dom (map_2) );

UN temp map_2 }

else undefined

map_compose ( map_l ,map_2 ) = CNF map_l TO Map_tdef and

CNF map_2 TO Map_tdef and

SB map-rng (map_l) map_dom (map_2)

then { RG p_l IS map_l ; RG p_2 IS map_2;

CR WITH ( p_l . a rgument , p_2. result ) WHERE ( p_l. result = p_2. argument ) }

else undefined

map_union ( map_l ,map_2 ) = CNF map_l TO Map_tdef and

CNF map_2 TO Map_tdef and

NN ( IN map_dom—

(map_l") map_dom (map_2) ) then UN map 1 map_2

else undefTned

- 44 -
4 . 3. 2. 4 Trees

An abstract VDM tree, t= (d_l , . . . ,d_n) , from the domain

D :: D_l...D_n is represented by the p-set

[ [d_l@branch, D_l@doma in] @# . . . ].

Again, for type checking purposes, a tree template is

defined as

TMP Tr ee_tdef = [ [d@branch ,D@domain] @#. . .WHERE ISIN d D]

.

There are only two different operations to be described

for trees: the construction of a new tree from the domain D,

mk-D ( d

1 , . . . ,d_n) , and the selection of a component, s-D i.

function

if

tree_select ion ( tree , domain) = CNF tree TO Tree_tdef and

CS (domain) and CD (domain) = 1 then { RG b IS tree; RG d IS domain

CR WITH ( b. branch ) WHERE ( b. domain = d ) }

else undefined

t

function tree_make ( d_l i st , D_1 i st) = if CNF d list TO Tpl tdef and

CNF D_list TO Tpl_tdef and

tpl-len (d_list) = tpl_len (D_list)

then { RG d IS d_list; RG D IS D_list;

CR WITH (branch : =d .component , domain:=

D. component) WHERE (d. index = D. index) } else undefined

4. 3. 2.

5

Functions

The VDM sets which can be represented on any limited,

real-world computer always have to be finite. In the same

way, all specified domains have to be limited as well, even

if they are defined recursively (i.e. an upper bound can be

placed on the depth of any recursion). This, however, means

that all function domains are also finite. Therefore we can

represent all abstract VDM functions by abstract maps. There

is, thus, no explicit need for an extra function

interpretation besides the presented interpretation for maps

in the VDM interpreter. In order to make the interpretations

simpler, we will, however, represent all semantic functions

by procedures and (PSP) functions as described in subsection

4.2.2. The only function operation, the application to its

arguments, is represented by the function or procedure

execution in the VDM interpreter.

- 45 -
4. 4 USE OF THE INTERPRETABLE SPECIFICATIONS

4.4.1 SPECIFYING AN OBJECT SYSTEM'S SEMANTICS

The interpr etable specifications as described in the

preceding sections can be used in a similar way as the data

model specifications in the data model processor [4,5] to

define an object system's semantics formally. The metalanguage to be used, however, will be VDM's Meta IV rather

than PSN and the original PSP commands.

First, all semantic object types are defined in the

semantic domains specifications of the formal model. Then,

each semantic domain definition may be refined by an

additional is-well-formed predicate in the static

consistency constraints section of the semantic model.

Auxiliary functions may be defined for and applied in any of

the predicate definitions.

Next, the global state has to be defined,

of the formal semantic model, a global state var

be declared for each object which might be aff

the interpretation of any of the operations to b

In addition, global state constants might be def

objects which are accessible from at least one

but which will not be altered by any of them,

all global variables and constants have, in any

defined in, or to be derived from the semantic d

In this part

iable has to

ected during

e specified,

ined for all

operation

,

The types of

case, to be

oma ins

.

Initializing the global state variables and constants

is a task comparable to the 'data model populator' role in

the DMP. An initial value has to be assigned to all

variables and constants. All the values have to conform to

both the corresponding structure descriptions in the

semantic domains, and, possibly, to their static consistency

constraints

.

In the second major part of the formal semantic model,

first the operations' names and operand types have to be

declared in the syntactic domains part of the model. All

operand types are either defined in the semantic domains, or

their definitions have to be given here. (The most important

example for such operand type definitions are the expression

derivation rules to be specified in the syntactic domains.)

Then, for each operation a dynamic consistency

predicate may be defined. It restricts the set of all

possible operands (as specified in the syntactic domains) to

the only well formed ones for, possibly, each single

operation.

- 46 -
Finally, the semantic functions are defined which

describe the semantics for all operations. For each

operation to be specified the corresponding semantic

interpretation function takes this operation's arguments,

and defines its semantics in terms of 'manipulating' side

effects to some global state variables. The semantic

functions which denote expression evaluations do not

manipulate any global state variables. They describe (in an

abstract way) the derivation of a result value from the

global variables and/or constants. Auxiliary functions may

be used in any semantic function definition.

4.4.2 ANALYZING THE INTERPRETABLE SPECIFICATIONS

Once a given object system is defined formally in terms

of the (slightly restricted) VDM meta-language, we are now

able to transform the semantic model into a semantically

equivalent PSN/PSP representation as described in sections

4.2 and 4.3. Then, the formal model can be analyzed

automatically on the DMP.

First, some consistency and completeness checks could

be applied:

- In the semantic domains, all object names (left-hand

sides of the defining equations) have to be defined

uniquely. For all object names used in the defining

expressions (right-hand sides of the defining

equations), a defining rule has to exist in the

semantic domains.

- Similarly, in the syntactic domains all operation

names have to be defined uniquely. Also, each

defining expression may be based on already defined

semantic domain objects only or on other abstract

syntactic objects specified in the syntactic domains.

- There may be one Boolean ' is-well-formed ' function

specified for each semantic or syntactic domain

object (i.e. for each semantic object or operation).

All these predicates can possibly be checked for

consistency, i.e. not to be so 'restrictive' that no

single semantic or syntactic domain object can make

them true .

- Most important, it should be checked that each actual

variable or constant in the global state conforms to

all structural restrictions as imposed by the

corresponding semantic domain definitions. In

addition, the corresponding static consistency

- 47 -
predicate should yield true if applied to each of

them. The consistency checks should be repeated for

each global variable after any manipulation during a semantic function interpretation. In case a global

value is 'incorrect' by that means, appropriate

exception handling procedures should be triggered (at

least a message to the user of the interpreting

system)

- For each

domains, th

function i formal mode

take pa ram

the syntac

should hav

effects on

possible k

one semanti

the correc

state vari

appropriate

operation specified in the syntactic

ere should be exactly one interpretation

n the elaboration functions' part of the

1. Each of these functions should only

eters of the correct types as specified in

tic domains. Interpretation functions

e no result values but rather have sidesome global state variables. For each

ind of expression there should be exactly

c evaluation function which, again, takes

t arguments, does not change any global

able, and results in a value of the

type.

All mentioned restrictions could be checked

automatically by the formal semantics interpreting system.

Finally, a formal specification of an object system's

semantics could be verified against its intended, and

usually informal initial semantic description (even if this

is not much more than some rather 'vague' ideas about the

system). Any specified operation can be simulated based on

its respective VDM semantic function specification. First,

the correctness of its parameters is assured, and then the

function is interpreted on the PSP. The semantic meaning of

the operation is defined by the global state changes

resulting from the interpretation of the corresponding

semantic function. If these changes do not reflect the

initial understanding of the operation's semantics, the

specification has to be changed and interpreted again in an

iterative process.

- 48 -
5. CONCLUSIONS

This paper introduces two different approaches to

database model semantics specification. In chapter 2, both

of them are applied to a subset of the Relational Data

Model. A comparison of their main advantages and

disadvantages leads to two alternative approaches to

integration of both methods.

In chapter 3, the Vienna Development Method is applied

to specify the semantics of the Positional Set Notation and

the corresponding Positional Set Processor commands of the

Data Model Processor. It is shown that Meta IV, the metalanguage of VDM is powerful enough to express all semantic

properties of the most important constructs of the data

model interpreter's specification language in a completely

formal way.

VDM is demonstrated to be an appropriate tool to model

all three semantic aspects of PSN and the PSP commands:

structures, operations, and both kinds of possible

constraints. The result is a formal model which is fairly

simple and straightforward for both the structure and

constraint descriptions. The functional model for the

operations is slightly more complex, especially for some of

the PSP commands. (See, for instance, the abstract syntax

and elaboration function for the 'create' command.) This may

be interpreted as a measure for complexity of the operations

which may, thus, not be so easily understood by novice users

of the DMP. However, breaking the complex semantic functions

down into several simpler (auxiliary) ones should help to

guide the user's understanding.

For any semantic specification method, th

definition of its meta-language tools is its cruc

In the DMP framework, the meta-language tools are

PSN and the PSP commands. So, the precise and

semantic model provides the semantic basis for

model specification language of the DMP

theoretically sound and widely accepted approach

semantic specification.

e semantic

ial basis,

given by

formal VDM

the data

using a to formal

In chapte

specification c meta-language

,

immediately on

major advantag

understandable

r 4, it is shown how a formal semantic

an be written in an abstract and high-level

and still be analyzed and evaluated

a software system. This approach combines the

es of both VDM and the PSP into a fairly

and powerful prototyping system.

- 49 -
The scope of the abstract semantic specification

interpreter is centered around but not limited to database

models. Data model semantics can be defined in an abstract

and representation-free meta-language, and then be emulated

on the data model processor. By using the integrated

methods, single database management systems' user

interfaces, or particular database applications with

corresponding transaction specifications can also be defined

at a high level of abstraction, and then be tested and

analyzed automatically at a rather early stage of their

design.

ACKNOWLEDGEMENTS

The help from Drs. D.R. Deutsch, L. Gallagher, W.T.

Hardgrave, M. Koll

,

J.W. Schmidt, and M s. S.B. Salazar in

supporting and

acknowledged

rev iewing this work i s g rateful ly

- 50 -
6 REFERENCES

[1] D. Bjjrfrner, C.B. Jones (Eds.): 'The Vienna Development

Method: The Meta Language', Lecture Notes in Computer

Science, no. 61, Springer Verlag, Berlin Heidelberg New

York, 1978.

[2] M.L. Brodie, J.W. Schmidt (Eds.): 'Final Report of the

Relational Database Task Group' , ANSI/X3/SPARC/DBSSG,

ACM SIGMOD RECORD, vol. 12, no. 4, July 1982.

[3] W.T. Hardgrave: 'Positional Set Notation', Advances in

Database Management, vol. 2, Heyden and Son, New York,

to appear 1983.

[4] W.T. Hardgrave, S.B. Salazar : 'The Positional Set

Processor: A Tool for Data Modeling', NBSIR 81-2302,

National Bureau of Standards, Washington, D.C., 1981.

[5] M. Roll, W.T. Hardgrave, S.B. Salazar: 'Data Model

Processing', Proc. National Computer Conference,

Houston, Texas, June 1982.

[6]

M. Roll, W.T. Hardgrave: 'Data Model Processor User's

Manual', Institute for Computer Science and Technology,

Center for Programming Science and Technology, Data

Management and Programming Language Division, National

Bureau of Standards, Washington, D.C., September 1981.

[7]

W. Lamersdorf, J.W. Schmidt: 'Specification of

Pascal/R' , Berichte Nr. 73 and 74, Fachbereich

Informatik, Universitat Hamburg, West-Germany

,

1980.

[ 8 ] E.J. Neuhold, T. Olnhoff : Method ( VDM) and its Use for

Relational Data Base System

Proc. IF I P 80, World

Tokyo/Melbourne, Oct. 1980, pp

'The Vienna

the Specifica

' , T. Laving

Computer

.3-16.

Development

tion of a ton (Ed.) : Congress,

[9] J.W. Schmidt, W. Lamersdorf:

Definition and its Formaliza

Fachbereich Informatik, Un

Germany, March 1982 - also ava

'Relational Datamodel: A

tion', Bericht Nr. 88,

iversitat Hamburg, West

il able in [ 2 ]

- 51 -
NBS-114A (rev. 2 >ac) U.S. DEPT. OF COMM.

BIBLIOGRAPHIC DATA

SHEET (See instructions)

1. PUBLICATION OR

REPORT NO.

NBSIR 83-2740

2. Performing Organ. Report Nc Hamburg-University

DBPL-Memo 111-82

3. Publication Date July 1983

4. TITLE AND SUBTITLE

Specification and Interpretation of Data Model Semantics: An Integration of Two

Approaches

5. AUTHOR(S)

Winfried Lamersdorf

6. PERFORMING ORGANIZATION (If joint or other then NBS. see instructions)

NATIONAL BUREAU OF STANDARDS

DEPARTMENT OF COMMERCE

WASHINGTON, D.C. 20234

7. Contraci/Grani No.

I. Type of Report & Period Covered

9. SPONSORING ORGANIZATION NAME AND COMPLETE ADDRESS (Street. City, State, ZIP)

10. SUPPLEMENTARY NOTES

[ Document describes a computer program; SF-185, FIPS Software Summary, is attached.

11. ABSTRACT (A 200-word or less foctual summary of most significant information. If document includes a significant

bi bl logrophy or literature survey, mention it here)

Two different approaches to database model description and evaluation are presented,

compared, and integrated: a formal semantic specification method as originally

developed for programming languages, and a computer-based data model processor to be

used as a rapid prototyping system. Both ways to specify database model semantics are applied to a common example.

Two alternatives to combine the advantages of both methods are analyzed in detail.

First, it is shown how the semantics of the data model processor can be precisely

described in terms of the formal semantic specification method. Then, it is demonstrated how the abstract meta-language of the specification method can be mapped to

the executable commands of the data model processor. Thus, database semantics can both be specified in an abstract and high-level way and still be analyzed and

evaluated automatically.

12. KEY WORDS (Six to twelve entries; alphabetical order; capitalize only proper names; and separate key words by semicolons)

databases; data models; data model processing; data model prototyping; data model

semantics; denotational semantics; formal semantic specification; relational database;

relational data model: semantic model interpreter

13. AVAILABILITY

|X I Unlimited

|

\ For Official Distribution. Do Not Release to NTIS

1

| Order From Superintendent of Documents, U.S. Government Printing Office, Washington, D.C.

‘ 20402. 22 Order From National Technical Information Service (NTIS), Springfield, VA. 22161

14. NO. OF

PRINTED PAGES

56

15. Price

$ 10.00

USCOMM-DC 6043-P80