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 its easier to validate (e.g using code reviews and testing etc.)
• Petra uses theory from formal verification and has been specifically design 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:

Verification

Proves absence of errors. A mathematical / logical process which provides a proof of system correctness. 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 for OOP languages 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. Functional languages are better in this respect however they do not scale well for large systems, which have many sub-systems, and those which are more naturally modelled with objects and/or state, and often the variety/complexity of code written in functional languages leads to systems which are hard to understand and verify.

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 a floatation device. This is addressed by validation. Validation includes review and testing processed which allows stakeholders to gain confidence in the system. Validation is used to increase the likely-hood that a system does what it was intended to do. Code in formal methods must be easy to validate in order for the method to be useful. 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 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 have to perform any manual proof steps and therefore does not have to be an expert in formal methods. The checks have also 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)