Skip to main content
main-content

Über dieses Buch

This work presents a purely classical first-order logical approach to the field of study in theoretical computer science sometimes referred to as the theory of programs, or programming theory. This field essentially attempts to provide a precise mathematical basis for the common activities involved in reasoning about computer programs and programming languages, and it also attempts to find practical applications in the areas of program specification, verification and programming language design. Many different approaches with different mathematical frameworks have been proposed as a basis for programming theory. They differ in the mathe­ matical machinery they use to define and investigate programs and program properties and they also differ in the concepts they deal with to understand the programming paradigm. Different approaches use different tools and viewpoints to characterize the data environment of programs. Most of the approaches are related to mathe­ matical logic and they provide their own logic. These logics, however, are very eclectic since they use special entities to reflect a special world of programs, and also, they are usually incomparable with each other. This Babel's mess irritated us and we decided to peel off the eclectic com­ ponents and try to answer all the questions by using classical first-order logic.

Inhaltsverzeichnis

Frontmatter

Introduction

Introduction

Abstract
Programming Theory. The field of study dealing with programs and programming languages in theoretical computer science is usually referred to as programming theory, or the theory of programs. This field essentially deals with the formal investigation of the world of programs, including characterization of programs, description of program properties and checking whether a given program satisfies certain properties. In order to support this investigation, programming theory attempts essentially to provide an appropriate mathematical foundation. This theory also attempts to provide appropriate, theoretically well based methods and tools to support practical applications, e.g. in the field of program specification and verification and also in program design and in programming language development.
Tamás Gergely, László Úry

Mathematical Background

Frontmatter

Chapter 1. Logic and Model Theory

Abstract
The programming theory to be developed in this work is based on first-order classical logic. In order to follow this development we expect the reader to be familiar with the elements of classical mathematical logic and with the basic notions of (naive) set theory that we accept as our starting point.
Tamás Gergely, László Úry

Chapter 2. Inductive Definability

Abstract
Developing a logic-based theory of programming, the chief concern is the logical definition of the main notions connected with programming. In order to deal successfully with this concern an appropriate definability theory has to be used . In our program-theoretic investigation, inductive definability will play a significant role in the establishment of certain relationship between models, computability and programs. In the present chapter we list the main concepts of this theory in accordance with Aczel [1977], Barwise [1975] and Moschovakis [1974].
Tamás Gergely, László Úry

Computability

Frontmatter

Chapter 3. Introduction to Part I

Abstract
Our main objective in this part is the development of a theory based on classical first-order logic which can serve as the foundation for a logic-based programming theory. Namely, this theory should deal with programs and with their logically meaningful semantics, and should also provide purely logical tools to extend programming languages with new computation devices or data structures. This theory should also be appropriate to investigate the programming languages for example from the viewpoint of their computational power, and to provide them with a sharp logical characterization.
Tamás Gergely, László Úry

Chapter 4. Main Properties of Program Schemas

Abstract
In this chapter we introduce a basic programming language by defining its syntax and semantics. The syntax is defined as a set of program schemas constructed with a given set of program constructs by using the terms and the open formulas of a fixed alphabet (similarity type). This ensures that the function and relation symbols from which the terms and formulas are built up are included in the program schemas . We take the traditional view of a programming language as syntactic: in this case the syntax is the set of program schemas of the given similarity type.
Tamás Gergely, László Úry

5. Extension of Program Schemas

Abstract
The basic programming language introduced so far should be considered as the minimal language in our investigation. It is sufficient for a programming logic to establish only some negative results by showing that something fails even in the case of this minimal language. However, for a programming logic we need a programming language which is universal in the computational sense, that is, in which any algorithm can be represented by an appropriate program. As we shall see in Chapter 7, the language r P σ is not such . Therefore, we need either another programming language or a special device to extend the language r P σ appropriately. We choose the latter approach and introduce a logical tool which ensures the required extension in a purely logical way.
Tamás Gergely, László Úry

Chapter 6. Program Schemas with Stacks

Abstract
We have seen so far how the programming language r P σ can be augmented with new computational devices by the use of extension. From the viewpoint of computational power, as in Chapter 5, it is sufficient to augment the language r P σ with stacks. Therefore, for the theory it is sufficient to use the stack extension of r P σ . However, the way the extension has been made does not limit the number of new devi ces usable in the programs. For example, according to Definition (5.1) infinitely many counters or stacks are allowed in the appropriate extension of r P σ .
Tamás Gergely, László Úry

