Attribute Annotations and Their Use in C Program Deductive Verification
Autor: | M. M. Atuchin, I. S. Anureev |
---|---|
Jazyk: | English<br />Russian |
Rok vydání: | 2011 |
Předmět: | |
Zdroj: | Моделирование и анализ информационных систем, Vol 18, Iss 4, Pp 21-33 (2011) |
Druh dokumentu: | article |
ISSN: | 1818-1015 2313-5417 |
Popis: | In this paper a new kind of annotations, called attribute annotations, and the methodology for their application in a deductive program verification are proposed. A collection of annotating attributes for the subset C-kernel of the C language is described, and on their base two versions of axiomatic semantics of C-kernel - forward semantics and mixed forward semantics - are presented. |
Databáze: | Directory of Open Access Journals |
Externí odkaz: |