The specification of properties that are preserved during the execution of a procedure, is an instance of the well-known frame problem.  The frame problem has proved to be one of the thorniest obstacles in the field of Specification and Verification of programs with rich heap structures and encapsulation.

Dynamic Frames is a formalism that was developed to deal with this problem.  Its emphasis is on preserving the modularity of the specification methodology, i.e., the ability to handle small parts of a larger program independently of each other, without compromising its expressiveness, i.e., without imposing a strict methodology that would exclude useful programs.  Further developments focused on automating the verification of programs written in the Dynamic Frames style.  Automation poses extra challenges, and calls for variations of the original formalism.

The original formalism as well as two such variations are discussed in this tutorial.  During the discussion, we compare the strengths and weaknesses of each approach, and we mention several important design goals and trade-offs, in the hope of providing a good starting point for people who are interested in conducting research in the area.