Chapter 7. Computability

Abstract
The theory of computability deals with the formal characterization of the “effectively Computable” functions and relations. Different pieces of machinery, such as recursive functions, register machines, and normal algorithms, have been proposed for this aim . Programming languages provide a new technique for the formalization of computability, and at the same time they make it possible to deal with the characterization of the computable functions and relations adequately within the programming theory.
Tamás Gergely, László Úry

Chapter 8. On Inductive Definability of 1- and 2- Computable Relations

Abstract
Up to now we have developed different logical tools in order to describe and investigate programming languages. However, from the logical viewpoint the programming languages remained external with respect to the logic, by the use of which the investigation took place . This raises an interesting question. Is it possible to give purely logical objects, which are internal to logic and which play the same role as programs? This question can be paraphrased as follows: Could programming languages be characterized in a purely logical way?
Tamás Gergely, László Úry

Extended Dynamic Logics

Frontmatter

Chapter 9. Introduction to Part II

Abstract
The first significant steps in developing a unique logically based programming theory have been made in Part 1. These steps resulted in a computation theory in the scope of first-order classical logic. To accomplish the development of our programming theory we have to make efforts to develop appropriate tools with the same scope to deal with the characterization of the programming languages and programs provided as formal objects by the computation theory. Moreover these tools should allow the required characterization in accordance with our computation theory. Part II is devoted to accomplishing the required development programming theory, that is, it is devoted to the development of the second subfield of programming theory in harmony with the first subfield outlined in Part 1.
Tamás Gergely, László Úry

10. Description of Program Properties

Abstract
Having formally defined the notions of programs and their executions over the abstract models of computers it is an important question how programs can be characterized. The first possibility is to consider how the programs are built up , i.e. what programming constructs participate in their definitions and how. The number of cycles or the number of constructs built into one another can be determined. However, this type of characterization is purely syntactic, of course, and considers programs only as texts. But the essence of programs is hidden in their execution, which takes place in the data environment and is represented by the definition of semantics of programming languages. Therefore, the semantic characterization of programs is necessary to reflect the pragmatic essence and to answer the question of what a program does . For this characterization, appropriate properties concerning program execution should be selected. According to the computation theory developed in Part I, these properties should concern the computation states from which the computational paths are formed and also to the traces themselves. For example a property like “the program terminates” refers to the finiteness of computation paths and also to the existence of a “terminal” state. However, this tight connection of properties with computation states suggests another view. Namely, the semantic characterization of programs should start with the appropriate definition of the program semantics, i.e. either of the denotations or of the traces. Since we aim to develop the programming theory in the scope of classical first -order logic, this definition should be stated using appropriate logical tools. Having given the logical definition of semantics, the same language will be appropriate to characterize the denotations or the traces. However, before starting to realize our view, which prefers the definition of the semantics to that of the description of program properties, we give a rough survey of the main properties.
Tamás Gergely, László Úry

Chapter 11. Den-based Descriptive Languages

Abstract
Programs operate on their data environments. If we are interested in the change caused by the execution of a program in its environment then the input-output semantics, defined as a binary relation on data sequences, is suitable. A great variety of program properties is connected with the relational semantics, e.g. partial correctness, quasi-total correctness, pseudo-total correctness, etc.
Tamás Gergely, László Úry

Chapter 12. The Problem of Completeness

Abstract
Besides the description of program properties, programming logics are also expected to provide appropriate tools for proving the existence of these properties at concrete programs. Therefore, an appropriate calculus is required to permit the proof of formulas of the descriptive language. Moreover, we expect this calculus to be realizable in some intuitive sense , i.e. to correspond to our requirement of having an effective proof concept. Completeness of a descriptive language requires the recursive enumerability of the appropriate formulas. On the other hand, concerning the calculus, it is required to enumerate all the appropriate formulas.
Tamás Gergely, László Úry

13. Dynamic Logic Generated by Extension

Abstract
As we have seen, the σ-type dynamic logic and even its Floyd-Hoare sublanguage are incomplete. The efforts made in the previous chapter to make dynamic logic complete did not bring us pragmatically satisfactory results. Therefore, we now look for another way to obtain a pragmatically satisfactory complete dynamic logic. First of all we require that this way should allow us to preserve the classical notion of completeness and should also provide us with the expected dynamic logic in the scope of classical first-order logic. The latter requirement follows from our original aim to develop programming theory in this scope. Moreover, we also require to develop the dynamic logic in compliance with the computation theory developed in Part 1. In the present chapter we introduce the main logical tools which can be used to develop different programming logic as classical first-order languages. These tools are based on the notion of extension introduced in Chapter 5 and are used to augment the programming language r P σ with different computational devices.
Tamás Gergely, László Úry

