The author redefines attribute grammars in an algebraic setting. In the new setting, the author shows (1) the correspondence of testing whether an attribute grammar is noncircular to syntactical correctness, and (2) the correspondence of establishing that an attribute grammar defines the right mapping to semantical correctness. Courcelle generalizes methods for proving the correctness of programs to proving the correctness of attribute systems and establishes the completeness of the system.