Fundamental research

Z Lem
Skocz do: nawigacji, wyszukiwania

Work on programming language Loglan'82 and its compiler was accompanied by vivid discussions and fundamental research. On these pages we shall report some of results and an attempt to define an axiomatic semantics of Loglan'82.

Problems and reports

Safe dealocation of objects

The problem is how to dealocate unused objects in a safe way?
Some programming languages (Pascal, C++) allow to use instruction delete(x). Other languages (Java, Python) forbid such instructions and relay on the garbage collection gc(). In this way the Java's object management system gains safety but becomes much less controlled. It may happen that another danger named memory leakage will appear. We are happy to present you the object managing system invented by Antoni Kreczmar. In his system one can use the atomic instruction kill(x) in order to dealocate an object being the value of the variable x.

The axiom of kill is here

[math] \underbrace{((x= y = ... =x_n) \wedge x \neq \textbf{none})}_{precondition}\Rightarrow \underbrace{[kill(y)]}_{\mathrm{statement}}\underbrace{(x= y = ... =x_n = \textbf{none})}_{postcondition} [/math]

It tells that all references to an object x obtain the value none. No dangling reference error appears. The cost of the kill operation is fixed, independent of how many variables share the object x as common value. For more information see


Note, no other programming language enjoys the property of safe dealocation.

How to determine the direct superclass?

One program may contain many classes of the same name. This is true of any programming language that allow to nest one class in another. Now, let us consider the inheritance relation between classes.

Suppose that a class B inherits (i.e. extends) the class A. Which of possibly many classes A we should identify as a base class?

This question is a fundamental one for the definition of semantics. Consider the following example written in Java.

class A extends B { // this can be class B or A.B i.e. class B contained in class A
class C extends D { // this can be class B.D or E.D
class F extends G {} // this can be class A.E.G or E.G
} // end C
class E {
class G {}
} // end E
class B extends E {} // this can be class E or A.E
} // end A
class B {
class D extends E {} // this can be class E or A.E
} // end B
class E {
class G extends B {} // this can be class B or A.B
class D {}
} // end E

Questions

  • The author of the program may write "extends B" or "extends A.B"(first line). It is to a compiler to guess what the author had in mind when writing the program and assign the correct answer. Which of possible 64 assignments is correct? Note, a real program may contain hundreds of classes.
  • How to diagnose incorrect programs? For there are innocently looking programs that do not posses a correct solution. See [{}] for an example.
  • Is there any efficient algorithm to determine direct superclasses?

There are 4 languages which admit both nesting of modules (i.e. block structure ) and inheritance:

  • Simula67
  • Loglan'82
  • BETA
  • Java

Each language gives another definition of the base class. We shall mention ...

Static binding

Let a be an applicative occurence of an identifier i. (Applicative means in an instruction.) Where to find a proper declaration of the idenfifier i? The problem known for block structured programming languages is far more complicated in the languages that admit not only nesting of modules but also inheritance.

For Loglan'82 a solution was find by Danuta Szczepańska (not published, validated through compiler).

A general case is considered in ...

Is it possible to keep the Dijkstra's mechanism of Display Vector ?

The problem arises when a programming language allows to nest declarations of classes as well as their extensions by inheritance. Now, if one defines a constructor of a class as a concatenation of constructors of inherited classes (it is so called rule of concatenation), then is it possible to define Dijkstra's Display Vector once for all instructions of the consolidated (by concatenation) constructor?
After some monthsof discusions the creators of Loglan programming language came to a solution see
Some time later Hans Langmaack found that the proposed semantic can not be called the correct static semantic.

Two papers appeared that led to a satisfactory solution

The experience gained through this research enabled later to solve the problems of determining drect base class in Java.

Coroutines

How to define the meaning of coroutine operations? in a way free of inconsistency?

Alien call

This is a protocol invented by Bolek Ciesielski in 1988(!) for communication and synchronisation among active objects of process modules. For the first time implemented in Loglan'82 programming language, it remains still little known for programmers.

Connecting virtual machines into a virtual multiprocessor

The virtual Loglan processors VLP can be connected through network thus forming a virtual multiprocessor computer. Each VLP obtains a unique node number.
Now, the creation of an active object of a process module Prc requires a node of virtual computer.

Example
unit Prc: process(nd:integer, <otherParams>); ... end Prc;
var a,b: Prc;
...
a:= new Prc(0,actualParams); (* active object a shares the processor with main *)
b:= new Prc(17, actualPms); (* active object b is placed on node 17 *)
Therefore, one program may organize concurrent and distributed computations.

Some screenshots may be helpful.

Mathematical model of concurrent computations