14. Continuous Denotational Semantics

Abstract
The development of a programming logic in the scope of classical first -order logic is connected with making the formal notions, used to describe program properties, internal. This can be ensured by defining the definability of these notions in the logic in question. Here we show how dynamic logic can be developed in classical first-order logic by internalizing the denotation Den only. This internalization can be achieved by an appropriate axiomatization of reflexive and transitive closure. For the latter we introduce in Section 14.1 the so-called transitive extension and the corresponding extended language. This language will be appropriate to introduce two axiom systems Ind σ and Ind σ * . In this section it will also be shown how these axiom systems can be used to define the denotational semantics. In Section 14.2, by using the axiom systems Ind σ and Ind σ * we introduce the dynamic logic with continuous denotational semantics DL σ ns and that with strongly continuous denotational semantics DL σ ns* . The first one we also call non-standard dynamic logic. These logics realize our aim to define dynamic logic in the scope of classical first-order logic. Moreover, they preserve the classical notion of completeness, and we will show that they are compact and complete. Considering the Hoare calculus and its generalization we will show that these calculi are complete with respect to the continuous and the strongly continuous denotational semantics, respectively. These results at the same time provide a first-order characterization of the Hoare calculus and of its generalization.
Tamás Gergely, László Úry

Chapter 15. Definable Denotational Semantics

Abstract
In this chapter we show how an appropriate first-order language can be built up to describe the properties of rP σ 1 -programs. Here we also use the logical tools introduced in Chapter 13, and the method of the development of the required dynamic logics is similar to that used in the previous chapter. We have proved in Part I that rP σ 1 I for a one-sorted similarity type σ. Thus first we present a logic within which any fixed-point equation of the form R(X) ≡ φ(X, P) (φ ∈ Σ+(σ,R)) has a solution. Secondly, we show how the semantics of rP σ 1 can be defined, and using this definition we give an appropriate semantic function \( \hat \cdot :rD_\sigma ^1 \to Form_\delta \). Finally we give similar characterizations and completeness results to those in Chapter 14.
Tamás Gergely, László Úry

Temporal Characterization of Programs

Frontmatter

Chapter 16. Introduction to Part III

Abstract
As we have seen, dynamic logic is based on input-output relational semantics. The expressive power of this descriptive language permits us to define many different program properties, including those connected with the “history” of execution. In order to characterize program semantics in this language, a computer is modelled by the data environment of the programs, and computer functioning, which is just data manipulation, represented by change of data. However, this functioning goes on in time, namely in time moments which depend on the construction of the computer and are generated by the computer’s “inner clock”. In the programming theories considered so far , time has been considered only at the metalevel, not allowing us to refer to time in the object language, i.e. in the descriptive language. In order to make a more refined model of a computer we represent it with both data environment and “inner clock”. For the latter we have to provide tools for explicit time consideration.
Tamás Gergely, László Úry

Chapter 17. Temporal Logic

Abstract
Temporal logic is based on modal logic which uses the standard two modalities □ and ◊ interpreted as “necessity” and “possibility”. Kripke [1963] elaborated a formal semantics for modal logic. Prior [1957] first suggested a temporal interpretation of the modalities, “always” for □ and “sometimes” for ◊. Following von Wright [1965] a new modality, the “next” time operator, denoted by o, was added to □ and ◊, and the temporal logic obtained was investigated in Prior [1967]. Prior’s temporal logic contains operators for referring to both past and future. From Prior’s work different temporal logics have been developed with different temporal operators. These logics realize different views of time such as the linear or branching time view; for example Pnueli [1977] adapted Prior’s temporal logic with the linear time view to describe program properties following an idea of Burstall [1974]. This temporal logic uses the future fragment only and it contains the temporal operators “sometimes” , “always” and “next”. The time view is linear and semantically represented by natural numbers.
Tamás Gergely, László Úry

Chapter 18. Temporal Logical Description of Program Properties

