How IPL works

Write a system interface once, precisely. Imandra turns the model into a map of every distinct behaviour, then into tests, simulators and proofs about it.

Speed
A language made for system interfaces: model complex protocols in days, not months.
Precision
Infinite state machines capture the real protocol, edge cases included.
Rigor
Every model can be analysed by Imandra: decomposed, checked, tested and simulated.
Integration is where systems break

The problem

To integrate complex systems safely you have to account for all of their possible interactions. Doing that by hand does not scale.

Virtually infinite interactions
Real systems, especially in finance, admit more message and state combinations than any test plan can list.
Prose specs are ambiguous
Rules of engagement leave edge cases open to interpretation, so every integration reads them differently.
Tests only sample
A handful of hand-written cases stand in for every input the system will see in production.
Simulators drift
Hand-built test venues fall out of step with the real system as soon as the spec changes.
From specification to tests, in six steps

How it works

Encoding an interface in IPL is what makes the rest possible: one precise model, analysed by Imandra, becomes a map, tests, simulators and proofs.

Write the interface as an infinite state machine

An IPL model keeps the structure of a state machine but lets state, messages and actions range over rich data.

  • State: a global record for the session, with as many fields as the protocol needs and explicit initial values.
  • Inbound messages: what a client may send, with validity statements on fields alone and in combination.
  • Actions and outbound messages: internal events such as fills or time changes, and the replies they emit.
IPL state diagram: inbound messages and actions update the state and emit outbound messages
Where you work with IPL

Tools

From the editor to the cloud: the same model in every tool, from writing it to testing against it.

An IDE for precise specifications

Domain-specific hints on hover, context-aware autocompletion, and detailed validation errors and warnings. Once a document validates, it is ready for analysis by Imandra.

Download the VS Code plugin
VS Code: An IDE for precise specifications
Built for writing specs, not just reading them

The language

IPL is strongly typed and editor-aware, so mistakes surface while you write the model rather than during analysis.

Custom library development
IPL allows you to create your own libraries for specific domains and access them with a library command.
Intelligent code autocompletion
Look up available fields and values with built-in editor autocompletion.
Context-aware help
The language will highlight any missing required fields that your model must support.
Local records
Locally declared records with linkable fields to messages and record types from FIX data dictionary.
Float type precisions
Explicitly set Float types (Qty, Price, etc.) precision for your model.
Library Documentation
Access documentation with a mouse-over.
Type checking
IPL is a strongly typed language, making it harder for you to introduce errors.
Validation on duplicate titles
User cannot introduce two fields with the same title - an error will be thrown by the editor.
Custom fields and enums
Extend the standard FIX enums, records, and messages with custom entries.

Model your interfaces with IPL

See IPL on your own specifications, or read how Imandra Connectivity puts it to work.