Enriched Languages

Peter Baumann

Institut fur Informatik der Universitat Zurich
Winterthurerstr. 190, 8057 Zurich, Switzerland

Email: bauma[email protected], Tel: ++41 1 257 45 79, Fax: ++41 1 363 00 35

Keywords: formal approaches, natural semantics, program verification

1 Introduction

Programmers are often faced with the problem of working in two languages: a specification language and a programming language. This is especially true when program development starts with a formal specification written in a language such as Z [BN+92] and ends with an imperative program. Over the years it has become clear that post facto program verification is not a practical approach. Therefore, it is well recognized that a sound and yet practical approach to developing imperative programs from formal specifications is needed. The main goal is a unified framework in which specification assertions and executable statements can be combined smoothly.

The purpose of this paper is to present a very general approach how to enrich imperative programming languages in the direction of wide spectrum languages. The key idea is to incorporate specification assertions into programming languages by allowing predicates on pairs of states to appear wherever a statement could appear. For example, a predicate x < x in Z1

specifies an operation that decreases the value of the variable x . We regard it as a syntactically correct statement, although it is not executable. In the same way, while x >= 5 do (x < x) is
regarded as syntactically correct and we will give it a formal semantics in a natural semantics style. Intuitively, it describes a computation that decreases x until it is less then 5. Although it is in some sense more concrete than the statement x >= 5 ) x < x , it is still not executable
and can be further refined to while x >= 5 do x := x ? 1. This shows the general pattern of our approach. Starting with a specification, program development proceeds by fading out specification assertions and fading in executable statements until there are no more specification assertions. The point is that all statements belong to one language, which is given a formal semantics. This allows expressing precisely the relationship between the different statements.

The semantic basis of the method is natural semantics which allows omitting restrictions on the applicability of the method in case of interference. In contrast, aliasing prevents the use of many methods [Heh93, Mor88, Rey81]. Natural semantics are one of the very few formal semantics that are effectively used today to describe real world programming languages [MTH90]. Our approach of extending programming languages towards wide spectrum languages makes heavy use of the ability to express all constructs of the enlarged language in natural semantics.

1In Z, x denotes the value of x after the operation.