Типовые примеры использования языка Atoment


https://doi.org/10.18255/1818-1015-2011-4-7-20

Полный текст:


Аннотация

Язык 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. https://doi.org/10.18255/1818-1015-2011-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.) https://doi.org/10.18255/1818-1015-2011-4-7-20

Просмотров: 2

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)