References to MetaSoft

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, 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, 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 which 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.

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 logics. Each of them is determined by 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 into the algebraic approach do denotational semantics.