Typical Examples of Atoment Language Using
Abstract
Atoment is a domain-specific language of executable specifications, used to describe methods and techniques of program verification. In this paper a collection of typical examples of the use of the Atoment language, covering topics such as program models, operational, transformational and axiomatic semantics, formal specification of programming languages is presented.
About the Author
I. S. Anureev
Институт систем информатики имени А.П. Ершова СО РАН
Russian Federation
Russian Federation
References
1. Ануреев И.С. Язык Atoment: синтаксис и семантика. Новосибирск, 2010. 39 с. (Препр./РАН. Сиб. отд-ние. ИСИ; №157).
2. Ануреев И.С. Язык Atoment: стандартная библиотека. Новосибирск, 2010. 32 с. (Препр./РАН. Сиб. отд-ние. ИСИ; №158).
3. Standard ECMA-334. C# Language Specification. 4th edition (June 2006). <http://www.ecma-international.org/publications/standards/Ecma-334.htm>.
4. Ануреев И.С. Операционно-онтологическая семантика операторов безусловной передачи управления в языке C# // Материалы международной конференции "Космос, астрономия и программирование" (Лавровские чтения) / Санкт- Петербургский государственный университет. СПб., 2008. С. 259-266.
5. Ануреев И.С. Операционно-онтологическая семантика обработки исключений // Материалы международной конференции "Космос, астрономия и программирование" (Лавровские чтения) / Санкт-Петербургский государственный университет. СПб., 2008. С. 15-22.
6. Ануреев И.С. Операционно-онтологический подход к формальной спецификации языков программирования // Программирование. 2009. №1. С. 1-11.
7. Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации C- программ. Язык С-light и его трансформационная семантика // Проблемы программирования. 2006. №2-3. С. 359-368.
8. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Формальные методы и модели информатики: Сборник научных трудов. Серия «Системная информатика». Новосибирск: Издательство СО РАН. 2004. №9. C. 51-134.
9. Nepomniaschy, V. A., Anureev, I. S., Promsky, A. V. Verification-oriented language C-light and its structural operational semantics // Proc. of Conf. 2003. PSI-2003, LNCS 2890. P. 1-5.
10. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика // Программирование. 2002. №6. С. 1-13.
11. Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. №6. С. 5-15.
12. Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. Система анализа и верификации C-программ СПЕКТР-2 // Моделирование и анализ информационных систем. 2010. Том. 17, №4. С. 88-100.
13. Anureev I.S. Integrated approach to analysis and verification of imperative programs // Joint NCC&IIS Bulletin, Series Computer Science. 2011. Vol. 32. 18 p. (To appear).
14. Why Home Page. - <http://why3.lri.fr/>.
15. Boogie: A Modular Reusable Verifier for Object-Oriented Programs / Barnett M., Chang B., DeLine R., Jacobs B. and Leino R. // FMCO 2005. 2006. LNCS 4111. P. 364-387.
Review
For citations:
Anureev I.S. Typical Examples of Atoment Language Using. Modeling and Analysis of Information Systems. 2011;18(4):7-20. (In Russ.)
Views:
573
Email this article 