Derivation of data intensive algorithms by formal transformation: the Schorr-Waite graph marking algorithm

De Montfort University Open Research Archive

Show simple item record

dc.contributor.author Ward, Martin
dc.date.accessioned 2005-09-05T19:49:55Z
dc.date.available 2005-09-05T19:49:55Z
dc.date.issued 2005-09-05T19:49:55Z
dc.identifier.citation Ward, M., (1996) Derivation of data intensive algorithms by formal transformation: the Schorr-Waite graph marking algorithm. IEEE Transactions on Software Engineering, 22 (9), pp. 665-686.
dc.identifier.other IR/2005/24
dc.identifier.uri http://hdl.handle.net/2086/47
dc.description Dated September 19, 1996 en
dc.description.abstract In this paper we consider a particular class of algorithms which present certain difficulties to formal verification. These are algorithms which use a single data structure for two or more purposes, which combine program control information with other data structures or which are developed as a combination of a basic idea with an implementation technique. Our approach is based on applying proven semantics-preserving transformation rules in a wide spectrum language. Starting with a set theoretical specification of “reachability” we are able to derive iterative and recursive graph marking algorithms using the “pointer switching” idea of Schorr and Waite. There have been several proofs of correctness of the Schorr-Waite algorithm, and a small number of transformational developments of the algorithm. The great advantage of our approach is that we can derive the algorithm from its specification using only general-purpose transformational rules: without the need for complicated induction arguments. Our approach applies equally well to several more complex algorithms which make use of the pointer switching strategy, including a hybrid algorithm which uses a fixed length stack, switching to the pointer switching strategy when the stack runs out. en
dc.format.extent 407024 bytes
dc.format.extent 349644 bytes
dc.format.mimetype application/pdf
dc.format.mimetype application/postscript
dc.language.iso en en
dc.relation.ispartofseries STRL en
dc.relation.ispartofseries 1996-12 en
dc.subject EPSRC
dc.title Derivation of data intensive algorithms by formal transformation: the Schorr-Waite graph marking algorithm en
dc.type Article en
dc.identifier.doi http://dx.doi.org/10.1109/32.541437
dc.researchgroup Software Technology Research Laboratory (STRL)


Files in this item

This item appears in the following Collection(s)

Show simple item record