Mechanizing some advanced refinement concepts

DOI10.1007/BF01383984zbMath0785.68063OpenAlexW3021087793MaRDI QIDQ1309250

T. Långbacka, J. Hekanaho, P. Luostarinen, Joakim von Wright

Publication date: 20 April 1994

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01383984

zbMATH Keywords

program transformationsprogram verificationprogram refinementHOL theorem proversemantics of programming languages

Mathematics Subject Classification ID

Related Items (2)

A tactic language for refinement of state-rich concurrent specifications ⋮ Deriving correctness properties of compiled code

Uses Software

• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theoretical basis for stepwise refinement and the programming calculus
• Prespecification in data refinement
• Refinement concepts formalised in higher order logic
• A calculus of refinements for program derivations
• Laws of data refinement
• Data refinement of predicate transformers
• Combining angels, demons and miracles in program specifications
• A formulation of the simple theory of types

This page was built for publication: Mechanizing some advanced refinement concepts