Early references to the project

Utworzono: poniedziałek, 24 grudzień 2018 12:55

Poprawiono: sobota, 23 styczeń 2021 17:53

Odsłony: 10301

As has been already mentioned on the site What is this project about, the current project Denotational Engineering is a follower of a project MetaSoft developed in the years 1970-1996. The present site provides links to full texts of some of my historical papers developed within MetaSoft. This selection is far from complete, but hopefully, it will be successively completed in the future. With each title, I attach on the site the original abstract of the paper. The ordering is chronological.

Andrzej Blikle, Equational languages, Information and Control 21, (1972), pp. 134-147

This paper deals with equations whose solutions are vectors of languages. Formally, solutions of equations are fix points of vectorial functions on languages. On the other hand equations (and sets of equations) can be considered as grammars. Three main groups of problems are dealt with: (1) solvability of equations in a lattice of languages, (2) relationship between types of functions used in equations and properties of languages defined by them, (3) applications to the theory of Context-free and regular languages.

Andrzej Blikle, An Analysis of Programs by algebraic means, Banach Center Publications, vol. 2, Polish Scientific Publishers, 1977

The rapid development of software techniques and technologies in the past decade raises the urgent necessity of creating a theoretical background adequate to fulfill the following three tasks:

1. improving our generał understanding of software; e.g., answering questions such as: What should a programming language look like? What are data structures and how should they be described? What can program complexity mean and how to measure it? etc.
2. providing tools for analysis, documentation, and designing of software objects such as programs, operating systems, programming languages, data banks, etc.
3. improving methods of teaching programming by introducing theories with well-defined ideas e.g., of a program, of recursion and iteration, of structuring, and eliminating teaching by examples as the only method of education in software.

The problem that stimulated the present contribution and a large number of others is connected with 2. above and is usually referred to as proving properties of programs. In fact, we try here to construct a mathematical tool for the analysis of programs.

Programs are clearly expressions in more or less formal languages, however, proving properties of programs is not proving properties of expressions but of their meaning. What are, therefore, the meanings of programs?

For the majority of authors, these meanings are functions, or binary relations, describing the input-output processing. How these relations are associated with programs is not a straightforward matter and therefore must be described formally. The most common method of carrying out such a description consists in introducing a formal language L, whose expressions are interpreted as programs. The way one associates such expressions with programs is considered obvious and therefore is not described in the system. The way one associates relations with expressions is not obvious at all and is usually described by a semantic function.

Proving properties of programs consists in proving properties of the associated relations. This may be carried out either within the usual mathematical theories such as set theory, algebrą. of relations, and the like, or in purpose-oriented formalized theories frequently equipped with a special logic. In the latter case, L is assumed to be a set of terms in the theory, and appropriate formulas are considered as theorems about programs.

In the present approach, we proceed in a different way. Mathematical models of programs are assumed to be abstract algorithms, and their meanings to be objects generated (defined) by these algorithms. The generated objects, however·, need not be solely relations. According to what we want to prove about a program, we associate with it an algorithm generating objects of the appropriate type:

1. the usual binary relations-for the usual input-output analysis,
2. the so-called c5-relations-for input-output analysis covering the description of infinitistic behavior (looping),
3. sets of sequences of states (called computations), to extend the input-output description to the description of runs,
4. languages, to prove properties of classes of programs with the same "topolology" but different interpretations of modules,
5. other objects-for other purposes.

Andrzej Blikle, Specified programming, Institute of Computer Science, Warsaw 1978, a preprint of a paper later published in the Proceedings of the International Conference on Mathematical Studies in Information Processing, Kyoto, August 1978.

The paper presents a method of mathematically supported correct programming. Totally correct programs are developed by means of transformation rules. These programs are considered and transformed together with their specifications. The specifications are of two types: global (pre- and post-conditions) and local (redundant tests). The transformations always preserve the total correctness of programs and are rather flexible; e.g. one may add or remove variables in the program or switch from one data type to another.

Andrzej Blikle, The Clean Termination of lterative Programs, Acta Informatica 16, 199-217 (1981)

The paper is devoted to a program-correctness concept that captures partial correctness, termination (nonlooping), and clean termination (non-abortion). The underlying proof method offers a one-stage proof of all three properties. This method is proved consistent and algebraically complete. It is first discussed for the generał case of arbitrary possibly nondeterministic iterative programs. Next, this case is restricted to arbitrary deterministic iterative programs and finally to structured programs. The presented approach is compared with partial correctness, total correctness, and weakest precondition methods. The concluding example shows the verification of an arithmetical program in machine-bounded arithmetics. As a side effect of the verification procedure, one finds input boundary conditions which guarantee clean termination.

Andrzej Blikle, On the development of Correct Specified Programs, IEEE Transactions on Software Engineering, vol. SE-7, No 5, September 1981

