Relational semantics in an integrated system

This paper contains the description of a system for handling semantics of computer programs. The methodology used for the description of semantics is the relational semantics: — possibly incomplete — information about programs is represented by binary relations. For the description we use the language Automath in which logic, mathematics, syntax and semantics are integrated. Moreover, the correctness of texts written in Automath can be checked mechanically by a computer. We consider an ALGOL6O-like programming language. The axiomatic basis of it is kept small, but it is large enough to make the definition of many ALGOL constructs possible. In the basis are included assignment, binary selection, concatenation, block structures and recursive parameterless procedures. For these basic constructs semantics is presented, and some examples are given how new program constructs can be described in terms of these basic ones.