На пути к технологии разработки операционной семантики компьютерных языков: унифицированный формат помеченных систем переходов
Ключевые слова:
операционная семантика, помеченные системы переходовАннотация
Предлагается формализм для описания помеченных систем переходов, который унифицируют формат состояний системы переходов, формат инструкций компьютерных языков, представляемых метками системы переходов, и формат и семантику правил перехода и, тем самым, делает процесс разработки операционной семантики компьютерных языков более технологичным.Литература
Ануреев И.С. Операционно-онтологический подход к формальной спецификации языков программирования // Программирование. 2009. № 1. С. 50-60
Ануреев И.С. Типовые примеры использования языка Atoment // Моделирование и анализ информационных систем. 2011. Том 18, № 4. – С. 7-20
Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Том 17, № 3. С. 5-28
Атучин М.М., Ануреев И.С. Атрибутные аннотации и их применение в дедуктивной верификации C-программ // Моделирование и анализ информационных систем. 2011. Том 18, № 4. С. 21-33
Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. Верификация C-программ в мультиязыковой системе СПЕКТР // Моделирование и анализ информационных систем. 2010. Том 17, № 4. С. 88-100
Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика // Программирование. 2002. № 6. С. 1-13
Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. № 6. С. 65-80
Непомнящий~В.А., Ануреев И.С., Промский А.В., Дубрановский И.В. На пути к верификации C# программ: трехуровневый подход // Программирование. 2006. № 4. С. 4-20
Шилов Н.В., Ануреев И.С., Бодин Е.В. О генерации условий корректности для императивных программ // Программирование. 2008. № 6. С. 5-23
Anureev I.S. A three-stage method of C program verification // Joint NCC&IIS Bulletin, Series Computer Science. 2008. Vol. 28. P. 1-29
Anureev I.S. Integrated approach to analysis and verification of imperative programs // Joint NCC&IIS Bulletin, Series Computer Science. 2011. Vol. 32. P. 1-18
AsmL: The Abstract State Machine Language. URL: http://research.microsoft.com/en-us/projects/asml/ (дата обращения: 16.10.2012)
Gurevich Y. Abstract State Machines: An Overview of the Project // Foundations of Information and Knowledge Systems (FoIKS): Proc. Third Internat. Symp. Lect. Notes Comput. Sci. 2004. Vol. 2942. P. 6-13
Gurevich Y. Lipari Guide // Specification and Validation Methods. ed. E.Borger. Oxford University Press, Inc. New York, NY, USA, 1995. P. 9-36
Honsell F., Pravato A., Ronchi della Rocca S. Structured Operational Semantics of the Language Scheme. Tech. Rep., University of Torino, Department of Informatics, 1995
Huggins J. Abstract State Machines Web Page. URL: http://www.eecs.umich.edu/gasm (дата обращения: 16.10.2012)
Lucas P., Walk K. On the Formal Description of PL/1 // Annual Review in Automatic Programming. 1969. Vol. 6(3). P. 105-182
Morris J. Algebraic Operational Semantics for Modula-2. PhD Thes. University of Michigan, Ann Arbor, MI, 1988
Morris J., Pottinger G. Ada-Ariel Semantics. Tech. Rep. Odyssey Research Associates, 1990
Norrish M. C Formalized in HOL. PhD Thes. University of Cambridge, Computer Laboratory, 1998
Plotkin G.D. A Structural Approach to Operational Semantics. Tech. Rep. DAIMI FN-19. Computer Science Department, Aarhus University. Aarhus, Denmark, 1981
XasM: An Extensible, Component-Based Abstract State Macnines Language. URL: http://www.xasm.org/ (дата обращения: 16.10.2012)
Wolczko M. Semantics of Smalltalk-80 // Object-Oriented Programming (ECOOP’87): European Conf. Lect. Notes Comput. Sci. 1987. Vol. 276. P. 108-120
Ануреев И.С. Типовые примеры использования языка Atoment // Моделирование и анализ информационных систем. 2011. Том 18, № 4. – С. 7-20
Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Том 17, № 3. С. 5-28
Атучин М.М., Ануреев И.С. Атрибутные аннотации и их применение в дедуктивной верификации C-программ // Моделирование и анализ информационных систем. 2011. Том 18, № 4. С. 21-33
Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. Верификация C-программ в мультиязыковой системе СПЕКТР // Моделирование и анализ информационных систем. 2010. Том 17, № 4. С. 88-100
Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика // Программирование. 2002. № 6. С. 1-13
Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. № 6. С. 65-80
Непомнящий~В.А., Ануреев И.С., Промский А.В., Дубрановский И.В. На пути к верификации C# программ: трехуровневый подход // Программирование. 2006. № 4. С. 4-20
Шилов Н.В., Ануреев И.С., Бодин Е.В. О генерации условий корректности для императивных программ // Программирование. 2008. № 6. С. 5-23
Anureev I.S. A three-stage method of C program verification // Joint NCC&IIS Bulletin, Series Computer Science. 2008. Vol. 28. P. 1-29
Anureev I.S. Integrated approach to analysis and verification of imperative programs // Joint NCC&IIS Bulletin, Series Computer Science. 2011. Vol. 32. P. 1-18
AsmL: The Abstract State Machine Language. URL: http://research.microsoft.com/en-us/projects/asml/ (дата обращения: 16.10.2012)
Gurevich Y. Abstract State Machines: An Overview of the Project // Foundations of Information and Knowledge Systems (FoIKS): Proc. Third Internat. Symp. Lect. Notes Comput. Sci. 2004. Vol. 2942. P. 6-13
Gurevich Y. Lipari Guide // Specification and Validation Methods. ed. E.Borger. Oxford University Press, Inc. New York, NY, USA, 1995. P. 9-36
Honsell F., Pravato A., Ronchi della Rocca S. Structured Operational Semantics of the Language Scheme. Tech. Rep., University of Torino, Department of Informatics, 1995
Huggins J. Abstract State Machines Web Page. URL: http://www.eecs.umich.edu/gasm (дата обращения: 16.10.2012)
Lucas P., Walk K. On the Formal Description of PL/1 // Annual Review in Automatic Programming. 1969. Vol. 6(3). P. 105-182
Morris J. Algebraic Operational Semantics for Modula-2. PhD Thes. University of Michigan, Ann Arbor, MI, 1988
Morris J., Pottinger G. Ada-Ariel Semantics. Tech. Rep. Odyssey Research Associates, 1990
Norrish M. C Formalized in HOL. PhD Thes. University of Cambridge, Computer Laboratory, 1998
Plotkin G.D. A Structural Approach to Operational Semantics. Tech. Rep. DAIMI FN-19. Computer Science Department, Aarhus University. Aarhus, Denmark, 1981
XasM: An Extensible, Component-Based Abstract State Macnines Language. URL: http://www.xasm.org/ (дата обращения: 16.10.2012)
Wolczko M. Semantics of Smalltalk-80 // Object-Oriented Programming (ECOOP’87): European Conf. Lect. Notes Comput. Sci. 1987. Vol. 276. P. 108-120
Опубликован
2013-04-01
Как цитировать
Ануреев, И. С. (2013). На пути к технологии разработки операционной семантики компьютерных языков: унифицированный формат помеченных систем переходов. Труды СПИИРАН, 2(25), 255-276. https://doi.org/10.15622/sp.25.13
Раздел
Статьи
Авторы, которые публикуются в данном журнале, соглашаются со следующими условиями:
Авторы сохраняют за собой авторские права на работу и передают журналу право первой публикации вместе с работой, одновременно лицензируя ее на условиях Creative Commons Attribution License, которая позволяет другим распространять данную работу с обязательным указанием авторства данной работы и ссылкой на оригинальную публикацию в этом журнале.
Авторы сохраняют право заключать отдельные, дополнительные контрактные соглашения на неэксклюзивное распространение версии работы, опубликованной этим журналом (например, разместить ее в университетском хранилище или опубликовать ее в книге), со ссылкой на оригинальную публикацию в этом журнале.
Авторам разрешается размещать их работу в сети Интернет (например, в университетском хранилище или на их персональном веб-сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению, а также к большему количеству ссылок на данную опубликованную работу (Смотри The Effect of Open Access).
