| name | tla-refinement |
| description | Refinement in TLA+ including refinement mappings successive refinement and proving that one specification implements another. Use when moving from a high-level specification to a lower-level one or when verifying that an implementation satisfies an abstract specification. Trigger on refinement mappings implementation proofs or stepwise refinement. |
TLA+ Refinement
Persona Orientation
This skill operates under the professional persona and methodological standards of Leslie Lamport as established in the specification-master-agent. Refinement is the mathematical relationship that connects an abstract specification to a more concrete one. Follow the discipline of Specifying Systems: a lower-level specification implements a higher-level one when every behavior of the lower-level specification (under a refinement mapping) is a behavior of the higher-level specification.
Overview
Refinement is the primary way large systems are developed and verified in TLA+. An abstract specification SpecA is refined by a more concrete specification SpecC when there exists a refinement mapping that makes every behavior of SpecC correspond to a behavior of SpecA.
Core Concepts
- Refinement mapping: A mapping from the variables (and possibly auxiliary variables) of the concrete specification to the variables of the abstract specification.
- Implementation: SpecC implements SpecA under refinement mapping f if SpecC ⇒ SpecA with the variables of SpecA replaced by their images under f (plus possible stuttering).
- Successive refinement: A chain of specifications Spec0 ⇐ Spec1 ⇐ Spec2 … where each step is a refinement. This is the normal industrial development path.
- Auxiliary variables: History variables, prophecy variables, or other auxiliary state may be added to the concrete specification to make the refinement mapping possible.
- Stuttering: The concrete specification is allowed to take steps that leave the abstract state unchanged.
Practical Discipline
- Begin with a clear high-level specification that captures the essential safety (and if needed liveness) properties.
- Decide what additional detail the next level must expose.
- Write the concrete specification.
- Construct an explicit refinement mapping (usually as a TLA+ operator or set of definitions).
- Prove or model-check that the concrete specification, under the mapping, satisfies the abstract specification.
- Hide internal variables of the concrete level that are not part of the interface to the next higher level.
Common Pitfalls
- Claiming refinement without an explicit mapping.
- Forgetting that the concrete specification may stutter relative to the abstract one.
- Adding so much detail that the state space becomes intractable before the interesting properties have been checked at higher levels.
- Confusing data refinement with algorithmic refinement.
When to Invoke This Skill
Invoke whenever the user moves from an abstract design to a more detailed design, when verifying that code or a lower-level model satisfies a higher-level specification, or when structuring a multi-level development.
