Preprints of IIS SB RAS, 2005

Preprint 131
E. Bodin, N. Kalinina, N. Shilov
VERIFYING COMPILER F@BOOL@ Part I: Outlines of F@BOOL@ project in the context of component-based programming. Mini-NIL: a prototype of F@BOOL@ virtual machine language

Verifying Compiler is a system program that proves specified program properties besides translation of program. Paper represents overview of the research project that is entitled to design and implement a verifying compiler F@BOOL@, provides some theoretical background for feasibility of the project, discusses importance of verifying compilers for component-based approach to programming.

At the same time paper fixes formal syntax and operational semantics of a toy programming language Mini-NIL. This language is designed for approbation of basic concepts of the project and is a prototype of F@BOOL@ virtual machine. Publication is the first part of F@BOOL@ documentation.

Preprint 129
Elena N. Bozhenkova
The investigation of testing relations for timed event structures

In this paper we try to decide a problem of recognising timed testing equivalences for event structures with dense time. For this purpose we construct a formula that characterizes a timed event structure up to the timed testing preorder. So, to understand if two timed event structures are in testing relations it is enough to check, if the formula is satisfied.

Preprint 128
V.A. Nepomniaschy, I.S. Anureev, I.V. Dubranovsky, A.V. Promsky
Towards C# program verification: a three-level approach

A new three-level approach to sequential object-oriented program verification is presented. It is applied to a significant C# subset called C#-light that includes all principal sequential C# constructs. At the first stage, C#-light is translated into an intermediate language C#-kernel. A Hoarelike logic is presented for C#-kernel. At the second stage, lazy verification conditions are generated by means of the Hoare-like logic. The generated verification conditions are lazy because they can include symbols representing postponed extractions of invariants of labelled statements as well as postponed invocations of methods and delegates. At the third stage, lazy verification conditions are refined using some algorithms of operational semantics. This approach allows us to simplify axiomatic semantics and to make unambiguous inference of lazy verification conditions. An example of verification of a C#-light program serves to illustrate this approach.

Preprint 127
Vitaliy V. Kalchenko
Review of algebras for xml database systems

XML database systems have become very popular last years. XQuery is regarded to be the most perspective query language for these systems. This paper contains a review of different algebras for XML databases. Estimation of their applicability for XQuery support is given.

Preprint 126
E.V. Bodin, L.V. Gorodnyaya, N.V. Shiliv
What is the subject of the computer science contest?

The paper is devoted to the current situation with Informatics and Programming contests. The major problem consists in the relative multitude of formats of programming contests as compared to contests in other fields; moreover, there is a certain fuzziness in the definition of the subject and organization structure. The basic definitions of the subject of Informatics and the complexity of its teaching at schools are demonstrated in a series of solutions of a rather well-known problem, which is often included, with slight variations, into such contests. The solution algorithms for this problem, including   heuristic algorithm of E.Dijkstra, illustrate the ambiguity of problem evaluation criteria and the variety of constructions yielding a formally correct solution.

Preprint 125
Leonid Novak, Alexandre Zamulin
An XML algebra for XQUERY (preliminary communication)

An XML algebra supporting the query language XQuery is presented. The algebra is in fact a number of expression constructing operators algebraically defined. The introduction of expression constructing operators instead of high-order operations using functions as parameters has permitted us to remain in the limits of first-order structures whose instance a many-sorted algebra is. The set of operators of the presented algebra substantially differs from the set of operators of relation algebra. The difference is caused by the more complex structure of the XML document compared to the relation. In fact, only selection by predicate test is more or less the same in both algebra. At the same time, the XML algebra in addition permits selection by node test. The projection operator of relation algebra is replaced by the path expression and a number of navigating functions permitting selection of different parts of the document tree. The join operator is replaced by a number of unnesting join expressions permitting creation of a stream of flat tuples on the base of several possibly nested parts of the document tree. In addition, a number of node constructing expressions permitting update of the current algebra by introduction of new are defined.

Preprint 124
Tatyana G. Churina, Victor S. Argirov
Modeling sdl specifications using modified htt-nets

In order to simplify simulation and verification of distributed systems, modified coloured Petri nets called hierarchical timed typed nets (HTT-nets) are introduced. The nets are extended by the priorities, Merlin's time concepts and special places representing queues of tokens. A method for translation from SDL into HTT-nets and its implementation are presented. Complexity bounds of resulted nets which confirm effectiveness of the translation method are given.

Preprint 123
Sergey Brazhnik, Alexandre Zamulin
An imperative extension of the object constraint language ocl

An extension of the object constraint language OCL by a mechanism permitting specification of methods updating the object state is described and investigated in the paper. An original version of transition rules of Abstract State Machines is proposed as such a mechanism. The new language facilities are investigated by specification of the class diagram of a representative example.




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.