Типовые примеры использования языка Atoment
Аннотация
Язык Atoment - предметно-ориентированный язык выполнимых спецификаций, применяемый для описания методов и техник верификации программ. В этой работе представлена коллекция типовых примеров использования языка Atoment, охватывающая такие темы, как модели программ, операционная, трансформационная и аксиоматическая семантики, формальная спецификация языков программирования.
Список литературы
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.
Рецензия
Для цитирования:
Ануреев И.С. Типовые примеры использования языка Atoment. Моделирование и анализ информационных систем. 2011;18(4):7-20.
For citation:
Anureev I.S. Typical Examples of Atoment Language Using. Modeling and Analysis of Information Systems. 2011;18(4):7-20. (In Russ.)
Просмотров:
560
Послать статью по эл. почте 