What is Petra?

An introduction to the Petra programming standard. A new way to structure OOP programs which enables efficient and comprehensive formal verification, whilst simplifying code so that it’s easier to validate using code reviews and testing.

What is Petra?

• A new way to structure OOP programs which enables efficient and comprehensive formal verification, whilst simplifying code so that it’s easier to validate (e.g using code reviews and testing)
• Petra uses theory from formal verification and has been specifically designed from the ground up to be a formal method and a programming language.
• petra-verifier is the first implementation of the Petra verifier, which verifies Java 8 OOP programs written in the Petra standard subset of Java 8.

How to program in Petra?

There are some notions in Petra which should be understood in order to learn Petra more easily:

Formal Verification

Proves absence of errors. To prove the absence of errors, engineers must move from testing to Formal Verification. This is the process of using mathematical proofs to verify the correctness of a system, i.e. that a system behaves correctly according to its specifications across all possible inputs. In simple terms Formal Verification is a logical consistency check that identifies fundamental structural issues within the system, performed in an exhaustive way that testing cannot achieve. Formal verification finds all possible logical errors including deep, edge-case violations that are often invisible to the naked eye, which are missed by informal engineering practices and tooling. Because it is impossible to test every possible combination of inputs, states, and environments, testing can demonstrate the presence of bugs, but never their absence. Correctness is defined by the verification system, for example the Java compiler can verify that a typed variable cannot be assigned to a value of the wrong type. Compilers in general only provide a weak set of guarantees and these do not easily relate to the behaviour of a program with respect to a domain problem.

Validation

Proves presence of errors. Formal verification methods aim to provide very strong correctness guarantees, however even a comprehensively verified system can still go wrong, if there is a mismatch between the system and the context it is being used in. For example a verified automobile should not be used as means of travelling through water. This is addressed by validation. Validation includes review and testing processes which allows stakeholders to gain confidence in the system. Validation is used to increase the likelihood that a system does what it was intended to do. In order to unlock the power of formal methods, the formally verified code must be easy for humans to understand for validation purposes. This requires the code to be as modular as possible (for testing) and as close to natural language as possible (for reviews).

V&V

Verification and Validation (V&V) are both required to ensure systems meet the expectation of stakeholders.

Top down / Bottom up reasoning

Petra composes programs using a hierarchical composition of both data and control flow. When programming it can be useful to think in terms of both top-down decomposition of a domain and bottom-up composition of abstractions over primitive values.

Petra’s features

Petra’s defining feature is the radical unification of formal specifications and programming, a design philosophy that collapses the boundary between abstract mathematical intent and executable code. Unlike traditional systems such as OpenJML, which rely on external annotation languages—essentially “layering” formal logic onto standard code via comments—Petra treats specifications as the primary language of architecture. In the provided Light example (below), the off() and on() methods function simultaneously as executable code and formal state predicates, while the toggle() method serves as a verifiable state transition. Because these definitions are baked into the core structure, the compiler acts as a formal verifier: it does not merely run the code, but mathematically proves that every execution path in toggle() satisfies the assert post-conditions. Consequently, the act of writing the program is the act of constructing a proof; the system ensures correctness by construction, rejecting any logic that could lead to an invalid state.

Petra provides strong correctness guarantees which include: Determinism for both sequential and parallel stateful programs (which means programs behave like functions) and Reachability of states (all methods guarantee that given an input, the method terminates and the result is an output, as specified by the method’s contract pre- and post-conditions). These checks are fully automated so the developer does not have to perform any manual proof steps and therefore does not have to be an expert in formal methods. The checks have also been designed to be efficient to compute such that they scale well for systems of any size. In addition, Petra offers a fluid way to express domain problems within code in a way that allows for domain level instructions to be verified, and Petra code can directly translate into a controlled English, which is a subset of English which is used to remove ambiguity.

Example: Light System

Main

This is used to start a Petra system.

import static com.cognitionbox.petra.ast.interp.util.Program.start;

public class Main {
    public static void main(String[] args){
        new Light().run();
    }
}

Light (entry point)

public final class Light {
  private final Power power = new Power();
  private final Control control = new Control();

  @Initial
  public boolean off() { return power.on() && control.off(); }
  public boolean on() { return power.on() && control.on(); }

  public void toggle() {
    if (off()){
      control.turnOn();
      assert(on());
    } else if (on()){
      control.turnOff();
      assert(off());
    }
  }
}

Power

@Base public final class Power {
  private boolean bool = true;

  public boolean off() { return bool==false; }
  @Initial
  public boolean on() { return bool==true; }

  public void turnOn() {
    if (on() || off()){
      bool=true;
      assert(on());
    }
  }

  public void turnOff() {
    if (on() || off()){
      bool=false;
      assert(off());
    }
  }
}

Control

@Base public final class Control {
  private boolean bool = false;

  @Initial
  public boolean off() { return bool==false; }
  public boolean on() { return bool==true; }

  public void turnOn() {
    if (on() || off()){
      bool=true;
      assert(on());
    }
  }

  public void turnOff() {
    if (on() || off()){
      bool=false;
      assert(off());
    }
  }
}

Explanation

The state symbolic space of the Light object is given by the Cartesian product of the symbolic states of Power and Control (which are defined by the boolean methods) i.e. Power = {on,off} and Control = {on,off} therefore Light = Power X Control = {(on,on), (on,off), (off,on), (off,off)}. The toggle method has two cases, one for going from off to on and the other from on to off. Each case is correct as the composition of method calls in each result in transitions which respect the pre/post conditions of the case. This is also true for the methods in the Power and Control objects.

Use Cases

Petra is well suited to back-end server processing, including but not limited to: modelling and execution of critical workflows for business processes, AI, machine learning, smart contract execution, blockchain applications, infrastructure orchestration and task coordination.

Further reading

• Read Petra Case Study (Algorithmic Trading)