Search Results

You are looking at 1 - 3 of 3 items for

  • Author: Tibor Gregorics x
Clear All Modify Search
Open access

Tibor Gregorics

Abstract

Several versions of the backtracking are known. In this paper, those versions are in focus which solve the problems whose problem space can be described with a special directed tree. The traversal strategies of this tree will be analyzed and they will be implemented in object-oriented style. In this way, the traversal is made by an enumerator object which iterates over all the paths (partial solutions) of the tree. Two different “acktracking enumerators” are going to be presented and the backtracking algorithm will be a linear search over one of these enumerators. Since these algorithms consist of independent objects (the enumerator, the linear search and the task which must be solved), it is very easy to exchange one component in order to solve another problem. Even the linear search could be substituted with another algorithm pattern, for example, with a counting or a maximum selection if the task had to be solved with a backtracking counting or a backtracking maximum selection.

Open access

Tibor Gregorics

Abstract

The A** algorithm is a famous heuristic path-finding algorithm. In this paper its different definitions will be analyzed firstly. Then its memory complexity is going to be investigated. On the one hand, the well-known concept of better-information will be extended to compare the different heuristics in the A** algorithm. On the other hand, a new proof will be given to show that there is no deterministic graph-search algorithm having better memory complexity than A**∗. At last the time complexity of A** will be discussed.

Open access

A unified approach of program verification

Dedicated to the memory of Antal Iványi

Tibor Gregorics and Zsolt Borsi

Abstract

The subject of this paper is a program verification method that takes into account abortion caused by partial functions in program statements. In particular, boolean expressions of various statements will be investigated that are not well-defined. For example, a loop aborts if its execution begins in a state for which the loop condition is undefined. This work considers the program constructs of nondeterministic sequential programs and also deals with the synchronization statement of parallel programs introduced by Owicki and Gries [7]. The syntax of program constructs will be reviewed and their semantics will be formally defined in such a way that they suit the relational model of programming developed at Eőtvős Loránd University [3, 4]. This relational model defines the program as a set of its possible executions and also provides definition for other important programming notions like problem and solution. The proof rules of total correctness [2, 5, 8, 9, 7] will be extended by treating abortion caused by partial functions. The use of these rules will be demonstrated by means of a verification case study.