Refactoring of B Models

Author

Sonja Holl

Abstract

Refactorings are an efficient way to reduce work and costs compared to manual source code transformations, which are a inherent part in a software development process. In formal specification languages like B, where proofs are involved, require more care than simple syntax tree modifications. In general a proof cannot be done automatically, therefore a good refactoring should avoid breaking the proofs. In this work, we present a method for proof-preserving refactoring of formal models. The main contributions of this work are:

• Data structures needed to transform syntax and proof trees. These structures are graphs representing the trees themselves and dependencies between specifications. Also we introduce several functions to handle relationship between proofs and syntax trees and scoping of syntax tree elements.
• A notion of proof preservation for B specifications. We reduce the problem to discharge a new proof obligation to the problem of discharging the old one. The old proof is used as a black box.
• Several new inference rules for B to simplify reasoning about refactorings.

A catalogue of refactorings that preserve provability.

Advised By

Michael Leuschel, Jens Bendisposto

Download: PDF