Preprints of IIS SB RAS, 2002

Preprint 101
V.I. Shelekhov
The predicate programming language P

ОThe Predicate programming language P is described here. A predicate program is the collection of recursive computable logical equations. It is possible to write a predicate program for each algorithmic decision of a problem whose specification may be written in the predicate form. Facilities of the P language for describing algorithms are more powerful than those of existing functional languages. Along with the functional programming style, the predicate (statement) programming style is applicable. In a predicate program, an array is defined by the forAll constructor which is like the parallel forAll loop in the FORTRAN-90 language. Parallel algorithms may be naturally expressed by means of parallel statements and forAll constructors.

Preprint 100
V. I. Shelekhov
Introduction to predicate programming

Calculus of computing predicates is proposed for the programs whose specification may be represented by a predicate. A language of predicate programming is developed on the basis of the calculus. A predicate program may be transformed into effective imperative one by applying a sequence of transformations. A cycle in an imperative program is the result of the tail recursion transformation. To transform a recursion to the tail recursion form, a universal method of generalization of a predicate program is used. After of the tail recursion transformation, other transformations may be applied: inline transformation for a predicate call, replacing two or more variables by one variable, etc. A hyperfunction appears to be an adequate form of specification of some programs. The split statement based on a hyperfunction is proposed as a new programming construct.

Preprint 99
Moskalyova N.S.
The category theoretical characterization of the trace equivalence for timed concurrent models

The timed extension of a trace equivalence is developed and is characterized on the category. The problem of decidability of this equivalence is solved in the setting of finite timed event structures. This work is supported by by RAS Program "Projects of Young Scientists" under Grant 114 and RFP "Integracia" ("Educational scientific centers").

Preprint 98
N. V. Shilov, N. O. Garanina
Combining knowledge and fixpoints

Program logics are modal logics for reasoning about programs and systems. In general case of semantics we examine the expressive power, model checking and decidability for pairwise fusions of the following program logics: (1)Elementary Propositional Dynamic Logic, Computation Tree Logic extended by actions, and the propositional mu-Calculus with (2)Propositional Logic of Knowledge and Propositional Logic of Common Knowledge. The focus of the paper is on the study of the model checking problem for these combined logics with respect to Forgetful Asynchronous semantics and Synchronous Perfect Recall semantics.

Preprint 97
V. A. Nepomniaschy, I. S. Anureev, I.N. Michailov, A. V. Promsky
Towards the verification of c programs. part 3. translation from c-light into c-light-kernel and its formal proof

Two-level scheme of C-program verification is based on rules for translation from C-light language to C-light-kernel. The translation rules are described in this paper. Operational semantics of C-light is modified in order to simplify both description of semantics of complex C-light constructs, and proving soundness of axiomatic C-light-kernel semantics. A notion of semantical extension is defined, and formal justification of correctness of this translation is given in this paper. We suggest to implement the translation rules in a program verification tool.

Preprint 96
I.S. Anureev
A software support for formal reasoning: from tacticals to tactical generator

A new three level scheme of a prover is suggested in this article. A new third level that presents a tactical generator has been introduced in addition to the usual levels of tactics and tacticals. An executable specification language specifying a class of programs which implement tacticals is described. Operational and axiomatical semantics of this language have been developed. The axiomatical semantics is based on the logical specification language which allows giving precondition, postcondition and invariants in Hoare logic. Examples of presentation of term rewriting systems, context formula rewriting systems, and formula rewriting systems in the executable specification language are given. Context formula rewriting systems allowing presentation of all known combinations of tactics (sequential application, alternate application, cyclic application and so on) have been first considered in this article.

Preprint 95
E. V. Kasianova, S. N. Kasianova
Programming for pupils: a collection of relatively complex problems with solutions

The preprint contains relatively complex problems of programming for pupils. All problems are given with solutions in Pascal. The aim is to coach the pupils using the basic methods for design of nontrivial programs.

Preprint 94
Kozura V.E.
Implementation of the model checking algorithm for coloured petri nets based on net unfoldings

The present paper describes the implementation of the model checking method for coloured Petri nets (CPN) based on net unfoldings. The considered system is a prototype implementation and contains some steps made manually. The main purpose of this work was to show the possibility of applying the model checking procedure based on net unfoldings for CPN to some practical models of distributed systems. As the examples, the CPN representing the dining philosophers problem, an Alternating Bit Protocol and the "Producer-Consumer" system have been considered. These examples are verified using the progress and safety properties as the logical specifications.

Preprint 93
N. N. Tsatsenko
Technologies of work with data in interoperable systems CORBA, RMI, EJB

Work represents the review of two object-oriented technologies of creation of the modern distributed systems - CORBA and RMI. Architecture RMI (Remote Method Invocation) which is integrated with JDK, is a product of company JavaSoft and realizes the distributed model of calculations. RMI allows client's and server's applications through a network to cause methods of the clients / servers which are carried out in Java Virtual Machine, and also gives an opportunity to send objects from the machine to the machine. Technology CORBA (Common Object Request Broker Architecture), developed OMG (Object Managment Group) since 1990 year, allows to cause methods in the objects which are taking place in a network anywhere how if all of them were local objects. One of main principles CORBA is interoperability, it means the opportunity of use in one system of the various applications realized in different languages and carried out on different platforms. The purpose of the given work is to show scale and advantages of technology CORBA in comparison with RMI. Besides as still there is no realization of componental model CORBA, in work the technology of creation of server objects EJB (Enterpise JavaBeans) considered and supported by Sun. In componental model EJB strengths both CORBA, and RMI are used. In the appendix two examples of application CORBA and EJB are resulted with detailed comments.

Preprint 92
V. A. Markin, S. V. Maslov, R. M. Novikov, A. A. Sulimov
Extended pascal to c++ converter

In this work, the main translation schemes elaborated for a converter from an essential Pascal extension to C++ are described. The converter has been developed by order of a large telecommunication company, and it must not only translate an input M-Pascal code to the functionally equivalent C++ code, but also meet some requirements. M-Pascal extensions and requirements for the converter have essentially influenced on the development of translation schemes.

Preprint 91
Kirill O. Senoshenko
Object-oriented specifications: set-theory based and algebraic approaches. a review

In this review, the main trends in object-oriented dynamic system specification are discussed. A classification for the specification approaches is given basing on the underlying model of system state; several representatives from different categories are presented. For each approach, a special attention is given to the completeness of support of various OO concepts, ability to define not only static aspects of the system but also its behavior and the specification transparency. Finally, a comparative review of the selected languages and formalisms is provided and directions for further work are outlined.

Preprint 83
V. A. Evstigneev
Overview of works of novosibirsk scientists in programming (based on materials of the commission on system software of the coordinating committee on computing machinery of the ussr ac.sci.)

This issue is based on materials of the Commission on system software of the Coordinating Committee on Computing Machinery of the USSR Ac.Sci. One of its sessions was devoted to works of the Novosibirsk school of system and theoretic programming over the period of more than 20 years. When discussing the activities, the main attention was paid to the results of the 70-ties and future plans for the 80-ties. Perspectives for the 80-ties turned out to be quite properly determined. This preprint gives us a good presentation of works of the Novosibirsk school at the beginning of 80-ties and in this aspect it can be considered as a successful and natural supplement to the collection of papers "Formation of the Novosibirsk school of programming (mosaic of memoirs)". The work is supported by grant N 02-05-12010в of the Russian Scientific Humanitarian Foundation.

You are reporting a typo in the following text:
Simply click the "Send typo report" button to complete the report. You can also include a comment.