Analyses - lgwagner/SpeAR GitHub Wiki

SpeAR features several types of analyses to ensure that the specification is well-formed and functionally correct. Some analysis, like type-checking, are performed in real-time as the user writes a specification. These types of analyses are provided to give users instant feedback so they can identify and correct errors as they arise.

Real-time analyses that are performed as the user writes the specification are:

• type checking
• unit checking
• well formedness checking
  • all specification output variables are assigned
  • all specification input variables are read
  • types, constants, patterns, and specifications are acyclic
  • pattern variables are assigned once and only once

Analyses that can be performed after a specification is completed are based on model-checking. These analyses perform a rigorous evaluation of the model. These analyses are:

• Logical Entailment
• Logical Consistency
• Realizability
• Unique First Cause Test Generation
• Pattern Validation
• Type Vacuity Checking