The specification statement

From MaRDI portal
Publication:4711615

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/



Related Items

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