Advertisement

A formal definition of a PL/I subset

  • H. Bekić
  • D. Bjørner
  • W. Henhapl
  • C. B. Jones
  • P. Lucas
Selected Papers Language Definition
Part of the Lecture Notes in Computer Science book series (LNCS, volume 177)

Abstract

This report provides a formal definition of large portions of the ECMA/ANSI proposed Standard PL/I language. The metalanguage used is described in the style of the "Mathematical Semantics". That is, the definition of PL/I is given by generating a function from a source program. A commentary is also provided to cover the less clear parts of the chosen model. For the convenience of the reader who wishes to have the commentary side by side with the formulae, the report is divided into two parts: Part I contains the description of the notation, the commentary and a cross-reference; Part II contains all the formulae.

Keywords

Context Condition Abstract Syntax Concrete Syntax Type Clause Vary String 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Abbreviations

aa

activation identifiers

abs

absolute

act

action

addr

address

ag

aggregate

aid

activation identifier

alloc

allocate

approx

approximate

arg

argument

arith

arithmetic

ass

assign, assignment

atm

atomic

augm

augment[ed.]

auto

automatic

bi

builtin

bif

builtin function

bin

binary

bl[s]

block[s]

bool

boolean

boe

block on-establishment

bp

bound-pair

bp1

bound-pair list

bs

base

c

cond-pref-set,context

cat

concatenate

cbif

condition built-in function

ccn

comp-cond-nm

c-nm

non-io-cond-nm or io-cond

ceil

ceiling

char

character

cl

class

clng

closing

cmp

composite

cn

cond-nm

comp

computational, component (the latter used more often!)

compar

compare

cond

condition

conn

connected

const

constant

constr

construct

cont

content

conv

conversion, convert

cprefs

cond-pref-set

cpv

cond-pv

ct1

control

ctld

controlled

cur

current

dcl

declaration

dcls

declaration set

dd

data-description

dec

decimal

def

defined

der

derived

descr[s]

descriptor[s]

dft

default

digitl

digit list

dim

dimension

distr[ib]

distributive

div

divide

dsgn

designator

dtp

data-type

ebp

evaluated bound-pair

edd

evaluated data description

el

element, elementary

elem

element

enab

enabled

env

environment

eq

equal

eu

executable-unit

evd

evaluated

eval

evaluate

eval-1

eval-to-left-value

ex-unit

executable-unit

expr

expression

ext

external

fact

factor

fct

function

f

field

fix

fixed

flt

float

fofl

fixed overflow

fuid

unique file identifier

ge

greater or equal

gen

generate

grp

group

gt

greater

hbound

high bound

id[s]

identifier[s]

im

immediate

impl

implementation

indep

independent

indices

set of index lists

indl

list of indices

inf

infix, information

init

initial, initialize

init-wh-do

DO statement with init and while

int

internal

int

interpret(in fn names)

intg

integer

io

input-output

ioc

io-cond

iter

iteractive, iteration

l

list

l-

location

lab

label

lb

lower bound

lbound

low bound

le

less than or equal

len

length

loc[s]

location[s]

locr

locator

loe[r]

local on-establishment [by reference]

lt

less than

l-to-r

left to right

max

maximum

maxl

maximum length

min

minimum

mod

modulo

mult

multiply

ne

not equal

nm[s]

name[s]

nmd

named

nod

number-of-digits

num

number,numeric

obs

objects

ofl

overflow

onsource

onsource location

op

operator

opng

opening

opt[s]

option[s]

ou

on-unit

parm[s]

parameter[s]

pdd

parameter data descriptor

pos

position

pos-cond-nm

positive-condition-name

prec

precision

pref[s]

prefix[s]

proc

procedure

prog

program

prom

promote

prop

proper

ps

proper statement

ptr

pointer

pv

pseudo variable

qual

qualifier

r

right

rec

recursive

recity

recursivity

ref

reference

rel

relevant

rep

representation

res

result

ret

return

ret-descr

returns-descriptor

rev

revert

sc

scalar

sdd

statically determined data description

scomp

static computational

sdtp

static data description

sect

section

sels

selector set

sentry

static entry data description

sig

signal

snap

SNAP or nil

snms

statement names

snom comp

static non-computational-

source

onsource-char-str-val

spec

specification

st[s]

statement[s]

step-do

DO statement with TO

stg

storage

str

string

strg

string range

struct

structure

strz

stringsize

subjs

subjects

subr

subroutine

subrg

subscript range

subscr

subscript

substr

substring

subt

subtract

t

text

targ

target

term

terminal

tp

type

truth

truth (truth value)

ub

upper bound

udf

undefined

ufl

underflow

uid

unique identifier

unal

un-aligned

v

value

val

value

var

variable

varity

variability

vary

variability

vr

value reference

wh

while

zdiv

zerodivide

1-loc

level-one location

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    ECMA.TC10/ANSI.X3J1 PL/I BASIS/1–11 European Computer Manufacturers Association Feb. 1974, 346 p.Google Scholar
  2. [2]
    K. Walk, K. Alber, M. Fleck, H. Goldmann, P. Lauer, E. Moser, P. Oliva, H. Stigleitner, G. Zeisel Abstract Syntax and Interpretation of PL/I (ULD Version III) Techn. Report TR 25.098, IBM Lab. Vienna, Apr. 1969.Google Scholar
  3. [3]
    P. Lucas On Program Correctness and the Stepwise Development of Implementations Proceedings of the Congress on Theoretical Informatics, Pisa, March 1973, pp.219–251.Google Scholar
  4. [4]
    C. D. Allen, D. N. Chapman, C. B. Jones A Formal Definition of ALGOL 60 Techn. Report TR 12.105, IBM UK Labs Ltd., Aug. 1972, 197 p.Google Scholar
  5. [5]
    D. Scott, C. Strachey Toward a Mathematical Semantics for Computer Languages Techn. Monograph PRG-6, Oxford Univ. Computing Lab. Aug. 1971, 42 p.Google Scholar
  6. [6]
    H. Bekić Semantics of Parallel Programs Techn. Report, IBM Lab. Vienna (forthcoming)Google Scholar
  7. [7]
    P. J. Landin The Mechanical Evaluation of Expressions The Computer Journal, Vol.6 (1964) No.4; pp.308–320.zbMATHGoogle Scholar
  8. [8]
    H. Bekić, K. Walk Formalization of Storage Properties Symposium on Semantics of Algorithmic Languages Springer Lecture Notes in Mathematics, No. 188 (1970), p.28–61.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • H. Bekić
    • 1
  • D. Bjørner
    • 1
  • W. Henhapl
    • 1
  • C. B. Jones
    • 1
  • P. Lucas
    • 1
  1. 1.IBM Laboratory ViennaAustria

Personalised recommendations