Combining angels, demons and miracles in program specifications

DOI10.1016/0304-3975(92)90309-4zbMath0754.68078OpenAlexW1973316014MaRDI QIDQ1199826

S. Singh

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

zbMATH Keywords

angelic nondeterminismdemonic nondeterminismcomplete lattice of monotonic predicate transformersunbounded nondeterminism

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Continuous lattices and posets, applications (06B35)

Related Items (9)

Efficient weakest preconditions ⋮ Predicate transformers as power operations ⋮ Angelic nondeterminism in the unifying theories of programming ⋮ Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism ⋮ The algebra of multirelations ⋮ Joining specification statements ⋮ BGSL: an imperative language for specification and refinement of backtracking programs ⋮ Mechanizing some advanced refinement concepts ⋮ Nondeterministic semantics of compound diagrams

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: Combining angels, demons and miracles in program specifications