Types - lgwagner/SpeAR GitHub Wiki
Typing information in a requirements specification is somewhat counter-intuitive. However, an important part of defining the correct behaviors of a new system is precisely identifying what data it will accept from the environment as inputs and what data it will provide back to the environment as outputs. As a result, SpeAR requires users to explicitly define the data being used and produced by an element. It also provides an abstract datatype that allows users to defer defining a datatype to allow them to continue developing a specification with incomplete information.
With the exception of abstract types, type-checking in SpeAR is structural. That is, two types are equivalent if they have the same underlying structure. If different units are provided for structurally equivalent types, unit dimensional analysis identifies those errors.
The following sections describe and define the types supported by SpeAR.
SpeAR supports the primitive datatypes of boolean, integer, and reals. Integers and reals in SpeAR are modeled with infinite precision; integers are from negative infinity to positive infinity and reals are modeled as infinite precision rationals. Primitive types are the only SpeAR types that do not have to be defined in the Types section of a Specification or Definitions file. Instead, when declaring an input, output, or local variable the user can identify the type of that variable as a primitive type directly in the declaration.
Named types can be used to alias existing types. As discussed in the Units section, this is generally useful in SpeAR for attaching units to existing types. For example, one might want to use reals to represent distance, time, and velocity. Named types will allow users to define each as a real while attaching units of meters, seconds, and meters per second, respectively.
Enumerations are useful for representing a unique members of a set of similar objects, such as colors, days of the week, or months of the year. The use of these enumerations in SpeAR is demonstrated in the following example.
Predicate subtypes are refinements of existing types. Refinements are made by providing a predicate expression that describes legal values for the type. For example, one natural predicate subtype to use is an integer where all acceptable values are nonnegative. Another is an integer where all values are positive reals. Yet another is a boolean whose value is alternating. Each of these types can be accomplished in SpeAR using predicate subtyping and are shown in the following example.
When defining a predicate subtype, one must be careful not to create a type that is vacuous. A vacuous type will have no satisfying values and thus, when used, will create a specification with no satisfying values. This is covered more in-depth in Type Vacuity Checking.
Record types are composite datatypes that have name-type pairings. For example, a two-dimensional coordinate could be captured using a record with fields x (for the x-axis value) and y (for the y-axis value). Building on that example, one could define a circle with field center defined by a two-dimensional coordinate, and radius defined by a positive real number. The following example shows how this can be defined in SpeAR using record types.
Note: this example uses a predicate subtype for the radius, since a radius with a negative, or zero, value is meaningless.
Arrays are a collection of homogenous elements. An array can be useful for capturing lists of objects, or N-dimensional objects. An example of how to declare array types is shown in the following example.
Note: This example uses the two dimensional coordinate as the base type for the array to show a possible path of an object in a 2-D space.
Abstract types are useful for identifying some data that the user knows will be useful in the specification, but does not yet know the structure of. The following example shows three abstract types that represent three unique datatypes whose structure is unknown.
Note: Type-checking of abstract types is nominal in SpeAR. That is, if two abstract types are equated then the tool will provide a type error if the abstract type names aren't the same.
