Welcome to the Imandra Protocol Language (IPL) documentation site!
Please note that this website is work-in-progress. All comments and requests are always welcome! Please email us at email@example.com
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.
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 - introduce types
- State - how model state is defined and how it may be referenced later
- Expressions - describes expression language
- Messages and Actions - messages and actions describe external and internal state transitions
- 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.