Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: gavan@za.ac.uct.mth.elc (Gavan Tredoux)
Message-Id: <9303241740.AA02704@elc.mth.uct.ac.za>
Subject: Prog. logics monograph available
To: info-hol@edu.uidaho.cs.ted (Info-hol mailing list)
Date: Wed, 24 Mar 93 19:40:06 EET


The following monograph is now available by anonymous
ftp, at the node elc.mth.uct.ac.za, as the file
pub/hol/monograph.dvi.Z 

As the filename indicates, this is in TeX dvi format,
compressed. Uncompress using the unix "uncompress"
utility.

The complete hol source is available as the file
pub/hol/prog_logic92.tar.Z 

The source can be extracted from this file using the command
"uncompress -c prog_logic92.tar.Z | tar xvf -" Note that
HOL88 ver 2.01 is required.

Abstract: "Mechanizing nondeterministic programming logics
	   in higher-order logic"
	   G. Tredoux, University of Cape Town, March 1993.

This monograph describes a mechanization of a number of
nondeterministic programming logics in the theorem prover Higher Order
Logic (HOL). The semantics of an unboundedly nondeterministic
programming language, the Partial Guarded Command language -- which
includes partial commands, nondeterministic choice, `random assignment'
and recursion -- is defined in the HOL logic.  Information about
intermediate states is provided by the semantics, which is based on
execution sequences. Failed computation is distinguished from divergent
computation; so that terminated, failed and divergent computations are
expressible in the semantics. No restriction is placed on possible
nondeterminism, which may be bounded, countable or uncountable.  Two
additional languages are defined, and it is shown that one contains
only total, deterministic commands, while the other contains only total
commands. Moreover, it is proved that the three languages defined may
be arranged hierarchically, as semantic subsets of each other.  The
programming logics emerge as derived rules of inference of the HOL
logic, forming a conservative extension of it, guaranteed to preserve
consistency. The following logics are derived: Dijkstra's calculus of
predicate transformers, Hoare logics for partial and total correctness,
a novel logic of invariant relations, and a temporal logic. The
derivation provides a soundness proof of these logics, establishing the
reasonableness of the semantics, and hopes to lay the foundation for
support, within the HOL environment, of mechanized proofs of program
correctness.

162 pages.