South African Computer Journal 1998(22)
http://hdl.handle.net/10500/23896
Thu, 21 Mar 2019 16:10:03 GMT2019-03-21T16:10:03ZpGCL: formal reasoning for random algorithms
http://hdl.handle.net/10500/24296
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.
Thu, 01 Jan 1998 00:00:00 GMThttp://hdl.handle.net/10500/242961998-01-01T00:00:00ZA logic for the design of multiprogramming systems
http://hdl.handle.net/10500/24295
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}.
Thu, 01 Jan 1998 00:00:00 GMThttp://hdl.handle.net/10500/242951998-01-01T00:00:00ZProblem analysis using small problem frames
http://hdl.handle.net/10500/24294
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.
Thu, 01 Jan 1998 00:00:00 GMThttp://hdl.handle.net/10500/242941998-01-01T00:00:00ZTeaching math more effectively, through the design of calculational proofs
http://hdl.handle.net/10500/24293
Teaching math more effectively, through the design of calculational proofs
Gries, D; Schneider, FB
Thu, 01 Jan 1998 00:00:00 GMThttp://hdl.handle.net/10500/242931998-01-01T00:00:00Z