PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 12

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available remote Using Hoare Logic in a Process Algebra Setting
Bergstra J. A., Middelburg C. A.
Fundamenta Informaticae
|
2021
|
Vol. 179, nr 4
321--344
EN
This paper concerns the relation between process algebra and Hoare logic. We investigate the question whether and how a Hoare logic can be used for reasoning about how data change in the course of a process when reasoning equationally about that process. We introduce an extension of ACP (Algebra of Communicating Processes) with features that are relevant to processes in which data are involved, present a Hoare logic for the processes considered in this process algebra, and discuss the use of this Hoare logic as a complement to pure equational reasoning with the equational axioms of the process algebra.
2
Content available remote Contradiction-Tolerant Process Algebra with Propositional Signals
Bergstra J. A., Middelburg C. A.
Fundamenta Informaticae
|
2017
|
Vol. 153, nr 1/2
29--55
EN
In a previous paper, an ACP-style process algebra was proposed in which propositions are used as the visible part of the state of processes and as state conditions under which processes may proceed. This process algebra, called ACPps, is built on classical propositional logic. In this paper, we present a version of ACPps built on a paraconsistent propositional logic which is essentially the same as CLuNs. There are many systems that would have to deal with selfcontradictory states if no special measures were taken. For a number of these systems, it is conceivable that accepting self-contradictory states and dealing with them in a way based on a paraconsistent logic is an alternative to taking special measures. The presented version of ACPps can be suited for the description and analysis of systems that deal with self-contradictory states in a way based on the above-mentioned paraconsistent logic.
3
Content available remote Instruction Sequence Size Complexity of Parity
Bergstra J. A., Middelburg C. A.
Fundamenta Informaticae
|
2016
|
Vol. 149, nr 3
297--309
EN
Each Boolean function can be computed by a single-pass instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. Auxiliary Boolean registers are not necessary for this. In the current paper, we show that, in the case of the parity functions, shorter instruction sequences are possible with the use of an auxiliary Boolean register in the presence of instructions to complement the content of auxiliary Boolean registers. This result supports, in a setting where programs are instruction sequences acting on Boolean registers, a basic intuition behind the storage of auxiliary data, namely the intuition that this makes possible a reduction of the size of a program. The work presented in this paper is carried out in the setting of PGA (ProGram Algebra).
4
Content available remote On Algorithmic Equivalence of Instruction Sequences for Computing Bit String Functions
Bergstra J. A., Middelburg C. A.
Fundamenta Informaticae
|
2015
|
Vol. 138, nr 4
411--434
EN
Every partial function from bit strings of a given length to bit strings of a possibly different given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a termination instruction. We look for an equivalence relation on instruction sequences of this kind that captures to a reasonable degree the intuitive notion that two instruction sequences express the same algorithm.
5
Content available remote Data Linkage Algebra, Data Linkage Dynamics, and Priority Rewriting
Bergstra J.A., Middelburg C.A.
Fundamenta Informaticae
|
2013
|
Vol. 128, nr 4
367--412
EN
We introduce an algebra of data linkages. Data linkages are intended for modelling the states of computations in which dynamic data structures are involved. We present a simple model of computation in which states of computations are modelled as data linkages and state changes take place by means of certain actions. We describe the state changes and replies that result from performing those actions by means of a term rewriting system with rule priorities. The model in question is an upgrade of molecular dynamics. The upgrading is mainly concerned with the features to deal with values and the features to reclaim garbage.
6
Content available remote On the Behaviours Produced by Instruction Sequences under Execution
Bergstra J.A., Middelburg C.A.
Fundamenta Informaticae
|
2012
|
Vol. 120, nr 2
111-144
EN
We study several aspects of the behaviours produced by instruction sequences under execution in the setting of the algebraic theory of processes known as ACP. We use ACP to describe the behaviours produced by instruction sequences under execution and to describe two protocols implementing these behaviours in the case where the processing of instructions takes place remotely. We also show that all finite-state behaviours considered in ACP can be produced by instruction sequences under execution.
7
Content available remote Data Linkage Dynamics with Shedding
Bergstra J.A., Middelburg C.A.
Fundamenta Informaticae
|
2010
|
Vol. 103, nr 1-4
31-52
EN
We study shedding in the setting of data linkage dynamics, a simple model of computation that bears on the use of dynamic data structures in programming. Shedding is complementary to garbage collection. With shedding, each time a link to a data object is updated by a program, it is determined whether or not the link will possibly be used once again by the program, and if not the link is automatically removed. Thus, everything is made garbage as soon as it can be viewed as garbage. By that, the effectiveness of garbage collection becomes maximal.
8
Content available remote An Interface Group for Process Components
Bergstra J.A., Middelburg C.A.
Fundamenta Informaticae
|
2010
|
Vol. 99, nr 4
335-382
EN
We take a process component as a pair of an interface and a behaviour. We study the composition of interacting process components in the setting of process algebra. We formalize the interfaces of interacting process components by means of an interface group. An interesting feature of the interface group is that it allows for distinguishing between expectations and promises in interfaces of process components. This distinction comes into play in case components with both client and server behaviour are involved.
9
Content available remote Instruction Sequences with Dynamically Instantiated Instructions
Bergstra J.A., Middelburg C.A.
Fundamenta Informaticae
|
2009
|
Vol. 96, nr 1/2
27-48
EN
We study sequential programs that are instruction sequences with dynamically instantiated instructions. We define the meaning of such programs in two different ways. In either case, we give a translation by which each program with dynamically instantiated instructions is turned into a program without them that exhibits on execution the same behaviour by interaction with some service. The complexity of the translations differ considerably, whereas the services concerned are equally simple. However, the service concerned in the case of the simpler translation is far more powerful than the service concerned in the other case.
10
Content available remote Maurer Computers with Single-Thread Control
Bergstra J.A., Middelburg C.A.
Fundamenta Informaticae
|
2007
|
Vol. 80, nr 4
333-362
EN
We investigate basic issues concerning stored threads and their execution, building upon Maurer's model for computers and the thread algebra of Bergstra et al. We show among other things that a single thread can control the execution on a Maurer machine of any executable finite-state thread stored in the memory of the Maurer machine. We also relate stored threads with programs as considered in the program algebra of Bergstra et al. The work is intended as a preparation for the development of a formal approach to model micro-architectures and to verify their correctness and anticipated speed-up results.
11
Content available remote Thread Algebra with Multi-Level Strategies
Bergstra J.A., Middelburg C.A.
Fundamenta Informaticae
|
2006
|
Vol. 71, nr 2,3
153-182
EN
In a previous paper, we developed an algebraic theory about threads and multi-threading based on the assumption that a deterministic interleaving strategy determines how threads are interleaved. The theory includes interleaving operators for a number of plausible deterministic interleaving strategies. The interleaving of different threads constitutes a multi-thread. Several multi-threads may exist concurrently on a single host in a network, several host behaviors may exist concurrently in a single network on the internet, etc. In the current paper, we assume that the above-mentioned kind of interleaving is also present at these other levels. We extend the theory developed so far with features to cover the multi-level case. We use the resulting theory to develop a simplified formal representation schema of systems that consist of several multi-threaded programs on various hosts in different networks. We also investigate the connections of the resulting theory with the algebraic theory of processes known as ACP.
12
Content available remote Located Actions in Process Algebra with Timing
Bergstra J.A., Middelburg C.A.
Fundamenta Informaticae
|
2004
|
Vol. 61, nr 3,4
183--211
EN
We propose a process algebra obtained by adapting the process algebra with continuous relative timing from Baeten and Middelburg [Process Algebra with Timing, Springer, 2002, Chap. 4] to spatially located actions. This process algebra makes it possible to deal with the behaviour of systems with a known time-dependent spatial distribution, such as protocols transmitting data via a mobile intermediate station. It is a reformulation of the real space process algebra from Baeten and Bergstra [Formal Aspects of Computing, 5, 1993, 481-529] in a setting with urgent actions. This leads to many simplifications.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.