The understanding developed in the lectures and exercises of
this School will provide a firm foundation for students
working in many areas of con-temporary Information Science
and Engineering, including: formal methods,formal modeling,
software design by model transformation, program
verification and dependable-system development.
The atmosphere of the School is one in which current
problems and advances are discussed, both in lectures and
during problem sessions, but also in informal discussions
where more speculative topics may be explored. Active
participation is expected.
This School contains two courses. The
Advances Course studies a notation, rCOS, for the
specification, refinement and verification of
component-based and object-oriented designs. The Foundations
Course studies the theory underlying such notations: why the
space of computations is partially ordered by a refinement
relation; and how more complicated computational behaviors
is captured incrementally using Galois connections between
semantic partial orders. That approach is used in the
Advanced Course to introduce the various concepts it
studies. The foundational approach complements that of
Unifying Theories of Programming due to Hoare and He. The
advanced study of rCOS includes an in-depth case study and
tool support.
By studying this pair of courses students
will be able to appreciate the range of techniques currently
advancing the subject, and to study an example of how they
are successfully used. Research topics will also be
suggested.
Background
The
first difficulty confronting Theoretical Computer Science
has been the construction of accurate models of various
computing paradigms. Historically that began with models for
(partial) computable functions in the 1930s with the work of
Turing, Church, Post, Markov, Hilbert and so on. Their
contribution was to show, in differing but equivalent ways,
how to capture the idea of a computation that might not
terminate. This made computations special cases of partial
functions, and provided them with a logic and laws.
Then, with software engineering and
high-level programming, arose levels of design more abstract
than code. Programming is sufficiently difficult that it is
not possible to write down, in one step, programs for
solving nontrivial problems. The purpose of the
partially-ordered spaces of program constructs is to provide
a design space: a framework in which the difficult task of
program design and construction can be achieved rigorously
in a step-wise manner. This is the mathematical and formal
counterpart of the informal graphical notations
optimistically proposed for that purpose.
The designs appearing in design space
featured demonic nondeterminism: if the choice between two
procedures is determined by the value of some local variable
which is hidden, then the choice between the procedures
becomes (demonically) nondeterministic. Thus abstraction
leads to (demonic) nondeterminism, as modeled and exploited
in the design methodologies of Dijkstra and Hoare. They
endowed (sequential) systems with the binary-relation and
the predicate-transformer semantic models, and produced
algebraic laws between programs. The result has been a
theory of algebraic reasoning about, and stepwise derivation
of, programs.
Then as stepwise derivations of
implementations from specifications became more widespread
and familiar, more general kinds of computation became
important because of the role they play at intermediate
stages of development. In that sense they are like the
complex numbers: even if a polynomial has only real roots, a
calculation in the complex field assists in their
derivation; and often, of course, genuinely complex roots
are required. Constructs like unbounded demonic
nondeterminism (i.e. noncontinuous computations), angelic
nondeterminism (dual to demonic nondeterminism) and
unenabled computations (dual to nonterminating computations)
arose from the work of Back, Morgan, Nelson and Morris. The
idea of that work has been to provide a calculus by which
sequential programs can be incrementally derived from their
specifications, by using just laws that have already been
proved sound in the accepted models.
That refinement formalism, known as the
refinement calculus, has since been extended to include
probabilistic computations, concurrency, time (synchronous
and asynchronous), and so on (even including quantum
computation), as well as to the topics in rCOS concerning
object orientation. The importance of such work is not just
that it models new and difficult computational behaviour. It
does so in an incremental manner, lifting previous results.
The purpose of this School is to study just
those methods (in the Foundations Course), and their use in
rCOS (in the Advances Course).
