A theoretical basis for stepwise refinement and the programming calculus

From MaRDI portal
Publication:578892

DOI10.1016/0167-6423(87)90011-6zbMath0624.68017OpenAlexW2087713039MaRDI QIDQ578892

Joseph M. Morris

Publication date: 1987

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0167-6423(87)90011-6



Related Items

The weakest precondition calculus: Recursion and duality, A relation algebraic model of robust correctness, Procedures and atomicity refinement, Building Specifications in the Event-B Institution, Verification conditions are code, Generalised rely-guarantee concurrency: an algebraic foundation, Safety and progress of recursive procedures, A calculus of refinements for program derivations, Superposition refinement of reactive systems, A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency, Unifying Theories of Programming in Isabelle, Balancing expressiveness in formal approaches to concurrency, Stepwise refinement of heap-manipulating code in Chalice, Modular verification for shared-variable concurrent programs, Verification of distributed systems with local-global predicates, Compositional noninterference from first principles, Refinement concepts formalised in higher order logic, Linking theories in probabilistic programming, Data refinement of predicate transformers, Processes and formalisms for unbounded choice, Weakest precondition semantics for time and concurrency, Combining angels, demons and miracles in program specifications, Angelic processes for CSP via the UTP, On the lattice of specifications: Applications to a specification methodology, The algebra of multirelations, Unifying theories of reactive design contracts, A formal software development approach using refinement calculus, Abstractions of non-interference security: probabilistic versus possibilistic, Dual unbounded nondeterminacy, recursion, and fixpoints, Preface, Action systems, unbounded nondeterminism, and infinite traces, Exits in the refinement calculus, Angelicism in the Theory of Reactive Processes, A UTP semantics for \textsf{Circus}, Set-Theoretic Models of Computations, Relational demonic fuzzy refinement, Coordinating action systems, Contracts, games, and refinement., Mechanizing some advanced refinement concepts, Nondeterminacy and recursion via stacks and games, Normal form approach to compiler design, The lattice of data refinement