Unity properties and sequences of states, some observations (Q688444)

We examine the expressive power of Unity properties in relation to execution sequences of Unity programs. One might expect that if two programs have the same unless and leadsto properties, then they have the same execution sequences. We show that this is not true. We examine whether this difference vanishes if we adopt a stronger notion of fairness, or use ensures properties instead of leadsto properties (possibly adopting a stronger fairness notion also). We show by a simple example that both approaches are not successful. Hence, properties are not expressive enough to characterize execution sequences, and it is not clear what execution model corresponds to Unity properties. As a consequence, the notion of property preserving program refinement differs from the notion of decreasing nondeterminism.