Combining angels, demons and miracles in program specifications
The work
| Authors | R.J.R. Back; J. von Wright |
|---|---|
| Type | article |
| Year | 1992 |
| Citekey | back1992combining |
Where it appeared
| Published in | Theoretical Computer Science |
|---|---|
| Publisher | Elsevier |
| Volume | 100 |
| Issue | 2 |
| Pages | 365--383 |
Identifiers
| DOI | 10.1016/0304-3975(92)90309-4 |
|---|---|
| OpenAlex | W1973316014 |
Access
| Landing page | https://doi.org/10.1016/0304-3975(92)90309-4 |
|---|
Abstract
The complete lattice of monotonic predicate transformers is interpreted as a command language with a weakest precondition semantics. This command lattice contains Dijkstra’s guarded commands as well as miracles. It also permits unbounded nondeterminism and angelic nondeterminism. The language is divided into sublanguages using criteria of demonic and angelic nondeterminism, termination and absence of miracles. We investigate dualities between the sublanguages and how they can be generated from simple primitive commands. The notions of total correctness and refinement are generalized to the command lattice.
A copy is held
pdf, 1.2 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | import via drheap-program-correctness |
|---|---|
| Added | 2026-08-19 00:00 UTC |
| Approved by | a person 2026-08-21 22:06 UTC |
Filed under
Cite it as
@article{back1992combining,
title = {Combining angels, demons and miracles in program specifications},
author = {R.J.R. Back and J. von Wright},
year = {1992},
journal = {Theoretical Computer Science},
volume = {100},
number = {2},
pages = {365--383},
publisher = {Elsevier},
doi = {10.1016/0304-3975(92)90309-4},
}
This record lives at https://refs.drheap.org/back1992combining/ and will keep doing so.