Fen-An Axiomatic Basis for Program Semantics

A formal system is presented which abstracts
the notions of data item, function, and relation. 
 It is argued that the system is more suitable than set
theory (or its derivatives) for the concise and 
accurate description of program semantics.  It is shown
how the system can be used to build composite 
data types out of simper ones with the operations of rowing,
structuring, and uniting.  It is also demonstrated 
that completely new primitive types can be introduced
into languages through the mechanism of singleton 
data types.  Both deterministic and nondeterministic
functions are shown to be definable in the system. 
 It is described how the local environment can be modeled
as a data item and how imperative statements 
can be considered functions on the environment.  The
nature of recursive functions is briefly discussed, 
and a technique is presented by which they can be introduced
into the system.  The technique is contrasted 
with the use of the paradoxical combinator, Y.  The
questions of local and global environments and of 
various modes of function calling and parameter passing
are touched upon. The theory is applied to the 
proof of several elementary theorems concerning the semantics
of the assignment, conditional, and iterative 
statements.  An appendix is included which presents in
detail the formal system governing webs and fen, 
the abstractions used informally in the body of the paper.

CACM August, 1973

MacLennan, B. J.

semantics, formal systems, lambda-calculus, extensible
languages, data types, modes, axioms, correctness, 
formal language definition, formal description, data structures,
description languages, models of computation

4.22 5.21 5.24 5.26

CA730804 JB January 23, 1978  11:01 AM

1469	4	2470
1486	4	2470
1491	4	2470
1781	4	2470
2021	4	2470
2060	4	2470
2178	4	2470
2222	4	2470
2227	4	2470
2294	4	2470
2315	4	2470
2326	4	2470
2326	4	2470
2470	4	2470
2470	4	2470
2470	4	2470
2470	4	2470
2684	4	2470
2732	4	2470
2865	4	2470
2896	4	2470
2943	4	2470
3014	4	2470
3044	4	2470
3068	4	2470
3077	4	2470
3124	4	2470
3143	4	2470
1303	5	2470
1469	5	2470
1834	5	2470
2264	5	2470
2470	5	2470
2470	5	2470
2470	5	2470