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 attribut

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 a three-valued predicate calculus. We use McCarthy's calculus in that 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.

The paper deMs with the problem of how to design a computer so that the loop-free parts of computations performed by it are handled in the most efficient and rapid manner.In particular, the question is how to design a unit to carry out loop-free computations and how to design the unit-oriented language.Clearly, the sensitive area here is the storing and accessing of intermediate results.It is assumed that the unit reads the appropriate program step-bystep, performs successive operations serially and stores the intermediate results in a sequence as the computation progresses.Now a problem arises how the unit should extract intermediate results from the sequence when needed.It is shown that the optimM solution is addressless units (the unit-oriented programs are address-free formulas) which operate in double-endedqueue disciplines, i.e. in disciplines where the actually extracted intermediate result is always either the first or the last element of the stored sequence.The paper follows and extends some ideas given by Z. Pawlak in a number of his papers.It gives the mathematical background and extentions of Pawlak's results which have been formulated originally in a rather descriptive and informM way.The reader is not assumed to be familiar with Pawlak's papers.

of twenty-six short communications presented at the meeting.For the Organizing Committee A. MOSTOWSKI A. BLIKLE