Types and invariants in the refinement calculus

DOI10.1016/0167-6423(90)90024-8zbMath0705.68076OpenAlexW2173852369MaRDI QIDQ918219

Carroll Morgan, Trevor Vickers

Publication date: 1990

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

Full work available at URL: https://doi.org/10.1016/0167-6423(90)90024-8

zbMATH Keywords

invariantsprogram specificationrefinement calculusprogram developmentdata typestype-checking

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01)

Related Items

Combining angels, demons and miracles in program specifications, A theory for execution-time derivation in real-time programs, A formal model of real-time program compilation