The paper describes a method of program development that guarantees correctness. Our programs consist of an operational part, called instruction, and a specification. Both these parts are subject to the development and the refinement process. The specification consists of a pre- and postcondition called global specification and a set of assertions called local specification. A specified program is called correct if: 1) the operational part is totally correct w.r.t the pre- and postcondition, 2) the precondition guarantees nonabortion, 3) local assertions are adequate for the proof of 1) and 2). The requirement of nonabortion leads to the use of three-valued predicate calculus. We use McCarthy’s calculus in this place. The paper contains a description of an experimental programming language PROMET-1 designed for our style of programming. The method is illustrated by the derivation of a bubblesort procedure.

Andrzej Blikle, Andrzej Tarlecki, Naive Denotational Semantics, Information Processing 83, R.E.A. Mason (ed.) Elsevier Science Publishers B. V. (North-Holland) © IFIP, 1983

The sophisticated mathematical framework of denotational semantics (Scott's reflexive domains and continuations) is not only discouraging for many practitioners but also leads to several technical problems in applications. In this paper, we investigate the possibility of developing denotational semantics where semantic domains are just sets and where states rather than continuations are transformed by the program's components. We show that a full mechanism of goto's may be described without continuations and that some procedural mechanisms (e.g. static binding with a hierarchy of procedural parameters like in PASCAL) do not require reflexive domains. We show further, that if we relax the denotational principle and adept a copy-rule semantics of procedures, then any procedural mechanism can be described in our framework.

Beata Konikowska, Andrzej Tarlecki, Andrzej Blikle, A three-valued logic for software specification and validation, an early preprint of a paper later published in VDM’88, VDM: The Way Ahead, Proc. 2nd VDM-Europe, Dublin 1988, Lecture Notes in Computer Science, Springer Verlag 1988, pp. 218-242

Different calculi of partial or three-valued predicates have been used and studied by several authors in the context of software specification, development, and validation. This paper offers a critical survey on the development of three-valued logics base on such calculi.

In the first part of the paper, we review two three-valued predicate calculi based on, respectively, McCarthy’s and Kleene’s propositional connectives and quantifiers, and point out that in a three-valued logic one should distinguish between two notions of validity: strong validity (always true), and weak validity (never false). We define in model-theoretic terms a number of consequence relations for three-valued logic. Each of them is determined by the choice of the underlying predicate calculus and of the weak or strong validity of axioms and theorems. We discuss mutual relationships between consequence relations defined in such a way and study some of their basic properties.

The second part of the paper is devoted to the development of a formal deductive system of inference rules for a three-valued logic. We use the method of semantic tableaux (slightly modified to deal with three-valued formulas) to develop a Gentzen-style system of inference rules for deriving valid sequents, which we use later to obtain a sound and complete system of natural deduction rules. We have chosen to study the consequence relation determined by the predicate calculus with McCarthy’s propositional connectives and Kleene’s quantifiers and by the strong interpretation of both axioms and theorems. Although we find this choice appropriate for applications in the area of software specification, verification, and development, we regard this logic merely as an example and use it to present some general techniques of developing a sequent calculus and a natural deduction system for a three-valued logic.

Andrzej Blikle, Denotational engineering, Science of Computer Programming 12 (1989) 207-253, North-Holland

This paper is devoted to the methodology of using denotational techniques in software design. Since denotations describe the essential components comprising a system and syntax provides ways for the user to access and communicate with these components, we suggest that denotations are developed in the first place and that syntax be derived from them later. That viewpoint is opposite to the traditional (descriptive) style where denotational techniques are used in assigning a meaning to some earlier defined syntax. Our methodology is discussed on an algebraic ground where both denotations and syntax constitute many-sorted algebras and where denotational semantics is a homomorphism between them. On that ground, the construction of a denotational model of a software system may be regarded as a derivation of a sequence of algebras. We discuss some mathematical techniques which may support that process especially this part where syntax is derived from denotations. The suggested methodology is illustrated in two small examples.

Andrzej Blikle, Why denotational? Remarks on applied denotational semantics, an early preprint of my paper (by 1990) later published in Fundamenta Informaticae 28, 1966, pp. 55-85

This is an essay where the author expresses his views on applied denotational semantics. In the author’s opinion, whether a software system has or does not have a sufficiently abstract denotational semantics should be regarded as a pragmatic attribute of the system rather than merely as a mathematical attribute of its description. In a software system with denotational semantics, structure programming is feasible, and for such systems, there is a routine method of developing program-correctness logic. All that may not be the case if denotationality is not ensured. On the other hand, a non-denotational semantics can always be artificially made denotational at the expense of lowering its level of abstraction. This leads to an important pragmatic question: to what extent and in which situations can we sacrifice denotationality and/or abstraction of a semantics? All discussion is carried on an algebraic ground, but the paper is not very technical and contains a short introduction to the algebraic approach to denotational semantics.