Specifying typestate properties
In Clara, users (or researchers) specify typestate properties as annotations to a monitoring aspect, written in AspectJ. It is also possible to perform static typestate analysis only, without any runtime monitor. In this case, the user just provides an annotated AspectJ aspect that has empty advice bodies.
Clara supports two different annotation languages:
Dependency State Machines subsume Dependent Advice, i.e. they carry strictly more information. Dependent Advice are a flow-insensitive representation that is rather useful as an internal representation for the two flow-insensitive typestate analyses that Clara offers. In most cases, users will want to use Dependency State Machines because they offer a syntax and semantics that is easier to understand and because they convey more information: they are a flow-sensitive representation of the typestate property. Internally, when given a Dependency State Machine, then Clara generates Dependent Advice from this Dependency State Machine anyway. Hence, with a Dependency State Machine, users can use both flow-insensitive and flow-sensitive analyses; with Dependent Advice, they can only use flow-insensitive analyses. So in a nutshell:
- Usually may want to use Dependency State Machines:
- support flow-sensitive and flow-insensitive optimizations
- subsume Dependent Advice
- Dependent Advice exist mostly for legacy reasons:
- support only flow-insensitive analyses
- are more complicated to understand than Dependency State Machines
