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 topological 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.

• Type: Journal
• Year: 2016
• Where: BIRTHDAY
• Authors: David A. Schmidt
• Keywords: Applied Computing, BIRTHDAY 2016