phyllis@utcsrgv.UUCP (Phyllis Eve Bregman) (05/17/84)
[****]
UofT Department of Computer Science Seminar Schedule for
the week of May 14th, 1984
May 17th, 4:00 P.M., GB244, Jeffrey Zucker, SUNY: "Program
correctness over abstract data structures, with error-state
semantics".
ABSTRACT: We extend the classical work on program correctness
for Hoare-style proof systems in two ways:
(a) We consider programs over not just integers, but abstract
data structures; in fact over classes of many-sorted structures
of a given signature, one sort of which will be numerical. In the
case of programs with recursive procedures, proof of expressivity
of the assertion language requires an investigation of computability
over abstract structures.
(b) The semantics are designed so as to model errors arising from
uninitialized variables. If such a variable is called in the course
of a computation, the computation will halt in an "error state".
Similarly, any expression containing such a variable may, on
evaluation, yield the "unspecified value". In particular,
considering Boolean expressions, we are led to a three-valued logic.
--
Phyllis Eve Bregman
CSRG, Univ. of Toronto
{decvax,linus,ihnp4,uw-beaver,allegra,utzoo}!utcsrgv!phyllis
CSNET: phyllis@toronto
(416) 978 6985