We define a structural fixpoint algebraic semantics for iterative programs (in the form of an abstract interpreter that can be instantiated to various operational, denotational, or relational semantics). Defining program properties as programs, we design, by calculus, a structural fixpoint calculus of program algebraic execution properties'' transformers (e.g. sets of traces), that is a collecting semantics for classic transformational logics to prove under or over approximating execution properties of programs. We then design, again by calculus, a structural fixpoint calculus of program algebraicsemantic properties'' transformer (e.g. sets of sets of traces). This is the hypercollecting semantics suitable for the calculational design of hyperlogics to prove under or over approximating semantic properties of programs. Over and under approximation proof systems are designed by calculus so are sound and complete by construction.

We show that an abstraction of the algebraic collecting semantics, hypercollecting semantics, or logic is a algebraic collecting semantics, hypercollecting semantics, or logic of the same form, which yields a hierarchy of semantics, property transformers, hyperproperty transformers, and hyperlogics.

However, proving that a program satisfies an abstract semantic property means, in full generality, that the abstract semantics property must contain the abstract program semantics exactly (e.g. the strongest invariants not only an inductive invariant as in classic program logics). This exact characterization of the abstract program semantics necessary for proving general abstract semantic properties is a great difficulty in practice. This yields to consider less general abstract program semantic properties, which are less precise, but otherwise offer adequate representations of semantic properties or allow for much simplified proof rules, closer to the tradition of classic program execution logics, and complete for well identified classes of abstract semantic properties. This leads to sound and complete proof rules for generalized forall-forall, forall-exists, and exists-forall hyperproperties.