Reuse of Specification Patterns with the B Method

TL;DR

This paper presents a method for reusing formal specification patterns in the B method, including composition techniques and proof reuse, to improve modularity and efficiency in formal specifications.

Contribution

It introduces a structured approach for reusing and composing specification patterns within the B method, including proof reuse strategies.

Findings

Defined three levels of pattern composition: juxtaposition, linking, unification.

Demonstrated how to instantiate and reuse specification patterns in B.

Showcased reuse of associated proofs for efficiency.

Abstract

This paper describes an approach for reusing specification patterns. Specification patterns are design patterns that are expressed in a formal specification language. Reusing a specification pattern means instantiating it or composing it with other specification patterns. Three levels of composition are defined: juxtaposition, composition with inter-patterns links and unification. This paper shows through examples how to define specification patterns in B, how to reuse them directly in B, and also how to reuse the proofs associated with specification patterns.