Larch Specification of Copying Garbage Collection

摘要

Garbage collection (GC) is an important part of many language implementations.One of the most important garbage collection techniques is copying GC. This paper consists of an informal but abstract description of copying collection, a formal specification of copying collection written in the Larch Shared Language and the Larch/C Interface Language, a simple implementation of a copying collector written in C, an informal proof that the implementation satisfies the specification, and a discussion of how the specification applies to other types of copying GC such as generational copying collectors. Limited familiarity with copying GC or Larch is needed to read the specification....Formal methods, Formal specification, Garbage collection, Algebraic specification, Copying garbage collection, Larch specification languages, Larch/C specification language.