Colloquium Details
Nondeterminism as an abstraction mechanism
| Author: | Michal Walicki Institute of Informatics, University of Bergen, Norway |
|---|---|
| Date: | May 17, 2001 |
| Time: | 15:30 |
| Location: | 220 Deschutes |
Abstract
We argue that nondeterminism provides a valuable, and even indispensable, mechanism for specifying programs and reasoning about algorithms at an adequate level of abstraction. The traditional means of abstraction - underspecification - can not achieve the same adequacy when dealing with abstract, which in this context means primarily unordered structures, like sets.
Using an example of a simple graph algorithm we show that the equational language of deterministic functions is insufficient for capturing the intended meaning of the algorithm. We propose a multialgebraic generalization of the algebraic specification framework, which incorporates the phenomenon of nondeterminism. The new framework is illustrated by means of the same example. We also present and discuss a sound and complete logic for reasoning about program specifications involving nondeterminism.
The presentation will try to avoid intricate technicalities and should be accessible to the broad audience with the general knowledge of the basics of theoretical computer science.