scholarly journals A Constructive Approach to Compiler Correctness

1980 ◽  
Vol 9 (118) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Target Language ◽  
Constructive Approach ◽  
Abstract Data Types ◽  
Machine Code ◽  
Data Types ◽  
Denotational Semantic ◽  
Abstract Data ◽  
The One ◽  
Semantic Definition

<br /> It is suggested that denotational semantic definitions of programming languages should be based on a small number of abstract data types, each embodying a fundamental concept of computation. Once these fundamental abstract data types have been implemented in a particular target language (e.g. stack-machine code), it is a simple matter to construct a correct compiler for any source language from its denotational semantic definition. The approach is illustrated by constructing a compiler similar to the one which was proved correct by Thatcher, Wagner <em>Et</em> Wright ( 1979). Some familiarity with many-sorted algebras is presumed.

scholarly journals Tree-Shaped Formats of Address Programming Language

2021 ◽  
Vol 4 ◽  
pp. 78-87
Author(s):  
Yury Yuschenko
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Theoretical Research ◽  
Direct Access ◽  
Complex Data ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data ◽  
The One ◽  
High Level

In the Address Programming Language (1955), the concept of indirect addressing of higher ranks (Pointers) was introduced, which allows the arbitrary connection of the computer’s RAM cells. This connection is based on standard sequences of the cell addresses in RAM and addressing sequences, which is determined by the programmer with indirect addressing. Two types of sequences allow programmers to determine an arbitrary connection of RAM cells with the arbitrary content: data, addresses, subroutines, program labels, etc. Therefore, the formed connections of cells can relate to each other. The result of connecting cells with the arbitrary content and any structure is called tree-shaped formats. Tree-shaped formats allow programmers to combine data into complex data structures that are like abstract data types. For tree-shaped formats, the concept of “review scheme” is defined, which is like the concept of “bypassing” trees. Programmers can define multiple overview diagrams for the one tree-shaped format. Programmers can create tree-shaped formats over the connected cells to define the desired overview schemes for these connected cells. The work gives a modern interpretation of the concept of tree-shaped formats in Address Programming. Tree-shaped formats are based on “stroke-operation” (pointer dereference), which was hardware implemented in the command system of computer “Kyiv”. Group operations of modernization of computer “Kyiv” addresses accelerate the processing of tree-shaped formats and are designed as organized cycles, like those in high-level imperative programming languages. The commands of computer “Kyiv”, due to operations with indirect addressing, have more capabilities than the first high-level programming language – Plankalkül. Machine commands of the computer “Kyiv” allow direct access to the i-th element of the “list” by its serial number in the same way as such access is obtained to the i-th element of the array by its index. Given examples of singly linked lists show the features of tree-shaped formats and their differences from abstract data types. The article opens a new branch of theoretical research, the purpose of which is to analyze the expe- diency of partial inclusion of Address Programming in modern programming languages.

scholarly journals A Semantic Algebra for Binding Constructs

1982 ◽  
Vol 10 (132) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Denotational Semantics ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data ◽  
Algebraic Operators

This paper presents a semantic algebra, suitable for use in giving the denotational semantics of various forms of declarations and binding constructs in programming languages. The emphasis of the paper is on the development of semantic descriptions which are easy to understand at an intuitive level, being based on algebraic operators corresponding to fundamental concepts of programming languages. Some familiarity with denotational semantics and abstract data types is assumed.

An Interpretability Approach to the Theory of Abstract Data Types1

1983 ◽  
Vol 6 (3-4) ◽  
pp. 297-332
Author(s):  
Wiktor Dańko
Keyword(s):  
Programming Languages ◽  
Dynamic Logic ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data ◽  
Algorithmic Logic

In this paper, similarly to [1,4,17,20,21,29,30], abstract data types are understood as formalized many-sorted theories based on algorithmic languages (e.g. a language of algorithmic logic [2,16] or a language of dynamic logic [11,29]). Operations on data types, leading from (more) primitive types to compound types, are defined in terms of the interpretability theory (cf. Szczerba [25]). The approach proposed here to defining new types accords with the methods of introducing new classes of objects in programming languages like Simula 67, Pascal, Loglan, Ada.

Pattern matching with abstract data types

1993 ◽  
Vol 3 (2) ◽  
pp. 171-190 ◽  
Author(s):  
F. Warren Burton ◽  
Robert D Cameron
Keyword(s):  
Programming Languages ◽  
Pattern Matching ◽  
Functional Programming ◽  
Abstract Data Types ◽  
Data Types ◽  
Functional Programming Languages ◽  
Equational Reasoning ◽  
Abstract Data ◽  
Algebraic Data Types ◽  
Lazy Functional Programming

AbstractPattern matching in modern functional programming languages is tied to the representation of data. Unfortunately, this is incompatible with the philosophy of abstract data types.Two proposals have been made to generalize pattern matching to a broader class of types. The laws mechanism of Miranda allows pattern matching with non-free algebraic data types. More recently, Wadler proposed the concept of views as a more general solution, making it possible to define arbitrary mappings between a physical implementation and a view supporting pattern matching. Originally, it was intended to include views in the new standard lazy functional programming language Haskell.Laws and views each offer important advantages, particularly with respect to data abstraction. However, if not used with great care, they also introduce serious problems in equational reasoning. As a result, laws have been removed from Miranda and views were not included in the final version of Haskell.We propose a third approach which unifies the laws and views mechanisms while avoiding their problems. Philosophically, we view pattern matching as a bundling of case recognition and component selection functions instead of a method for inverting data construction. This can be achieved by removing the implied equivalence between data constructors and pattern constructors. In practice, we allow automatic mapping into a view but not out of the view. We show that equational reasoning can still be used with the resulting system. In fact, equational reasoning is easier, since there are fewer hidden traps.

