Language Description - lgwagner/SpeAR GitHub Wiki

The SpeAR specification language allows users to write files of type different types: Specification files and Definitions files. SpeAR is designed to be a constraint-based specification language backed by the formal semantics of the Lustre synchronous dataflow programming language. It allows users to describe interface of the element being specified, and explicit sections describe how the elements inputs and outputs relate to each other. Finally, it allows for several different types of analyses that can be used to ensure that the element is correct, consistent, and realizable.

The SpeAR language is designed to allow users to capture complex temporal relationships using a somewhat sophisticated expression language based on Lustre and Past-Time only Linear Temporal Logic, which is often referred to as PLTL. PLTL allows one to describe a predicate that should hold from the beginning of a program's execution to the program's current state of execution. It is backward looking, hence Past-Time.

The SpeAR language can capture many different types of temporal relationship, but there are things that are expressible in Lustre that cannot be represented in SpeAR. For those situations, users are encouraged to investigate the use of Patterns which are able to harness the full expressive capability of the Lustre language. Patterns can be called similarly to functions. This allows them to be easily used within specifications when appropriate.