FMSE
Formal
Methods in
Software Engineering
Publications From Small-step Semantics to Big-st ... Anonymous  Login
From Small-step Semantics to Big-step Semantics, Automatically
Stefan Ciobaca  
iFM 2013,   2013  
Abstract:

Small-step semantics and big-step semantics are two styles for
operationally de ning the meaning of programming languages. Small-step
semantics are given as a relation between program con gurations that
denotes one computational step; big-step semantics are given as a relation
directly associating to each program con guration the corresponding
nal con guration. Small-step semantics are useful for making precise
reasonings about programs, but reasoning in big-step semantics is easier
and more intuitive. When both small-step and big-step semantics are
needed for the same language, a proof of the fact that the two semantics
are equivalent should also be provided in order to trust that they both
de ne the same language. We show that the big-step semantics can be
automatically obtained from the small-step semantics when the small-
step semantics are given by inference rules satisfying certain assumptions
that we identify. The transformation that we propose is very simple
and we show that when the identi ed assumptions are met, it is sound
and complete in the sense that the two semantics are equivalent. For a
strict subset of the identi ed assumptions, we show that the resulting
big-step semantics is sound but not necessarily complete. We discuss our
transformation on a number of examples.

Project(s):    K
Grant(s):    DAK
NEWS
New publication : Model checking recursive programs interacting via ... - 01 feb 2015

Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating reference fields. In the presence of recursive ... (more)


New publication : K-Java: A Complete Semantics of Java - 10 sep 2014

This paper presents K-Java, a complete executable formal semantics of Java 1.4.
K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology.
more)


New publication : K-Java: A Complete Semantics of Java - 09 jul 2014

This paper presents K-Java, a complete executable formal semantics of Java 1.4.
K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology.
more)


New publication : Engineering Hoare Logic-based Program Verification in ... - 30 oct 2013

We propose a language-independent symbolic execution framework for languages endowed with a formal operational semantics based on term rewriting. Starting from a given definition of a language, a new language ... (more)


New talk: PAS 2013 - 20 oct 2013

Dorel lucanu will give a talk at PAS 2013.

(more)

     Archive

@FMSE 2010-2011