Applying Program Transformations for Deductive Verification of the List Reverse Program

The program transformation methods to simplify the deductive verification of programs with recursive data types are investigated. The list reversion program is considered as an example. A source program in the C language is translated to the cP functional language which includes no pointers. The resulting program is translated further to the WhyML language to perform deductive verification of the program. The cP language includes the same constructs of the C language except pointers. In the C program, all actions that include pointers are replaced by the equivalent fragments without pointers. These replacement are performed by the special transformations using the results of the program dataflow analysis. Three variants of deductive verification of the transformed list reverse program in the Why3 verification platform with SMT solvers (Z3 4.8.6, CVC3 2.4.1, CVC4 1.7) are performed. First, the recursive WhyML program supplied with specifications was automatically verified successfully using only SMT solvers. Second, the recursive program was translated to the P predicate language. Correctness formulae were constructed for the P program and translated further to the why3 specification language. The formulae proving correctness were easy like the first variant. But correctness formulae for the first and second variants were different. Third, the "imperative" WhyML program that included while loop with additional invariant specifications was verified. The proving was easy but not automatic. So, for deductive verification, recursive program variant appears to be more preferable against imperative program variant.

TECHNOLOGIES OF MULTILEVEL STRUCTURES MODELLING ON THE EXAMPLE OF THE PROBLEM OF COMPLETING PRODUCTS

Urgency of the research. One of the typical tasks encountered in the de-signing of intelligent systems is modelling of the multilevel structures for solving various applied problems. Target setting. Consideration the possibilities of the language of artificial intelligence Visual Prolog for the implementation of recursive technology-based on the example of solving a multi-level task of product configuration. Actual scientific researches and issues analysis. Such scientists as Biletsky O. B., Lytvyn V. V., Chery S., Gottlob G., Luger G. F., Russell G.F. made significant contribution to the development of the theory, methodology of artificial intelligence application for solving problems in the field of economics. Uninvestigated parts of general matters defining. At the same time, insufficient scientific works highlight the features of the introduction of modern means of artificial intelligence for solving multilevel economic problems. The research objective. Analyze existing approaches to solving multi-level tasks. To propose an effective tool for solving multilevel tasks using artificial intelligence language Visual Prolog. The statement of basic materials. The problem of modeling of multilevel structures in intellectual systems on the basis of iterative and recursive technologies on the example of the problem of components is considered. The main characteristics of such structures are presented, their complexity is determined and the necessity of finding effective methods for their presentation and processing in the memory of the machine is given. There are two important paradigms in the development of recursive technologies: functional and logical programming. We consider the corresponding languages of artificial intelligence: Lisp and Prolog, their heirs and the most powerful language of Visual Prolog. The classical well-known iterative algorithm and the recursive program on the Prologue of solving the problem of the components of the internal combustion engine, as well as the recursive program on Visual Prolog, developed by the authors of the article, are given. Their comparison is made from the position of using the number of structures for the presentation of the information base, the cost of memory for their preservation, the complexity of developing and debugging the program, the ease of perception of their work. Conclusions. The power of the language Visual Prolog is emphasized, which is especially manifested in the tasks of processing multi-level structures.

Logic Macroprogramming for Wireless Sensor Networks

It is notoriously difficult and tedious to program wireless sensor networks (WSNs). To simplify WSN programming, we propose Sense2P, a logic macroprogramming system for abstracting, programming, and using WSNs as globally deductive databases. Unlike macroprograms in previous works, our logic macroprograms can be described declaratively and imperatively. In Sense2P, logic macroprogrammers can easily express a recursive program or query that is unsupported in existing database abstractions for WSNs. We have evaluated Sense2P analytically and experimentally. Our evaluation result indicates that Sense2P successfully realizes the logic macroprogramming concept while consuming minimal energy as well as maintaining completeness and soundness of the answers.