Computer Science, № 29, 2009

An approach to the development of easy-to-use operational specifications of dynamic systems is presented. It is based on the formalism of context machines and the language of description of context machines CML. The main notions of the theory of context machines are defined. Classification of general-purpose contexts is suggested. The...

The process of development of an ontology-based knowledge portal and creation of its content is time-consuming and labor-intensive. It is very desirable to have special analysis facilities for maintenance and development of such a portal. The subject of our paper is a tool for visual analysis of content and ontology...

The behaviour of concurrent systems is often specified extensionally by describing their “state-transitions” and the observable behaviours that such transitions produce. The simplest formal model of computation able to express naturally this idea is that of labelled transition systems, where the labels on the transitions represent the observable part of...

An acute problem for archives and museums is providing high-quality digitized text from low-quality or damaged originals. The majority of companies working in the field of optical character recognition (OCR) focus on digitzed texts of high quality, which represent the majority of processed data and the market for these companies’...

In this paper, by means of an abstract model of the SIMD type with vertical data processing (the STAR{machine), we present basic associative parallel algorithms. These algorithms are represented as the corresponding procedures for the STAR{machine, whose correctness is justified and the time complexity is evaluated. We also propose a...

The paper describes a programming interface that we have developed to separate constraints, solvers, and cooperation strategies in a constraint programming toolkit UniCalc. The interface is simple but it allows us to express such constraint solving techniques as increasing the level of consistency, various strategies for exhaustive search, and cooperation...

The fully automatic verification of programs is a tempting and hardly accessible goal of modern programming. The low-level nature of the most popular programming languages, such as C and C+, has raised its difficulty to a new level. New formal methods and specification languages are required, because the classical Hoare...

Logical semantics is a new kind of formal semantics used to describe semantics of pure call-by-value functional languages. For the statement S, the logical semantics LS(S) is a predicate that is true for the variable values for which the execution of S is finished. Let a specification of the statement...

The purpose of the F@BOOL@ project is to develop a transparent for users, compact, portable and extensible verifying compiler F@BOOL@ for annotated computer programs, that uses effective and sound automatic programs for checking satisfiability of propositional Boolean formulas. The kernel programming language of the project interprets all variables by residuals...

In the paper, the algorithm of the hierarchical cluster analysis is considered and the method is proposed to transfer this algorithm onto the parallel multiprocessor system used on modern graphics processing units (GPUs). Within the frameworks of some natural assumptions, we have estimated the run time of the algorithm in...