Welcome to the Imandra Protocol Language (IPL) documentation site!
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 spefications. 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:
IPL is comprised of the following 4 elements:
- Ability to import libraries - like those containing types and messages of FIX protocol
- Define model state
- Describe how to treat incoming messages and submit new ones
- Describe 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 if 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:
- A strongly statically typed language with type inference. For every expression (and, recursively, its sub-expressions) the typechecker 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
- Language Server features which perform context-specific auto-completion and hover-style documentation
- 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.
- 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.