Abstract
Now let us see how the σ-type temporal logic ML σ can be used to reason about programs and how program properties can be described. The temporal logic of programs will not mention programs explicitly, but it will operate on the computational paths realizing the execution of a program. This is one of the fundamental differences between the viewpoints of temporal logic and dynamic logic, since the latter does not directly operate on the computation but only on their input and output elements, yet it can directly refer to many programs.
Tamás Gergely, László Úry

Chapter 19. Is Temporal Logic Expressible in Dynamic Logic?

Abstract
As is well known, temporal logic can be defined in dynamic logic (ef. Harel [1984]) in the propositional case. This fact was used by Meyer [1980] when he stated that temporal logic is uninteresting from a scientific point of view.
Tamás Gergely, László Úry

Chapter 20. Is Dynamic Logic Expressible in Temporal Logic?

Abstract
In this chapter we complete the investigation of the interrelation of temporal and dynamic logics by showing that they are incomparable. For this we have to prove that temporal logic cannot define dynamic logic.
Tamás Gergely, László Úry

Chapter 21. The Case of Enumerable Models

Abstract
Countable models play a significant role in programming theory from a pragmatic point of view, since programs are executed in countable models (e.g. on integers). Therefore it is interesting to study the relationship between the two logics in question with respect to the enumerable models. One may expect either that the results of the above chapters are inherited or that dynamic logic is more powerful. However, as we shall see, neither of these expectations is borne out. In fact, temporal logic is of greater expressive power. Before we attempt to investigate their comparative expressiveness we consider an important semantic construction.
Tamás Gergely, László Úry

22. Temporal Axiomatization of Program Verification Methods

Abstract
Temporal logic as a descriptive language allows us to formalize our expectations about the time during which a program runs. Since different program verification methods differ in their view of how they consider program execution we can characterize them axiomatically by using temporal logic. In this chapter we give the required characterization for the Floyd-Hoare method, for the method of intermittent assertions introduced by Burstall [1974] and subsequently propagated by Manna, Waldinger [1978], and for the method introduced by Pnueli [1977] . Sain [1986, 1991] study in detail the axiomatic characterization and interrelation of these program verification methods by means of different induction axiom schemas in the scope of her non-standard dynamic logic.
Tamás Gergely, László Úry

Programming Logic with Explicit Time

Frontmatter

23. Introduction to Part IV

Abstract
Temporal logic investigated in the previous part represents program execution by taking trace semantics into account. The traces are represented by the changes of local variables. The computational paths are realized according to the time structure of the temporal logic. Note that for a given program p the set Trace A . 〚p〛 of traces in a given model A, when the input is fixed, forms a tree. Depending on the time structure this tree can be represented in different ways. We considered a time structure which allowed us to represent Trace A . 〚p〛 as the set of all possible paths from the root (given input) to the leaves (outputs) of the tree. It is important to emphasize that temporal logic uses a fixed linear time structure built into the Kripke models.
Tamás Gergely, László Úry

Chapter 24. Time Logic

Abstract
In the previous part, temporal logic was introduced to describe program properties. For this logic, traditional modal logic with a temporal interpretation of the modalities was augmented with two kinds of variables, global and local. The use of local variables allows us to describe and characterize the program execution. However, as observed in Wolper [1983] there are some properties, usually referring to counting events, which are not expressible in the considered version of temporal logic where quantification over local variables is not allowed. Moreover, temporal logic does not allow us to refer explicitly to time moments or intervals. The result is that temporal logic handles at once all the computational paths starting from the same input.
Tamás Gergely, László Úry

Chapter 25. Definability in Regular Time Theories

Abstract
In order to develop a flexible and powerful programming theory an appropriate formal theory is required which permits us to define all the objects and notions necessary for the theoretical characterization of programs and programming languages in a uniform way. The required formal theory can be ensured by an appropriate definition theory which allows the effective usage of fixed-point equations. Effectivity means that the equations can be solved in finitely many steps. Moreover, in programming theory it is important to work with explicitly defined notions and objects. Therefore we expect that the implicit definitions given in the form of fixed-point equations can be turned into explicit ones. Thus arises the requirement that the solutions of fixed-point equations should be definable.
Tamás Gergely, László Úry

Chapter 26. Expressive Power of Time Logic

Abstract
With the time logic introduced in the previous chapter we have three languages for supporting programming theory. How are these languages related to each other? We show in the present chapter that time logic is the most powerful in expressive power. This will be shown by embedding the other two languages, i.e. temporal and dynamic logics, into time logic.
Tamás Gergely, László Úry

Backmatter

Weitere Informationen