The specification statement

DOI10.1145/44501.44503zbMath0825.68302OpenAlexW2011444209MaRDI QIDQ4711615

Carroll Morgan

Publication date: 25 June 1992

Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: http://www.acm.org/pubs/contents/journals/toplas/1988-10/

Mathematics Subject Classification ID

Theory of software (68N99)

Related Items (38)

Developments in concurrent Kleene algebra ⋮ A relation algebraic model of robust correctness ⋮ Procedures and atomicity refinement ⋮ An analysis of refinement in an abortive paradigm ⋮ Loop verification with invariants and contracts ⋮ Generalised rely-guarantee concurrency: an algebraic foundation ⋮ Base-type languages: Program design by upper semantic approximation ⋮ A calculus of refinements for program derivations ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm ⋮ Superposition refinement of reactive systems ⋮ On Rely-Guarantee Reasoning ⋮ A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency ⋮ Designing a semantic model for a wide-spectrum language with concurrency ⋮ In praise of algebra ⋮ Using schedulers to test probabilistic distributed systems ⋮ A unification of probabilistic choice within a design-based model of reversible computation ⋮ Mechanised support for sound refinement tactics ⋮ HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier ⋮ Data refinement of predicate transformers ⋮ Predicate transformers and higher-order programs ⋮ Footprints in Local Reasoning ⋮ A single complete rule for data refinement ⋮ Combining angels, demons and miracles in program specifications ⋮ On the lattice of specifications: Applications to a specification methodology ⋮ A formal software development approach using refinement calculus ⋮ A wide-spectrum language for verification of programs on weak memory models ⋮ Abstract implementation of algebraic specifications in a temporal logic language ⋮ The behavioural semantics of Event-B refinement ⋮ Preface ⋮ Action systems, unbounded nondeterminism, and infinite traces ⋮ Exits in the refinement calculus ⋮ An adaptation-complete proof system for local reasoning about cloud storage systems ⋮ Joining specification statements ⋮ Set-Theoretic Models of Computations ⋮ A theory for execution-time derivation in real-time programs ⋮ Coordinating action systems ⋮ The lattice of data refinement

This page was built for publication: The specification statement