Formal models, validation, and documentation for metainfo annotations