Refinement concepts formalised in higher order logic

DOI10.1007/BF01888227zbMath0703.68074MaRDI QIDQ916409

Elsie Sterbin Gottlieb

Publication date: 1990

Published in: Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

refinement calculusweakest preconditionprogram developmentmechanical theorem proving

Mathematics Subject Classification ID

Related Items (7)

A specification-oriented semantics for the refinement of real-time systems ⋮ A predicative semantics for the refinement of real-time systems ⋮ A tactic language for refinement of state-rich concurrent specifications ⋮ From Proposition to Program ⋮ Theories for mechanical proofs of imperative programs ⋮ Real-time refinement in Manna and Pnueli's temporal logic ⋮ Mechanizing some advanced refinement concepts

Uses Software

• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theoretical basis for stepwise refinement and the programming calculus
• Duality in specification languages: A lattice-theoretical approach
• Stepwise refinement of parallel algorithms
• A simple fixpoint argument without the restriction to continuity
• A calculus of refinements for program derivations
• Data refinement of predicate transformers
• Edinburgh LCF. A mechanized logic of computation
• A lattice-theoretical fixpoint theorem and its applications

This page was built for publication: Refinement concepts formalised in higher order logic