Formal basis for the refinement of rule based transition systems

Research output: Contribution to journalArticlepeer-review


This paper makes a contribution to the refinement of systems which involve search by proposing a simple non-deterministic model for rule based transition systems and using this to define a meaning for rule based refinement which allows each stage of the software development path to be verified with respect to the previous stage. The proposal allows a system which involves search to be specified in terms of all the possible outcomes. Each stage of refinement will introduce complexity to the rules and therefore develop the search space in ever more sophisticated ways. At each stage of the refinement it will be possible to be precise about which collections of outcomes have been deleted, thereby achieving a verified (prototype) implementation.
Original languageEnglish
Pages (from-to)329-354
JournalJournal of Functional Programming
Issue number02
Publication statusPublished - 1 Mar 1996


Dive into the research topics of 'Formal basis for the refinement of rule based transition systems'. Together they form a unique fingerprint.

Cite this