b-create

/z-spec:b-create - Create B Machine

You are creating a B Abstract Machine Notation (AMN) specification. B machines are executable formal specifications that can be type-checked, animated, model-checked, and refined toward implementation --- all using probcli.

This command has two modes:

1. Description mode: Create a B machine from a natural language description
2. Translation mode: Translate an existing Z specification (.tex) to a B machine

Input

Hint: $ARGUMENTS

Determine the mode:

• If the argument is a path to a .tex file: translation mode
• Otherwise: description mode (treat as natural language description)

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.

1. Create specs/ Directory

mkdir -p specs

Update .gitignore if needed:

for pattern in "specs/*.prob" "specs/*.prob2project"; do
    grep -qxF "$pattern" .gitignore 2>/dev/null || echo "$pattern" >> .gitignore
done

2a. Description Mode

If working from a natural language description:

Analyze the Description

Extract:

• Entities: What things does the system track?
• Attributes: What properties do entities have?
• Constraints: What must always be true?
• Operations: What state transitions exist?
• Relationships: How do entities relate to each other?

Generate the Machine

Create a .mch file following this structure:

MACHINE MachineName

SETS
    /* Deferred sets for entity identifiers */
    ID;
    /* Enumerated sets for status values */
    STATUS = {active, inactive}

CONSTANTS
    max_capacity

PROPERTIES
    max_capacity : NAT &
    max_capacity = 100

VARIABLES
    /* State variables */
    entries,
    statuses

INVARIANT
    /* Typing constraints */
    entries : ID +-> NAT &
    statuses : ID +-> STATUS &
    /* Domain consistency */
    dom(entries) = dom(statuses) &
    /* Business invariants */
    card(entries) <= max_capacity

INITIALISATION
    entries := {} ||
    statuses := {}

OPERATIONS
    /* Operations with PRE/THEN substitutions */
    add(id, val) =
        PRE id : ID & val : NAT &
            id /: dom(entries) &
            card(entries) < max_capacity
        THEN
            entries := entries \/ {id |-> val} ||
            statuses := statuses \/ {id |-> active}
        END;

    remove(id) =
        PRE id : ID & id : dom(entries)
        THEN
            entries := {id} <<| entries ||
            statuses := {id} <<| statuses
        END;

    nn <-- count =
        nn := card(entries)
END