scholarly journals Unified Algebras and Action Semantics

1988 ◽  
Vol 18 (272) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Abstract Data Types ◽  
Data Types ◽  
Action Semantics ◽  
Nondeterministic Choice ◽  
Abstract Data

The recently-developed framework of Unified Algebras is intended for axiomatic specification of abstract data types. In contrast, the somewhat older framework of Action Semantics (earlier known as ''Abstract Semantic Algebras'') is for denotational specification of programming languages. This paper gives an introduction to the main features of Unified Algebras and Action Semantics, and discusses the relation between them. The two frameworks both exploit nondeterministic choice in unconventional ways.

Algebraic specification of abstract data types

2001 ◽  
Author(s):  
J. Loeckx ◽  
H.-D. Ehrich
Keyword(s):  
Programming Languages ◽  
Data Structures ◽  
Complex Structure ◽  
Abstract Data Type ◽  
Specification Languages ◽  
Abstract Data Types ◽  
Data Types ◽  
Control Structures ◽  
Abstract Data ◽  
Number Of Publications

It is widely accepted that the quality of software can be improved if its design is systematically based on the principles of modularization and formalization. Modularization consists in replacing a problem by several “smaller” ones. Formalization consists in using a formal language; it obliges the software designer to be precise and principally allows a mechanical treatment. One may distinguish two modularization techniques for the software design. The first technique consists in a modularization on the basis of the control structures. It is used in classical programming languages where it leads to the notion of a procedure. Moreover, it is used in “imperative” specification languages such as VDM [Woodman and Heal, 1993; Andrews and Ince, 1991], Raise [Raise Development Group, 1995], Z [Spivey, 1989] and B [Abrial, 1996]. The second technique consists in a modularization on the basis of the data structures. While modern programming languages such as Ada [Barstow, 1983] and ML [Paulson, 1991] provide facilities for this modularization technique, its systematic use leads to the notion of abstract data types. This technique is particularly interesting in the design of software for non-numerical problems. Compared with the first technique it is more abstract in the sense that algebras are more abstract than algorithms; in fact, control structures are related to algorithms whereas data structures are related to algebras. Formalization leads to the use of logic. The logics used are generally variants of the equational logic or of the first-order predicate logic. The present chapter is concerned with the specification of abstract data types. The theory of abstract data type specification is not trivial, essentially because the objects considered — viz. algebras — have a more complex structure than, say, integers. For more clarity the present chapter treats algebras, logics, specification methods (“specification-in-the-small”), specification languages (“specification-in-the-large”) and parameterization separately. In order to be accessible to a large number of readers it makes use of set-theoretical notions only. This contrasts with a large number of publications on the subject that make use of category theory [Ehrig and Mahr, 1985; Ehrich et al., 1989; Sannella and Tarlecki, 2001].

HYPERSUBSTITUTIONS OF MANY-SORTED ALGEBRAS

2008 ◽  
Vol 01 (03) ◽  
pp. 337-346 ◽  
Author(s):  
Klaus Denecke ◽  
Somsak Lekkoksung
Keyword(s):  
Computer Science ◽  
Binary Operation ◽  
Data Type ◽  
Abstract Data Type ◽  
Abstract Data Types ◽  
Data Types ◽  
Abstract Data ◽  
The Many ◽  
The One

Many-sorted algebras are used in Computer Science for abstract data type specifications. It is widely believed that many-sorted algebras are the appropriate mathematical tools to explain what abstract data types are ([1]). In this paper we want to extend the concept of a hypersubstitution from the one-sorted to the many-sorted case. Hypersubstitutions are used for one-sorted algebras to define hyperidentities and M-solid varieties ([2]). We will prove that extensions of hypersubstitutions for many-sorted algebras are endomorphisms of the many-sorted clone of a given type. As in the one-sorted case we define a binary operation for hypersubstitutions and prove that with respect to this operation all many-sorted hypersubstitutions form a monoid.

Towards the Temporal Approach to Abstract Data Types

1988 ◽  
Vol 11 (1) ◽  
pp. 49-63
Author(s):  
Andrzej Szalas
Keyword(s):  
Temporal Logic ◽  
Abstract Data Types ◽  
Data Types ◽  
First Order ◽  
Abstract Data ◽  
Order Completeness ◽  
General Method

In this paper we deal with a well known problem of specifying abstract data types. Up to now there were many approaches to this problem. We follow the axiomatic style of specifying abstract data types (cf. e.g. [1, 2, 6, 8, 9, 10]). We apply, however, the first-order temporal logic. We introduce a notion of first-order completeness of axiomatic specifications and show a general method for obtaining first-order complete axiomatizations. Some examples illustrate the method.

Sign in / Sign up

Export Citation Format

Share Document