Search Results

1 - 6 of 6 items :

Clear All


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.


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.


Reliability of the technological processes or reliability of devices used in different industries is an important part of designing safety critical systems. The failure of such systems leads to economic losses, health damage or environmental pollution. An important role in the development of safety critical systems is therefore the reliability analysis, the assessment of the risks associated with the use of the technical means and the consequent reduction of this risk. The actual level of risk considered tolerable will vary depending on a number of factors such as the level of human control over the circumstances, the voluntary or unintentional nature of the risk, the number of people at risk in each individual case, the degree of responsibility placed on safety and critical systems reflects the need for quality design and ensure of software safety. Various standards and methods are used to achieve the desired level of safety. One of the methods used for reliability analysis is the use of a block diagram of reliability.


In 1970, D.S. Scott gave applications of Kleene’s fixed point theorem to describe the meaning of recursive denotational specifications in programming languages. Later on, in 1994, S.G. Matthews and, in 1995, M.P. Schellekens gave quantitative counterparts of the Kleene fixed point theorem which allowed to apply partial metric and quasi-metric fixed point techniques to denotational semantics and asymptotic complexity analysis of algorithms in the spirit of Scott. Recently, in 2005, J.J. Nieto and R. Rodríguez-López made an in-depth study of how to reconcile order-theoretic and metric fixed point techniques in the classical metric case with the aim of providing the existence and uniqueness of solutions to first-order differential equations admitting only the existence of a lower solution. Motivated by the aforesaid fixed point results we prove a partial quasi-metric version, when the specialization order is under consideration, of the fixed point results of Nieto and Rodríguez-López in such a way that the results of Matthews and Schellekens can be retrieved as a particular case.


Proving properties of distributed algorithms is still a highly challenging problem and various approaches that have been proposed to tackle it [1] can be roughly divided into state-based and event-based proofs. Informally speaking, state-based approaches define the behavior of a distributed algorithm as a set of sequences of memory states during its executions, while event-based approaches treat the behaviors by means of events which are produced by the executions of an algorithm. Of course, combined approaches are also possible.

Analysis of the literature [1], [7], [12], [9], [13], [14], [15] shows that state-based approaches are more widely used than event-based approaches for proving properties of algorithms, and the difficulties in the event-based approach are often emphasized. We believe, however, that there is a certain naturalness and intuitive content in event-based proofs of correctness of distributed algorithms that makes this approach worthwhile. Besides, state-based proofs of correctness of distributed algorithms are usually applicable only to discrete-time models of distributed systems and cannot be easily adapted to the continuous time case which is important in the domain of cyber-physical systems. On the other hand, event-based proofs can be readily applied to continuous-time / hybrid models of distributed systems.

In the paper [2] we presented a compositional approach to reasoning about behavior of distributed systems in terms of events. Compositionality here means (informally) that semantics and properties of a program is determined by semantics of processes and process communication mechanisms. We demonstrated the proposed approach on a proof of the mutual exclusion property of the Peterson’s algorithm [11]. We have also demonstrated an application of this approach for proving the mutual exclusion property in the setting of continuous-time models of cyber-physical systems in [8].

Using Mizar [3], in this paper we give a formal proof of the mutual exclusion property of the Peterson’s algorithm in Mizar on the basis of the event-based approach proposed in [2]. Firstly, we define an event-based model of a shared-memory distributed system as a multi-sorted algebraic structure in which sorts are events, processes, locations (i.e. addresses in the shared memory), traces (of the system). The operations of this structure include a binary precedence relation ⩽ on the set of events which turns it into a linear preorder (events are considered simultaneous, if e 1e 2 and e 2e 1), special predicates which check if an event occurs in a given process or trace, predicates which check if an event causes the system to read from or write to a given memory location, and a special partial function “val of” on events which gives the value associated with a memory read or write event (i.e. a value which is written or is read in this event) [2]. Then we define several natural consistency requirements (axioms) for this structure which must hold in every distributed system, e.g. each event occurs in some process, etc. (details are given in [2]).

After this we formulate and prove the main theorem about the mutual exclusion property of the Peterson’s algorithm in an arbitrary consistent algebraic structure of events. Informally, the main theorem states that if a system consists of two processes, and in some trace there occur two events e 1 and e 2 in different processes and each of these events is preceded by a series of three special events (in the same process) guaranteed by execution of the Peterson’s algorithm (setting the flag of the current process, writing the identifier of the opposite process to the “turn” shared variable, and reading zero from the flag of the opposite process or reading the identifier of the current process from the “turn” variable), and moreover, if neither process writes to the flag of the opposite process or writes its own identifier to the “turn” variable, then either the events e 1 and e 2 coincide, or they are not simultaneous (mutual exclusion property).

, Meriläinen J and Eronen M, 2009. Dendroclimatic transfer functions revisited: Little Ice Age and Medieval Warm Period summer temperatures reconstructed using artificial neural networks and linear algoritms. Annales Geophysicae 27: 1097-1111. Kasatkina EA, Shumilov OI and Krąpiec M, 2007. On periodicities in long term climatic variations near 68° N, 30° E. Advances in Geosciences 13: 25-29, DOI 10.5194/adgeo-13-25-2007. Krawczyk AJ and Krąpiec M, 2003a. Annual growth sequences and solar activity cycles (examples from subfossil oaks from Southern Poland). Bulletin of