Petra-Java Dev Guide

Description

A development guide for the Petra-Java programming standard.

A development guide for the Petra-Java programming standard. This guide covers the rules, verification principles, core concepts, and design patterns for writing Petra-compliant Java code, enabling efficient formal verification while keeping code simple and reviewable.

Petra-Java Rules

Petra-Java defines specific rules for structuring Java classes to ensure they can be formally verified. These rules distinguish between base objects (the foundational building blocks) and non-base objects (compositions of base objects). All fields in any object must be private to encapsulate state properly.

Base Objects

Base objects are the core primitives or simple composites in Petra. All base object classes must be annotated with @Base to indicate they follow base rules.

Fields must be primitive types (like boolean, int, etc.) and non-final, allowing state changes.
Base objects can have public boolean methods which overlap i.e. they are allowed to evaluate to true at the same time.

Non-Base Objects

Non-base objects compose base objects hierarchically. They must follow a specific syntax to ensure composability and verifiability. Fields must be private and final, making them immutable references to base or other non-base objects.

Here’s a simple explanation of the syntax rules using bullet points:

A non-base object is a class that contains fields, predicates (boolean methods defining states), and actions (void methods that change state).
Fields are declared as private final Type fieldName = new Type(); – each is a private, final reference to another object instance.
Predicates are boolean methods like boolean stateName() { return expression; } – they define possible states of the object based on its fields.
Actions are void methods like void methodName() { body } – they contain conditional logic to transition between states.
Expressions in predicates can check a field’s state like field.stateName(), or combine them with AND (&&), OR (||), XOR (^), NOT (!), or parentheses for grouping.
States in conditions are like stateName or combined with XOR (^) for mutual exclusivity.
The body of an action can be a sequence of else-if branches, or just an if-statement.
Each branch is like if (precondition) { statements; assert(postcondition); } – checking a starting state, performing changes, and asserting the ending state.
Statements can be parallel blocks like par(() -> { code; }, () -> { code; }) for concurrent execution, sequences separated by ;, or direct calls to change states.
In parallel blocks, use lambdas like () -> { field.methodName(); } to call actions on fields concurrently.

Annotations

Petra uses annotations to guide verification and structure:

@Base: Marks a class as a base object, indicating it follows base rules for primitive or simple state handling. This tells the verifier to treat it as a foundational component.
@Initial: Placed on specific boolean methods (predicates) in a class to indicate the initial state of objects. For example, marking a method like @Initial public boolean off() { ... } means objects start in that state.
@External: Marks classes that don’t follow Petra structure, so the verifier ignores them. Use this for integrating legacy or third-party code that isn’t Petra-compliant.

Petra Verification Rules

Petra verification ensures programs are deterministic, terminate, and meet their contracts. Rules are defined for different components, allowing modular checks.

OBJ

An object (OBJ) is verified as a whole: its fields, predicates, and actions must compose correctly. Verification checks that there is at least one predicate (i.e. state) and that predicates do not overlap (i.e. they each represent a disjoint set of states), and the object actions transition between them reliably.

BASE_OBJ

Base objects require at least one predicate i.e. state.

CASE

A case in an action is an if-branch with pre- and post-conditions. Verification proves that if the pre-condition holds, the statements lead to the post-condition, with no side effects outside this contract. In order for this to be the case the composition of method calls within the case, must catch all the possible values coming through the pre-condition, i.e the pre-condition must fit within the input of this composition. Similarly, the compositions output must fit within the post-condition.

BASE_CASE

In base objects, the cases of each method always have a single state for the post-condition, and at least one state for the pre-condition.

CASES

Multiple cases in a method must have mutually exclusive pre-conditions.

Petra Concepts

Petra allows reasoning about programs one layer at a time, promoting modularity. A layer consists of an object, its private fields (which could be other objects), the object’s methods (predicates and actions), and the methods of its fields. This hierarchical approach means you verify locally: check an object’s predicates are disjoint against it’s state space based on it’s fields states, and actions compose field actions to transition states correctly. Higher layers build on verified lower ones, enabling scalable verification for complex systems.

Petra Design Patterns

Petra requires patterns that enhance observability and modularity, particularly when bridging the gap between formal verification and non-deterministic external environments.

Reactive Update Pattern

This pattern is used to handle non-determinism from external sources (such as LLMs, sensors, or user input) within a verified reactive loop. This pattern can be used to handle any non-determinism, such as reading data from external sources. By isolating external side effects inside an update() method, the rest of the system can react to changes using deterministic safety logic.

