  We present Behavioral Program Logic (BPL), a dynamic logic for trace
properties that incorporates concepts from behavioral types and allows
reasoning about non-functional properties within a sequent calculus. BPL uses
behavioral modalities [s |- {\tau} ], to verify statements s against behavioral
specifications {\tau}. Behavioral specifications generalize postconditions and
behavioral types. They can be used to specify other static analyses, e.g., data
flow analyses. This enables deductive reasoning about the results of multiple
analyses on the same program, potentially implemented in different formalisms.
Our calculus for BPL verifies the behavioral specification gradually, as common
for behavioral types. This vastly simplifies specification, calculus and
composition of local results. We present a sequent calculus for object-oriented
actors with futures that integrates a pointer analysis and bridges the gap
between behavioral types and deductive verification. This technical report
introduces (1) complete LAGC semantics of a Core Active Object language (CAO)
without continuations (2) Behavioral Program Logic and (3) gives an example for
a behavioral type expressed in Behavioral Program Logic, method types. This
report contains the soundness proofs for method types. While the semantics
cover CAO with suspension, the method types do not, to simplify the
presentation.
