https://ir.unisa.ac.za/handle/10500/23896 2026-05-02T18:31:56Z 2026-05-02T18:31:56Z Morgan, C McI, A https://ir.unisa.ac.za/handle/10500/24296 2018-06-07T01:00:49Z 1998-01-01T00:00:00Z

pGCL: formal reasoning for random algorithms Morgan, C; McI, A Dijkstra's guarded-command language GCL contains explicit 'demonic' nondeterminism, representing abstraction from (or ignorance of ) which of two program fragments will be executed. We introduce probabilistic nondeterminism to the language, calling the result pGCL. Important is that both forms of nondeterminism are present - both demonic and probabilistic: unlike earlier approaches, we do not deal only with one or the other. The programming logic of 'weakest preconditions' for GCL becomes a logic of 'greatest pre-expectations' for pGCL: we embed predicates (Boolean-valued expressions over state variables) into arithmetic by writing [P], an expression that is 1 when P holds and 0 when it does not. Thus in a trivial sense [P] is the probability that P is true, and such embedded predicates are the basis for the more elaborate arithmetic expressions that we call "expectations". pGCL is suitable for describing random algorithms, at least over discrete distributions. In our presentation of it and its logic we give two examples: an erratic 'sequence accumulator', that fails with·some probability to move along the sequence; and Rabin's 'choice-coordination' algorithm. The first illustrates probabilistic invariants; the second illustrates probabilistic variants.

1998-01-01T00:00:00Z Misra, J https://ir.unisa.ac.za/handle/10500/24295 2018-06-07T01:01:18Z 1998-01-01T00:00:00Z

A logic for the design of multiprogramming systems Misra, J This paper presents a short introduction to the UNITY logic, a fragment of linear temporal logic. The logic was designed to specify safety and progress properties of reactive systems. A version of the UNITY logic appears in {1}. There have been several changes in this logic since then; a full account is available at http:// www.cs.utexas.edu/users/psp/newunity.html, and the essential ideas have appeared in {5, 4}.

1998-01-01T00:00:00Z Jackson, MA https://ir.unisa.ac.za/handle/10500/24294 2018-06-07T01:01:06Z 1998-01-01T00:00:00Z

Problem analysis using small problem frames Jackson, MA The notion of a problem frame is introduced and explained, and its use in analysing and structuring problems is illustrated. A problem frame characterises a class of simple problem. Realistic problems are seen as compositions of simple problems of recognised classes corresponding to known frames.

1998-01-01T00:00:00Z Gries, D Schneider, FB https://ir.unisa.ac.za/handle/10500/24293 2018-06-07T01:00:43Z 1998-01-01T00:00:00Z

Teaching math more effectively, through the design of calculational proofs Gries, D; Schneider, FB

1998-01-01T00:00:00Z