Fen—an axiomatic basis for program semantics

ABSTRACT

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 simpler 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.

REFERENCES

• 1: Bekid, H., and Walk, K. Formalization of storage properties. In Symposium on Semantics AIgorithmie Languages. Erwin Engeler (Ed.), Springer Lecture Note Series, Springer-Verlag, Heidelberg, 1971, p. 39.
• 2: BOhm, C. The CUCH as a formal and descriptive language. In Formal Language Description Languages./or Computer Programmhlg T.B. Steel (Ed.), North-Holland, Amsterdam, 1966, pp. 198- 220.
• 3: J. M. Cadiou , Zohar Manna, Recursive definitions of partial functions and their computations, ACM SIGPLAN Notices, v.7 n.1, p.58-65, January 1972
• 4: Alonzo Church, The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics Studies), Princeton University Press, Princeton, NJ, 1985
• 5: Church, A. An unsolvable problem of elementary number theory. Am. J. .Math. 58 (1936), 345-363.
• 6: Curry, H. B., and Feys, R. Combinatory Logic, Vol 1. North- Holland, Amsterdam, 1958.
• 7: Dennis, J. B. Notes on the design of a common base language. Mimeographed notes prepared for Tutorial Syrup. on Semantic Models of Computation, Dec. 1971.
• 8: Peter Henderson, Derived semantics for some programming language constructs, Communications of the ACM, v.15 n.11, p.967-973, Nov. 1972 [doi>10.1145/355606.361880]
• 9: Hilbert, D., and Bernays, P. Grundlagen der Mathematik, Berlin, 1934 and 1939, Sec. 1.
• 10: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 11: Philippe Jorrand, Data types and extensible languages, ACM SIGPLAN Notices, v.6 n.12, p.75-83, December 1971
• 12: Donald M. Kaplan, Some Completeness Results in the Mathematical Theory of Computation, Journal of the ACM (JACM), v.15 n.1, p.124-134, Jan. 1968 [doi>10.1145/321439.321447]
• 13: Landin, P.J. The mechanical evaluation of expressions. Computer J. 6 (Jan. 1964), 308-320.
• 14: Landin, P.J. A formal description of ALGOL 60. In Formal Language Description Languages for Computer Programming. T. B. Steel (Ed.), North-Holland, Amsterdam, 1966, pp. 266-294.
• 15: P. J. Landin, Correspondence between ALGOL 60 and Church's Lambda-notation: part I, Communications of the ACM, v.8 n.2, p.89-101, Feb. 1965 [doi>10.1145/363744.363749]
• 16: P. J. Landin, The next 700 programming languages, Communications of the ACM, v.9 n.3, p.157-166, March 1966 [doi>10.1145/365230.365257]
• 17: John A. N. Lee, Computer Semantics: Studies of Algorithms Processors and Languages, Krieger Publishing Co., Inc., Melbourne, FL, 1978
• 18: Lucas, P., and Walk, K. On the formal description of PL/I. Annual Reviews t2{Automatic Programming 6, 3 (1969).
• 19: MacLennan, B. Semantic specification and machine independent compilation. Proc. ACM 10th Ann. Southeast Reg. Conf.,,June 1971 (mimeographed).
• 20: Zohar Manna , Stephen Ness , Jean Vuillemin, Inductive methods for proving properties of programs, ACM SIGACT News
• 21: James B. Morris, Jr. , Mark B. Wells, Generalized data structures in Madcap VI, ACM SIGPLAN Notices, v.6 n.2, February 1971 [doi>10.1145/1115880.1115895]
• 22: yon Neumann, J. Die Axiomatisierung der Mengenlehre. Math. Z. 27 (1928), 669-752.
• 23: yon Neumann, J. Line Axiomatisierung der Mengenlehre. J. reine angew. Math. 154 (1925), 219 240.
• 24: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 25: Scott, D. The lattice of flow diagrams. In Symposium on Semantics of Algorithmic Languages. Erwin Engeler (Ed.), Springer Lecture Note Series, Springer-Verlag, Heidelberg, 1971, pp. 311-366.
• 26: Scott, D. and Strachey, C. Toward a Mathematical Semantics Jbr Computer Languages. Oxford U. Computing Lab., Programming Research Group Tech. Mono. PRG-6.
• 27: Strachey, C. Towards a formal semantics. In Formal Language Description Languages for Computer Programming. T.B. Steel (Ed.), North-Holland, Amsterdam, 1966, pp. 198 220.
• 28: van Wijngaarden, et al. Report on the algorithmic language ALGOL 68. Numerische Mathematik 14 (1969), 79-218. Offprint available from Dept. AL68-D, ACM Headquarters, New York.
• 29: Wirth, N. The programming language Pascal. Acta blformatica 1, 1 (1971), 35-63.
• 30: Wulf, W.A., et al. Bliss Reference Manual. Dept. of Computer Sci. document, Carnegie-Mellon U., Pittsburgh, Pa., 1970.

INDEX TERMS

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