https://ir.unisa.ac.za/handle/10500/23886 Mon, 04 May 2026 14:43:05 GMT 2026-05-04T14:43:05Z https://ir.unisa.ac.za/handle/10500/24169 The refinement calculus Morgan, C The refinement calculus, based on weakest preconditions, elaborates imperative program developments as a series of steps linked by a mathematical refinement relation. Specifications and executable code are regarded equally as programs, allowing a gradual transformation from one to the other. The extra generality afforded by admitting specifications as code allows a uniform treatment of procedures, parameters, recursion, data refinement, typing and miracles. Sun, 01 Jan 1995 00:00:00 GMT https://ir.unisa.ac.za/handle/10500/24169 1995-01-01T00:00:00Z https://ir.unisa.ac.za/handle/10500/24157 A gentle introduction to domain theory: domains and powerdomains Goslett, J.; Melton, A This tutorial is a companion paper to the tutorial Denotational Semantics and Domain Theory by Goslett, Hulley, and Melton. The purpose of the earlier tutorial was to present a computationally intuitive introduction to domain theory and denotational semantics. The purpose of this tutorial is to present a mathematically rigorous introduction to domain theory. Thus, we develop the mathematical foundation which was not presented in the earlier tutorial. Though this is a mathematical presentation, it is a gentle introduction with the proofs given in much detail. Sun, 01 Jan 1995 00:00:00 GMT https://ir.unisa.ac.za/handle/10500/24157 1995-01-01T00:00:00Z https://ir.unisa.ac.za/handle/10500/24156 Modal logics for programs Goldblatt, R These lectures provide an introduction to modal logic and its use in formalising reasoning about the behaviour of computational processes. They begin with a general introduction to the syntax, semantics, and proof-theory of modal languages, and their historical origins. There then follows an exposition of some particular formalisms that are particularly relevant to computer science: dynamic logic, the temporal logic of concurrency, the Hennessy­-Milner logic of processes, and the powerful Mu-Calculus that encompasses all of these systems. The third part explains technical methods (canonical models, filtrations) that have been developed to analyse particular logics, and finally, these methods are applied to give a proof of the completeness theorem for linear temporal logic. Sun, 01 Jan 1995 00:00:00 GMT https://ir.unisa.ac.za/handle/10500/24156 1995-01-01T00:00:00Z https://ir.unisa.ac.za/handle/10500/24155 Functionality decomposition by compositional correctness preserving transformation Brinksma, E; Langerak, R We present an algorithm for the decomposition of processes in a process algebraic framework. Decomposition, or the refinement of process substructure, is an important design principle in the top-down development of concurrent systems. In the approach that we follow the decomposition is based on a given partition of the actions of a system specification, such that for each partition class a subprocess must be created that realizes the actions in that class. In addition, a suitable synchronization structure between the subprocesses must be present to ensure that the composite behaviour of the subprocesses is properly related to the behaviour of the original specification. We present our results for the process-algebraic specification language LOTOS and give a compositional algorithm for the transformation of the original specification into the required subprocesses. The resulting specification is observation congruent with the original, and, interestingly enough, the subprocesses inherit much of the structure of the original specification. The correctness preserving transformation has been implemented in a tool and has been used for the derivation of protocol specifications from formal descriptions of the desired service. This is possible as it can be shown that the required synchronization mechanisms between the subprocesses can be readily implemented over (reliable) asynchronous media. Sun, 01 Jan 1995 00:00:00 GMT https://ir.unisa.ac.za/handle/10500/24155 1995-01-01T00:00:00Z