Expressions - lgwagner/SpeAR GitHub Wiki
SpeAR's expression language supports basic logic, arithmetic, and relational expressions amongst booleans, integers, and real typed variables, in addition to a rich set of temporal operations that are useful for describing how the inputs and outputs of a specification relate to each other. The following subsections describe and provide examples of how to use each possible expression in the SpeAR language.
Literal expression are constant expression values for primitive types. The following example shows some constants which are set to integer, boolean, or real literal values.
Id expression are used to reference existing variables, constants, macros, or enumeration values. The following example shows how to use ID expressions to reference existing elements of a specification.
If/Then/Else expression are useful for assigning a value conditionally. The following example shows how to assign a conditional value to an integer macro m1.
Often times it is necessary to describe what the value for a computed variable is on the initial step of computation. This can be accomplished using the initially expression. The following example shows how to use initially to define the initial value of a variable x.
When writing a specification it is useful to refer to the previous value of a variable in a specification to determine if some interesting change has occurred. Previous expressions are used to accomplish this. Previous expressions can be used on a variable of any type, and allow the user to optionally specify the value of the previous expression on the initial state. In the following example the previous expression is used with and without the optional initial value expression.
Note: a previous expression without an initial value is accompanied with a warning. This is because the value of this expression is not defined on the initial state and may cause properties to fail during logical entailment, logical consistency, and realizability analyses to fail.
Past-time Linear Temporal Logic (PLTL) are useful for describing temporal properties that are similar to standard LTL, but instead, focus only on describing temporal orderings in the system from the first state of execution up to the current state. SpeAR supports PLTL operators once, historically, triggers, and since.
The historically operator is a predicate that captures whether or not the contained expression has been true for every step ofthe execution of the system. In the following example, the macro e1 expresses whether or not a has been less than 10 historically, or for all steps of execution from the beginning state, to the current state.
The once operator is a predicate that captures whether or not the contained expression has been true one or more time throughout the execution of the system. In the following example, the macro e2 expresses whether or not a has been greater than 10 at least once, or for all steps of execution from the beginning state, to the current state.
The since operator is binary expression that captures whether or not the first expression has been true, since the second expression was last true. In the following example, the macro e3 expresses whether or not a has been less than 1000 since b was equal to 0.
The triggers operator is a binary expression that captures whether or not after both expressions are true, that the second expression remains true. In the following example, the macro e4 expresses whether or not after a is greater than 10 and b less than 50 simultaneously (both expressions) that b remains less than 50.
These temporal expressions are simply convenient re-writes of the previously defined PLTL expressions. They do not offer functionality that could not already be defined by users using PLTL, instead they define some convenient constructs that may be more natural for users.
The While/Then expression is a rewrite for logical implication. In the following example, while a is greater than 100 then b must be less than 75. This is the same as a greater than 100 implies b less than 75.
The After expression is a rewrite for the PLTL once expression. In the following example, after a is less than 100 is the same as the PLTL expression once a is less than 100.
The Before expression is a rewrite for not once expression. In the following example, before a is less than a 100 is the same as not once is less than 100.
The After/Until expression is a rewrite for the triggers expression, with the second expression negated. In the following example, after a is greater than 100 until a is greater than 1000 is identical to a is greater than 100 triggers not a greater than 1000.
Note: This expression is useful for defining an interval between two expressions a and b that define the start and end of the interval respectively.
The Never expression is a rewrite for historically with argument negated. In the following example, never a greater than 100 and b less than 50 is equivalent to historically not a greater than 100 and b less than 50.
SpeAR supports logical expressions of and, or, xor, implies, and not. Logical expressions must be performed over expressions that are boolean typed. The following example shows the syntax for each type of boolean expression.
SpeAR supports addition, subtraction, multiplication, division, and modulus for integer and real typed expressions. The following example demonstrates each one for integer and real typed expressions.
Note: the underlying SMT solvers have incomplete (Z3) or nonexistent (the rest) support for nonlinear arithmetic. If the solver selected doesn't support nonlinear arithmetic, offending expressions will be highlighted. If the underlying solver does support it, it is somewhat likely that results of unknown will be returned by the solver.
SpeAR supports greater than, greater than or equal to, less than, and less than or equal to for integer and real typed expressions. Further, it supports equality and non-equality for any two type-equivalent expressions.
The following example demonstrates each relational operation and how to use it.
SpeAR supports composite data types of record and array. There are specific expressions in the SpeAR language design to support the creation, indexing, and non-destructive updating of composite data types. The following sections cover the different ways this can be accomplished.
Records are (field,expression) pairings. To use a record it is often necessary to create one, access one or more fields of an existing record, or update one or more elements of an existing record. The following sections define how to define record expressions, fieldless record expressions, record field access expressions, and update expressions for the following record type.
Record expressions create new records for an existing record type. A record expression must use the keyword new, followed by the type of record it is instantiating and assignments for every legal field of the record. The following example shows how to use a record expression to create a new record.
Fieldless record expressions create a new records for an existing type without having to explicitly list the fields. This is convenient for a record structure with many field names. The following example shows how to use a fieldless record expression to create a new record.
Record field access expressions are used to obtain the value for a field within a given record. The following examples show how to use field access expressions to get the contents of a record.
Record update expressions allow one to change a single field of a record without having to create an entirely new record. The following example shows how to use it.
Arrays are homogenous lists. To use an array it is often necessary to create one, access one or more elements of an existing array, or update one or more elements of an existing array. The following sections define how to define array expressions, array index expressions, and array update expressions for the following record type.
Array expressions create new arrays for an existing array type. An array expression must use the keyword new, followed by the type of record it is instantiating and assignments for every legal field of the record. The following example shows how to use an array expression to create a new record.
Array index expressions are used to obtain the value for an array element. The following examples show how to use array index expressions to get the contents of an array.
Array update expressions allow one to change a single element of an array without having to create an entirely new array. The following example shows how to use it.
Spear supports reasoning about set membership for finite data types. Set membership reasoning requires the user pair a single element (for example, a single variable of an arbitrary type) and a collection of elements that describe the set. The two elements are combined with the "in" expression which expresses that the element on the left hand side of the "in" expression is a member of the element on the right-hand side.
The following example shows the different types of set membership operations supported by Spear.
Each type of set membership operator is discussed further in the following subsections.
In expressions are the combining element for set expressions. In expressions match an element of an arbitrary type on the left-hand side to the set described by the right hand side. In the following example, the macro m0 is assigned using a in expression. The reader should as "Input1 is assigned one of the values in the set {A, C, E}."
The right-hand side of in expressions could be a set expression (explained in the next subsection), an array expression, or an interval expression (for integer and real typed variables).
Set expressions are a convenient way to collect values that a user wants to check membership of. The only restriction on their use is that every element of the set is of the same type.
The previous section's example illustrates the use of a set expression for the enumeration values A, C, and E.
For numeric types (integers and reals) it can be more natural to reason whether or not a value lies within an interval. Interval expressions provide a mechanism for reasoning over intervals. The following example shows the use of interval expressions for integer and real type variables.
Sometimes one might want to use an existing specification to define the behaviors of some elements of a current specification. This can be done by simply equating the outputs of an existing specification to variables within the specification being developed using a specification call. The following example shows how to constrain the value of x according to the constraints in specification called as applied to input a.
Note: the file containing the specification being call must be imported to be referenced in a specification call.
If a pattern is necessary, it can be called in a function-call style, similar to a specification call, but without the spec keyword. The following examples shows how to use a pattern call.
Sometimes one might want to cast a variable of one type to another. Spear natively supports casting from boolean to integer (btoi), real to integer (floor) and integer to real(real). Any other type of casting expression can be accomplished using a user provided pattern.
There are several miscellaneous expressions that have been added to the Spear language for convenience to the specification writer. The following subsections show each.
This expression references the current step the model is during evaluation. This can be useful for conditional requirement specification as shown in the following example.
This expression takes a boolean argument and returns how many times it has been true. This can be useful for tracking failures or count occurrences of interesting events in a specification. The following example shows it being used to count how many times a variable "failure" has been true.
This expression takes a boolean argument and returns how many times it has been consecutively true. This can be useful for tracking failures or count occurrences of interesting events in a specification. The following example shows it being used to count how many times a variable "failure" has been consecutively true.
