Guards, Failure, and Partiality: Dijkstra's Guarded-Command Language Formulated Topologically

摘要

Existing treatments of Dijkstra's guarded-command language treat divergence and failure as equivalent, even though Dijkstra clearly states they are not. We reexamine Dijkstra's language, redefining its denotational semantics with powerdomains formulated in topologi-cal terms. The results refine existing work, give a sound semantics of guards, failure, and divergence for non-flat storage domains, and reveal the important role that general topology plays in program correctness.