Атрибутные аннотации и их применение в дедуктивной верификации C-программ

Предложен новый вид аннотаций, называемых атрибутными аннотациями, и методология их применения в дедуктивной верификации программ. Описана коллекция аннотирующих атрибутов для подмножества C-kernel языка C и на их основе представлены два варианта аксиоматической семантики языка C-kernel – семантика прямого прослеживания и смешанная семантика прямого прослеживания.