Preprints of IIS SB RAS, 2012

Preprint 169
A.V. Promsky
A formal approach to the error localization

At first sight the program verification is trustworthy and convenient, which is guaranteed by its well-developed formal basis. However, this method works smoothly in an ideal case only: a program and its annotations are correct, a domain theory is complete and a theorem prover is powerful enough. In case any of these prerequisites do not hold, the verification becomes much more complicated. Apart from possible defects in the foundations (which are not discussed here), one of the reasons is that verification, as a process, still relies on informal methods or implementation tricks. Error tracing is one of them. In this paper we would like to address this issue by giving a review of error localization and explanation methods developed in the C-light project. Their application is illustrated by examples.

Preprint 168
N.V. Vizovitin, V.A. Nepomniaschy
UCM-specifications to colored Petri nets translation algorithms
Algorithms for translation of UCM (Use Case Maps) specifications to colored Petri nets (CPN) are described. A UCM specification allows for modeling of functional requirements in a concise and efficient manner. The UCM visual scenario notation focuses on the causal flow of behavior optionally superimposed on a structure of components. Translation of all standard UCM constructs is described, with the exception of complex decomposition constructs. Translation of UCM specifications to CPN is illustrated with an example.
Preprint 167
I.V. Kablukov, V.I. Shelekhov
Variable gluings in a predicate program

The variable gluing transformation is a replacement of all occurrences of a variable to another variable in a predicate program. The sound set of variable gluings is founded on the basis of data flow analysis of the program.

Preprint 166
M.S. Chushkin, V.I. Shelekhov
Generation and proof of correctness conditions for predicate programs

Rules for proving the correctness conditions for different statement of a predicate program are developed. The implementation of a generator of the total correctness of a predicate program is described. The total correctness conditions of a program are translated to the specification language of the PVS proof system.

Preprint 165
I.S. Anureev
Transition systems oriented to development of software systems specification and verification tools

A high-level specification language for labeled transition systems oriented to development of software systems specification and verification tools is proposed in this paper. The classes of such systems, focused on development of operational semantics of programmming languages and proving of safety properties of programs are presented. A methodology of application of the specialized transition systems for development of oprational semantics and safety logic by the example of a model programming language is described.

Preprint 164
V.I. Shelekhov
Development and verification of heapsort algorithms in predicate programming paradigm

Three heapsort (classic, Floyd’s, and improved) algorithms are described. The improved heapsort algorithm is the fastest sorting algorithm. The algorithms are described in the P predicate programming language with their specifications in the form of a precondition and postcondition. Deductive verification of the algorithms in the framework of the PVS prover and repeated development of the specifications were performed over two months.

Preprint 163
V.А. Batrakov, V.I. Shelekhov
Automatic proving of correctness formulas from predicate programs in the Russell system

The development of a translator of the P language formulas into the language of the Russell automatic prover system with the purpose of proving the correctness formulas in Russell is described.

Preprint 162
I.V. Kablukov, V.I. Shelekhov
Checking the dynamic semantics conditions of predicate programs

In the predicate programming system, the development of checking the dynamic
semantics conditions of predicate programs by means of automatic proof
in the PVS system is described.

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.