b-refine

/z-spec:b-refine - B Refinement

Create or verify a B refinement machine. B-Method's refinement chain (Machine -> Refinement -> Implementation) lets you introduce concrete data structures while provably preserving the abstract machine's properties.

This command has two modes:

1. Create mode (one argument): Generate a refinement .ref from an abstract .mch
2. Verify mode (two arguments): Check that a .ref correctly refines its .mch

Input

Arguments: $ARGUMENTS

Parse arguments:

• One argument (.mch file): create mode — generate a refinement
• Two arguments (.mch + .ref): verify mode — check the refinement
• --imp: Generate an implementation (.imp) instead of a refinement (.ref)

Process

0. Check Prerequisites

Verify probcli is installed:

PROBCLI="${PROBCLI:-$HOME/Applications/ProB/probcli}"
if ! which probcli >/dev/null 2>&1 && [ ! -x "$PROBCLI" ]; then
    echo "PROBCLI_NOT_FOUND"
fi

If probcli not found: Stop and tell the user:

probcli is not installed. Run /z-spec:setup probcli first.

1a. Create Mode

Read the Abstract Machine

Load the .mch file and identify:

• Machine name
• SETS (deferred and enumerated)
• VARIABLES and their types (from INVARIANT)
• OPERATIONS (names, parameters, preconditions, effects)
• Key invariants

Guide the Refinement Strategy

Ask the user what data refinement they want. Common strategies:

Abstract	Concrete	Gluing Invariant
Set	Array + count	ran(array(1..count)) = abstract_set
Partial function	Two parallel arrays	!i.(i:1..count => keys(i) |-> vals(i) : abstract_fn)
Sequence	Array + length	!i.(i:1..length => array(i) = abstract_seq(i))
Enumerated status	Integer code	status = active <=> code = 1
Unbounded NAT	Bounded 0..MAX	concrete_val = abstract_val

If the user doesn't specify, suggest the simplest refinement: same data representation with tighter bounds or minor restructuring.