Constraint - lgwagner/SpeAR GitHub Wiki

SpeAR specifications are a collection of constraints that relate how the system relates to the environment it is operating within. Assumptions describe constraints that the system expects the environment to honor. Requirements describe constraints that the system will honor. Finally, Properties describe contraints that the Assumptions and Requirements will honor together. Properties are a way of validating that the system is described correctly.

Constraints are defined by an identifier (a unique name for the constraint) and an expression that evaluates to true or false (also known as an predicate).

The following example shows a simple specification that takes two inputs a and b and returns two outputs x and y. First, the specification makes assumptions a0 and a1 that a and b will both be greater than or equal to zero. The requirement r0 establishes a constraint that the output x is equal to the difference of a and b. Similarly r1 establishes a constraint that the output y is the sum of a and b. Finally, we have a property p0 that states that output y will always be greater than or equal to output x.