Introduction

Welcome to the Imandra Protocol Language (IPL) documentation site!

About IPL

Financial markets run on many interconnected systems - ensuring they can effectively and safely understand each other is the fundamental task.

Numerous recent regulatory directives and industry initiatives have called for more ‘rigorous’ testing of trading systems. Ultimately, a Limit order at NYSE is different from a Limit order at BATS. Getting these details correct is very important and the ability to specify precisely behaviours is key to achieving fair and rigorous trading systems.

IPL was designed to be a protocol-independent language for expressing system connectivity specifications. The current libraries implement FIX protocol, but the framework is generic enough to be extended to other protocols.

IPL is an example of a language which provides a Machine-Reasonable API. This means that the model is not only machine readable, but also it is possible to reason about a model written in the language. One can prove properties, known as verification goals about a machine-reasonable language, automatically populate test-cases, and make meta-level statements about it. Machine-Reasonable Regulations are regulations which correspond to statements about which we can automatically reason, given an IPL model.

For more explanation and examples of Machine-Reasonable APIs and Regulations, please consult the following blog posts:

  • Machine Reasonable APIs
  • The Wolf, Goat and Cabbage Exchange

IPL is comprised of the following 4 elements:

  • ability to import libraries - like those containing types and messages of FIX protocol
  • definition of model state
  • specification of how to treat incoming messages and submit new ones
  • formalise how to handle internal system events and their interaction with the state

Each IPL file models a state transition system on the life cycle of one order. If an IPL file is free from errors then it is guaranteed to be able to generate a functioning implementation (see Imandra Markets), which can be analysed automatically, creating automatic test cases and verifications. In order to achieve this IPL has the following features:

  • type inference via a strongly statically typed language. For every expression (and, recursively, its sub-expressions) the type checker deduces its type and makes sure that it is valid in a given context.
  • ability to write block code in an imperative style using if then else constructs
  • internal validity construction verifying that any specification returns messages with all required fields completed
  • provision of an integrated development environment via a sophisticated language server which performs context-specific auto-completion and hover-style documentation

IPL Plugin

In collaboration with TypeFox (the company behind the XText framework), we have developed a plugin supporting the Language Server Protocol (see more at LSP).

  • You can now download IPL VS Code plugin at IPL VS Code Plugin
  • You may also run the IPL plugin with other editors supporting LSP. As of December 2017, the protocol is supported by VS Code, MS Monaco Editor, Eclipse Che, Eclipse IDE, Emacs, GNOME Builder and Vim. For up-to-date list and instructions, see the LSP website.

Documentation Layout

  • Types - introduces types.
  • State - describes how model state is defined and how it may be referenced.
  • Expressions - describes the expression language.
  • Messages and Actions - introduces messages and actions which describe external and internal state transitions.
  • Libraries - descibes the available FIX libraries and how to import them, and if necessary modify any imported artifacts.
  • Tutorials - here we combine the knowledge into concrete examples which can be tested in the language server. They also show the output from an automated analysis by imandra. We recommend this is a good place to start to get acquainted with ipl.
  • Generating documentation - describes the documentation generation feature of the VS Code extension for IPL.