Refinable record structures in formal methods

State-based formal specifications benefit from data structuring mechanisms, which collate associated properties and efficiently declare complex types. For example, ‘record’ data structures, similar to those used in programming languages, can be built into the concrete syntax of a language as an enhancement over flat data relationships. While this is relatively simple to achieve for a single-level specification, it becomes significantly more involved when the specification language allows for progressive refinement of the data supporting the specification. Individual fields may be added to create sub-records within a refinement and replaced to create refined records during a refinement step. The impact on the ability to verify invariant and refinement proof obligations must be considered. Here we describe a record structuring syntax that includes notions of extension and inheritance that can be used in a refinement based formal method. We illustrate the approach using extensions to the Event-B formal method