maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1094Research ArticleОригинальные статьиArticlesТиповые примеры использования языка AtomentTypical Examples of Atoment Language UsingАнуреевИгорь СергеевичAnureevI. S.anureev@iis.nsk.suИнститут систем информатики имени А.П. Ершова СО РАНRussian Federation201120122011184720Copyright © Ануреев И.С., 20112011Ануреев И.С.Anureev I.S.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1094

Язык Atoment - предметно-ориентированный язык выполнимых спецификаций, применяемый для описания методов и техник верификации программ. В этой работе представлена коллекция типовых примеров использования языка Atoment, охватывающая такие темы, как модели программ, операционная, трансформационная и аксиоматическая семантики, формальная спецификация языков программирования.

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.

верификацияспецификацияоперационная семантикааксиоматическая семантикатрансформационная семантикапредметно-ориентированные языкисистемы верификацииverificationspecificationoperational semanticsaxiomatic semanticstransformational semanticsdomain-specific languagesverification systemsReferencesАнуреев И.С. Язык Atoment: синтаксис и семантика. Новосибирск, 2010. 39 с. (Препр./РАН. Сиб. отд-ние. ИСИ; №157).Ануреев И.С. Язык Atoment: синтаксис и семантика. Новосибирск, 2010. 39 с. (Препр./РАН. Сиб. отд-ние. ИСИ; №157).Ануреев И.С. Язык Atoment: стандартная библиотека. Новосибирск, 2010. 32 с. (Препр./РАН. Сиб. отд-ние. ИСИ; №158).Ануреев И.С. Язык Atoment: стандартная библиотека. Новосибирск, 2010. 32 с. (Препр./РАН. Сиб. отд-ние. ИСИ; №158).Standard ECMA-334. C# Language Specification. 4th edition (June 2006). <http://www.ecma-international.org/publications/standards/Ecma-334.htm>.Standard ECMA-334. C# Language Specification. 4th edition (June 2006). <http://www.ecma-international.org/publications/standards/Ecma-334.htm>.Ануреев И.С. Операционно-онтологическая семантика операторов безусловной передачи управления в языке C# // Материалы международной конференции "Космос, астрономия и программирование" (Лавровские чтения) / Санкт- Петербургский государственный университет. СПб., 2008. С. 259-266.Ануреев И.С. Операционно-онтологическая семантика операторов безусловной передачи управления в языке C# // Материалы международной конференции "Космос, астрономия и программирование" (Лавровские чтения) / Санкт- Петербургский государственный университет. СПб., 2008. С. 259-266.Ануреев И.С. Операционно-онтологическая семантика обработки исключений // Материалы международной конференции "Космос, астрономия и программирование" (Лавровские чтения) / Санкт-Петербургский государственный университет. СПб., 2008. С. 15-22.Ануреев И.С. Операционно-онтологическая семантика обработки исключений // Материалы международной конференции "Космос, астрономия и программирование" (Лавровские чтения) / Санкт-Петербургский государственный университет. СПб., 2008. С. 15-22.Ануреев И.С. Операционно-онтологический подход к формальной спецификации языков программирования // Программирование. 2009. №1. С. 1-11.Ануреев И.С. Операционно-онтологический подход к формальной спецификации языков программирования // Программирование. 2009. №1. С. 1-11.Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации C- программ. Язык С-light и его трансформационная семантика // Проблемы программирования. 2006. №2-3. С. 359-368.Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации C- программ. Язык С-light и его трансформационная семантика // Проблемы программирования. 2006. №2-3. С. 359-368.Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Формальные методы и модели информатики: Сборник научных трудов. Серия «Системная информатика». Новосибирск: Издательство СО РАН. 2004. №9. C. 51-134.Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Формальные методы и модели информатики: Сборник научных трудов. Серия «Системная информатика». Новосибирск: Издательство СО РАН. 2004. №9. C. 51-134.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.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.Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика // Программирование. 2002. №6. С. 1-13.Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика // Программирование. 2002. №6. С. 1-13.Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. №6. С. 5-15.Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. №6. С. 5-15.Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. Система анализа и верификации C-программ СПЕКТР-2 // Моделирование и анализ информационных систем. 2010. Том. 17, №4. С. 88-100.Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. Система анализа и верификации C-программ СПЕКТР-2 // Моделирование и анализ информационных систем. 2010. Том. 17, №4. С. 88-100.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).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).Why Home Page. - <http://why3.lri.fr/>.Why Home Page. - <http://why3.lri.fr/>.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.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.

The authors declare that there are no conflicts of interest present.