Combining angels, demons and miracles in program specifications
From MaRDI portal
Publication:1199826
DOI10.1016/0304-3975(92)90309-4zbMath0754.68078MaRDI QIDQ1199826
Publication date: 17 January 1993
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(92)90309-4
angelic nondeterminism; demonic nondeterminism; complete lattice of monotonic predicate transformers; unbounded nondeterminism
68Q55: Semantics in the theory of computing
68Q60: Specification and verification (program logics, model checking, etc.)
06B35: Continuous lattices and posets, applications
Cites Work
- A theoretical basis for stepwise refinement and the programming calculus
- Command algebras, recursion and program transformation
- Duality in specification languages: A lattice-theoretical approach
- Types and invariants in the refinement calculus
- A theory for nondeterminism, parallelism, communication, and concurrency
- A calculus of refinements for program derivations
- On correct refinement of programs
- A generalization of Naundorf's fixpoint theorem
- General correctness: A unification of partial and total correctness
- Laws of programming
- The specification statement
- Programming as a Discipline of Mathematical Nature
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
