Preprints of IIS SB RAS, 2005

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.

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.

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.

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.

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.

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.