## Expressions

Expressions define how values can be constructed in the logic of IPL. In this section we describe the general framework of constructing expressions, and show how to reason about them and where this is possible within an IPL model.

We can create values of a certain type, or we can declare a local variable and assign a value to it and it then automatically becomes of this type. For concrete values refer to the examples of literals given in the Basic Types section. Recall for example we can create concrete initial values for fields within the state:

For concrete values of compound types, the name of the type is given with literals corresponding to each of the argument types in brackets. For example the time 8 a.m. can be given as UTCTimeOnly (8, 0, 0, None) - the None in this case is an example of a missing option case - this is discussed further in the section on Optional Types.

For enumeration types it is possible to use only the value provided by the enum. For example with the Side enumeration type one can construct the simple value SellShort. In the case where the names of enumeration cases clash, a typing error may occur in IPL. For example, the Buy entry also appears in the AdvSide enumeration type. In this case the name must be Qualified by writing Side.Buy to denote that this value belongs to the Side enumeration type.

Set Literals can be expressed using the [] notation - for example

#### Fresh values

A keyword in IPL is fresh() which implicitly creates a new value for a particular field, but not one whose precise value we need to know about. A classic example is the ExecID of a sent acknowledgement may need to be generated, but the precise value is not of logical importance, purely that has not appeared before in the model.

For manipulation with numeric values and variables IPL provides one with the standard arithmetic operations +, - (both binary and unary), * and / together with the comparison operators >, <, >= and <=. The equality operator == and its negation != are used to compare values of the same kind. For the Boolean algebra there are &&, || operators, unary negation ! and, useful in certain circumstances, an implication operator ==> and an equivalence operator <==>.

The if-then-else construction can be used as a ternary operator to make an inline conditional expression. The condition, and both conditional branches must be expressions too.

Lastly, one can use a list inclusion in operator to check whether a certain value is present in a list

#### Arithmetic operations

The operators +, -, * and / apply to any number type - in our case float and int. Furthermore, >, <, >= and <= apply in general to any comparable. A comparable type is either an int or a float or a compound datatype with purely number or optional number types. For example one can compare two variables of type UTCTimeOnly(int,int,int,?int):

Further to this, as a special operation it is possible to add elements of type Duration to the type UTCTimeStamp:

More such operators are forthcoming in IPL.

In order to reference fields in the model, IPL uses a Qualified Name convention. For the purposes of this section we demonstrate this using the state, but it applies equally to actions and messages - this is discussed further in the section on Messages and Actions.

When referencing the value of a field such as the Limit field of the state we write state.Limit. To reference an internal record field such as the opening_time field of the venue_times record we write state.venue_times.opening_time.

Recall from the Optional Types are used within IPL to represent information which may not be present. Let us say we are reasoning with the Limit field from the state defined in the section on Defining State:

In order to reason about Limit we need to be able to determine if it is present or not, and if so, make use of its value. IPL includes a special keyword present which can be used as follows

which returns an expression value 1.0 if it is present.

If the value of Limit is not present, then its value is by definition the literal None. If it is present then it contains its value within the constructor Some. We can extract this value by using a case statment as follows:

which returns a boolean expression of equating to true if and only if the Limit field of state if present and its values is greater than 0.0. The variable x is referred to as the capture variable which stores the value in the Limit.

When receiving messages or actions, as described in the section on Messages and Actions it is possible to write imperative style code to describe the desired logic. In general code blocks exist within {} brackets - within code blocks the following code constructs are available:

#### return

This simply exits whatever function the statement lies within

#### if-then-else

These have optional else statements. If there is just one statement after the then or else then there is no need for {}; otherwise this is necessary. Note that if-then-else is valid in both Expressions and statement. The following are all valid examples of if-then-else statements:

#### case

This allow imperative reasoning about case statements. It is possible to exclude either the None case or the Some case, but if both are included, the None case must come first. The following are valid examples of imperative case statements:

#### let

It is possible to define local variables in code blocks. These variables remain within scope of their respective block and are overridden by variable names with the same name in more nested blocks or case statements. Case capture variables such as x above act as local variables in this sense. Types of local variables are not defined and are inferred from their assignment. A local variable must be assigned a value. Valid examples of local variable declarations are

#### assignFrom

This allows all of the fields from the state to be assigned to the fields of an incoming message. We introduced the concept of assignable in the State section. These fields correspond to those in messages, and assignFrom(msg, state) assigns the intersection of the fields in the message msg with those from the internal declaration state.

#### send

It is possible to send an outbound message, as described in the Messages section, it is possible to use the send statement to denote this being send from the venue. It is possible to send the outbound message with all fields explicitly set, or by incorporating the assignable section of an internal state declaration. All of the required fields of an outbound message must be assigned in a send. For example, given an outbound message ExecutionReport which has fields CumQty: float and LeavesQty: float the following are all valid send statements:

If any required fields are missing from the sent outbound message an error will be raised in IPL.