During the work on Loglan project we conceived and published a model explaining how the execution of concurrent programs look like. The model was named Max model of concurrency. Later it was known under the name of true concurrency model.

Bibliography

  1. [AlgoLog] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic. Warszawa: PWN, 1987, s. 345.

Artykuły

  1. [GMP] Anna Góraj, Grazyna Mirkowska, Anna Paluszkiewicz. On the notion of description of program. „Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.”, s. 499 - 505, 1970.  W tej pracy zawarte jest twierdzenie. Niech P bedzie programem deterministycznym iteracyjnym. Niech o będzie odwzorowaniem przypisującym każdej krawedzi diagramu tego programu formułę pierwszego rzędu. Odwzorowanie to nazwiemy opisem programu P. Opis o jest twierdzeniem teorii T wtedy i tylko wtedy gdy jest dopuszczalny w każdym modelu tej teorii. Powyższe twierdzenie udowodniono wcześniej od tw. Cooka (1978) o relatywnej pełności logiki Hoare'a,
  2. [GM1] Grazyna Mirkowska. Algorithmic logic and its applications in the theory of programs I. „Fundamenta Informaticae”, s. 1-17, 1977. 
  3. [GM2] Grazyna Mirkowska. Algorithmic logic and its applications in the theory of programs II. „Fundamenta Informaticae”, s. 147-165, 1977. 
  4. [AS1] Andrzej Salwicki. Formalized Algorithmic Languages. „Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.”, s. 227-232, 1970. 
  5. [AS3] Andrzej Salwicki. On the predicate calculi with iteration quantifiers. „Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.”, s. 279-285, 1970. 
  6. [LB1] Lech Banachowski. Investigations of Properties of Programs by means of Extended Algorithmic Logic I. „Fundamenta Informaticae”, s. 93-119, 1977. 
  7. [LB2] Lech Banachowski. Investigations of Properties of Programs by means of Extended Algorithmic Logic II. „Fundamenta Informaticae”, s. 167-193, 1977. 
  8. [LB3] Lech Banachowski. An Axiomatic Approach to the Theory of Data Structures. „Bull. Acad. Polon. Sci. Ser. Math. Astr. Phys.”, s. 315-323, 1975. 
  9. [AK1] Antoni Kreczmar. Programmability in Fields. „Fundamenta Informaticae”, s. 195-230, 1977. 
  10. [AK2] Antoni Kreczmar. Effectivity problems of Algorithmic Logic. „Fundamenta Informaticae”, s. 19-32, 1977. 

Part II Axiomatic definitions of sublanguages of Loglan'82

Here we shall present an increasing sequence of sublanguages [math]\mathcal{L}_0\subset\mathcal{L}_1\subset\mathcal{L}_2\subset \mathcal{L}_3\subset\mathcal{L}_4\subset \dots[/math]Loglan'82. For each language [math]\mathcal{L}_i[/math] we shall present its grammar and some axioms and inference rules that define its semantics.

Program

Program in Loglan'82 has the following structure

Program
definiendum definiens
program program <name>;
<declarations>

begin

<instructions>

end

where name is any identifier, i.e. a finite sequence of letters and digits beginning with a letter.

The declarations and instructions are finite sequences of declarations and instructions respectively, empty squence included.

This allow us to define the first sublanguage [math]\mathcal{L}_0[/math] of Loglan'82.

[math]\mathcal{L}_0 \stackrel{df}{=}\{p\in \mathcal{A}^*: p=\textbf{program}\ \textit{id}; \textbf{begin end} \}[/math]

Programs of the language [math]\mathcal{L}_0[/math] are empty programs, they posses just a name. Their list of instructions as well as list of declarations are empty. The effect of execution of such program is do nothing.

Now we shall define a new language [math]\mathcal{L}_{0.1}[/math]. First, we say that any expression of the form:
writeln;
write(integer);
write("here your text");
is an output instruction.

[math]\mathcal{L}_{0.1} \stackrel{df}{=}\{p\in \mathcal{A}^*: p=\textbf{program} \textit{ id}; \textbf{begin} \lt\textit{output instructions}\gt \textbf{end} \}[/math]

Example 0.1
program print;

begin

write("hallo world!"); writeln;
write("Today is: May"); write(22); write(2014); writeln

end

Declarations of variables. Assignment instructions

Example

program P2 ;

var x,y: integer;

begin

y:=74;
x:= y+ 8;

end

Grammar
Context free grammar

Well formed expressions

Axiom

[math]\{x:=\tau\}( \alpha ) \Leftrightarrow \alpha(x/\tau)[/math]

Źródło „http://lem12.uksw.edu.pl/index.php?title=Fundamental_research&oldid=1932”