How it Works

The Updateable Interface
Base objects (agents) implement Updateable, marking the @External update() method as the point where the outside world influences the system.
State Encapsulation
The agent maintains an internal state (e.g., SET_GREEN, SET_RED) which is mutated by the external call.
Non-Deterministic Predicates
Predicates annotated with @NonDet allow the controller to reason about the agent’s “intent” or “desire” without knowing exactly which path the agent will take until runtime.
The Reactive Loop
The startReactive method continuously triggers these updates, while an EntryPoint (the MAS controller) monitors the agents’ states and enforces global safety invariants.

Code Example: The Traffic Agent

In this example, the TrafficAgent uses an LLM to decide its state. The @External annotation tells Petra that the state change is not controlled by internal logic alone.

@Base
public class TrafficAgent implements Updateable {

    private State status = State.WAITING;
    private final LLM tool = new LLM();

    @Initial
    public boolean noDecision() { return status == State.WAITING; }

    // Non-deterministic predicates evaluated by the Controller
    @NonDet public boolean wantsGreen() { return status == State.SET_GREEN; }
    @NonDet public boolean wantsRed() { return status == State.SET_RED; }

    @Override
    @External
    public void update() {
        try {
            // Call to external LLM tool
            this.status = State.valueOf(tool.askLLM("... respond with SET_GREEN or SET_RED."));
        } catch (Exception e) {
            // Fail-safe logic if the external tool fails
            this.status = State.SET_RED;
        }
        assert(wantsGreen() || wantsRed());
    }

    // ... logic for signaling and resetting
}

Safety Orchestration

The Multi-Agent System (MAS) Controller (below) then evaluates these non-deterministic states. The key point is that in the layer above the agents, the @NonDet states are handled safely. If both the TrafficAgent and a PedestrianAgent simultaneously return wantsGreen(), the controller executes a fail-safe (e.g., trafficAgent.forceRed()) before any physical signal is changed, ensuring the system never enters an unsafe state. The controller defines its own non-deterministic predicates that combine the agents’ desires and enforces global safety invariants before any physical actions are taken. This guarantees that the system never enters an unsafe state, even when external non-determinism (LLMs, sensors, etc.) is involved. For example, if both the TrafficAgent and a PedestrianAgent simultaneously return wantsGreen(), the controller executes a fail-safe (trafficAgent.forceRed()) before any signal is changed.

// --- MAS CONTROLLER ---
public class TrafficControlMAS implements EntryPoint {

    // all base objects must be instantiated as singletons
    private final PedestrianAgent pedestrianAgent = singleton(PedestrianAgent.class);
    private final TrafficAgent trafficAgent = singleton(TrafficAgent.class);

    @Initial
    @NonDet public boolean start() {
        return pedestrianAgent.noDecision() && trafficAgent.noDecision();
    }

    @NonDet public boolean bothWantGreen() {
        return pedestrianAgent.wantsGreen() && trafficAgent.wantsGreen();
    }

    // IMPORTANT: Required to handle failsafe correctly
    @NonDet public boolean bothWantRed() {
        return pedestrianAgent.wantsRed() && trafficAgent.wantsRed();
    }

    @NonDet public boolean bothWantDifferent() {
        return ((pedestrianAgent.wantsRed() && trafficAgent.wantsGreen()) || (pedestrianAgent.wantsGreen() && trafficAgent.wantsRed())) ;
    }

    public boolean signalled() {
        return pedestrianAgent.signalled() && trafficAgent.signalled();
    }

    public void main() {
        if (bothWantGreen()) {
            // handles the non-deterministic bothWantGreen() state using a fail-safe to bothWantDifferent(),
            // which works by forcing the traffic agent to a red light.
            trafficAgent.forceRed();
            assert(bothWantDifferent());
        }
        else if (bothWantDifferent()) {
            seq(()->pedestrianAgent.signal(),()->trafficAgent.signal());
            assert(signalled());
        }
        else if (bothWantRed()) {
            seq(()->pedestrianAgent.signal(),()->trafficAgent.signal());
            assert(signalled());
        }
        else if (signalled()) {
            seq(()->pedestrianAgent.reset(),()->trafficAgent.reset());
            assert(start());
        }
    }
}

Full Code Listing

You can find the complete implementation of this pattern, including the MAS controller and pedestrian agent, here: Pedestrian Crossing MAS Example