Constants - lgwagner/SpeAR GitHub Wiki

The Constants section is useful for defining constant values that may be useful for the specification under development. The notion of constants is rather flexible in SpeAR. The simplest way to define a constant is to assign its value to a literal. However, a legal constant can also be constructed by performing arithmetic operations on existing constants. SpeAR performs static analysis on constants as the user writes them and will identify illegal constants as errors to the user.

Constants require the user to define a unique name for the constant, the type, and the expression defining the constant.

In this example we define constants for each primitive real (pi), int (MAX_ALTITUDE), and bool (not_useful). These constants are used to define constants for the composite types int_array and record_type.