Observation Predicates in Flow Logic

Motivated by the connection between strong and soft type systems we explore flow analyses with hard constraints on the admissible solutions. We show how to use observation predicates and formula rearrangements to map flow analyses with hard constraints into more traditional flow analyses in such a way that the hard constraints are satisfi ed exactly when the observation predicates report no violations. The development is carried out in a large fragment of a first order logic with negation and also takes care of the transformations necessary in order to adhere to the stratification restrictions inherent in Alternation-free Least Fixed Point Logic and similar formalisms such as Datalog.