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. They handle basic state and operations.

Strict Base Objects

Strict base objects are limited to primitive fields for simplicity and verifiability.

Fields must be primitive types (like boolean, int, etc.) and non-final, allowing state changes.
No non-primitive fields are allowed.

Non-Strict Base Objects

Non-strict base objects offer more flexibility while still being verifiable.

Fields can be primitive and non-final (for mutable state).
Or, fields can be non-primitive (like other objects) but must be final (immutable references).

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 encourages patterns that enhance observability and modularity in verified code.

Update Reset Pattern

This pattern observes changes to primitive values in strict base objects, where fields are mutable primitives. Use an “update” action to set a new value (e.g., increment a counter), paired with a “reset” action to revert or acknowledge the change (e.g., set a flag back to false after reading). Predicates check for “updated” states (e.g., boolean changed() { return value != initial; }). This allows higher layers to react to primitive mutations in a verifiable way, like in event-driven systems.

Views Pattern

For observing a portion of a large, complex base object, create view classes that reference the base but expose only subsets of its state and actions. A view is a non-base object that uses a single final field to point to parts of the base. The view must pick out disjoint predicates from the base (base objects are allowed to have non-disjoint state predicates). This pattern simplifies reasoning about big bases by focusing verification on relevant slices, improving code reviews and testing.