There is an apparent similarity between the descriptions of small-step operational semantics of imperative programs and the semantics of nite automata, so de ning an abstraction mapping from semantics to automata and proving a simulation property seems to be easy. This paper aims at identifying the reasons why simple proofs break, among them artifacts in the semantics that lead to stuttering steps in the simulation. We then present a semantics based on the zipper data structure, with a direct interpretation of evaluation as navigation in the syntax tree. The abstraction function is then de ned by equivalence class construction.
Among the formalisms employed to describe the semantics of transition systems,
two particularly popular choices are abstract machines and structural
operational semantics (SOS). Abstract machines are widely used for modeling and
verifying dynamic systems, e.g. nite automata, Buchi automata or timed
automata [
This kind of semantics is often extended by adding a background state
composed of a set of variables with their values: this is the case of timed automata,
which use background clock variables [
Another formalism for modeling transition systems is structural semantics
(\small-step", contrary to \big-step" semantics which is much easier to handle
but which is inappropriate for a concurrent setting), which uses a set of reduction
rules for simplifying a program expression. It has been described in detail in [
This kind of rules is intuitive; however, the proofs involving them require
induction over the expression structure. A di erent approach to writing a
structural semantics was described in [
(Seq e1 e2 ; s) ! (e1 e2 ; s) (Empty ; s) ! ( ; s)
Here the \ " operator designates concatenation of control stacks. The semantics of continuations does not need induction over the expression, something which makes proof easier; however it requires more auxiliary steps for maintaining the control stack which do not have direct correspondance in the modeled language.
For modeling non-local transfer of control, Krebbers and Wiedijk [
The present paper describes an approach to translation from structural
operational semantics to nite automata extended with background state. All the
considered automata are an extension of Buchi automata with background state,
i.e. they have a nite number of nodes and edges but can produce an in nite
trace. The reason of our interest in abstracting from structural semantics to
Buchi automata is our work in progress [
The contents of the paper has been entirely formalized in the Isabelle proof
assistant [
We have identi ed the following as the main problems when trying to prove the correctness of the translation between a programming language semantics and its abstraction to automata: 1. Preservation of execution context: an abstract machine always sees all the available nodes while a reduced expression loses the information about previous reductions. 2. Semantic artifacts: some reduction rules are necessary for the functionality of the semantics, but may be missing in the modeled language. Additionally, the rules can produce expressions which do not occur in the original language.
These problems occur independently of variations in the presentation of
semantic rules [
We will describe these two problems in detail, and later our approach to their solution, in the context of a minimalistic programming language which only manipulates Boolean values (a Null value is also added to account for errors): datatype val = Bool bool j Null
The language can be extended in a rather straightforward way to more complex expressions. In this language, expressions are either values or variables: datatype expr = Val val j Var vname
The statements are those of a small imperative language: datatype stmt =
Empty j Assign vname val j Seq stmt stmt j Cond expr stmt stmt j While expr stmt | no-op | assignment: var := val | sequence: c1; c2 | conditional: if e then c1 else c2 | loop: while e do c 2.1
Preservation of execution context Problem 1 concerns the loss of an execution context through expression reductions which is a design feature of structural semantics. Let us consider a simple example.
Assume we have a structural semantics for our minimal imperative language (some rules of a traditional presentation are shown in Figure 1): we want to translate a program written in this language into an abstract machine. Assume that the states of variable values have the same representation in the two systems: this means we only need to translate the program expression into a directed graph with di erent nodes corresponding to di erent expressions obtained by reductions of the initial program expression.
On the abstract machine level the Assign statements would be represented as two-state automata, and the Cond as a node with two outgoing edges directed to the automata for the bodies of its branches.
Consider a small program in this language Cond bexp (Assign a 5) Empty and its execution ow.
Cond bexp (Assign a 5) Empty (Assign a 5) a:=5 Empty
Empty
The execution can select any of the two branches depending on the bexp value. There are two di erent Empty expressions appearing as results of two di erent reductions. The corresponding abstract machine would be a natural graph representation for a condition statement with two branches (Figure 2).
Cond bexp (Assign a 5) Empty
Assign a 5 a:=5 Empty Cond bexp (Assign a 5) Empty :::
During the simple generation of an abstract machine from a program expression the two Empty statements cannot be distinguished although they should be mapped into two di erent nodes in the graph. We need to add more information about the context into the translation, and it can be done by di erent ways.
A straightforward solution would be to add some information in order to distinguish between the two Empty expressions. If we add unique identi ers to each subexpression of the program, they will allow to know exactly which subexpression we are translating (Figure 3). The advantage of this approach is its simplicity, however, it requires additional functions and proofs for identi er management.
Cond n1 bexp (Assign n2 a 5) (Empty n3) Assign n2 a 5 a:=5 Empty n2 Cond n1 bexp (Assign n2 a 5) Empty n3 n2 n3 ::: :::
Another solution for the problem proposed in this paper involves usage of a
special data structure to keep the context of the translation. There are known
examples of translations from subexpression-based semantics [
(e1; s) ! (e10; s0) (Seq e1 e2; s) ! (Seq e10 e2; s0) [Seq1] (Seq Empty e2; s) ! (e2; s) [Seq2]
Here the Empty expression means that the rst expression in the sequence has been reduced up to the end, and we can start reducing the second expression. However, any imperative language translated to an assembly language would not have an additional operator between the two pieces of code corresponding to the rst and the second expressions. The rule Seq2 must be marked as a silent transition when translated to an automaton, or the semantic rules have to be changed.
Our plan is to propose an alternative technique to formalize operational
semantics that will make it easier to preserve the execution context during the
translation to an automata-based formalism. Our technique is built around a
zipper data structure, whose purpose is to identify a location in a tree (in our
case: a stmt ) by the subtree below the location and the rest of the tree (in our
case: of type stmt-path). In order to allow for an easy navigation, the rest of the
tree is turned inside-out so that it is possible to reach the root of the tree by
following the backwards pointers. The following de nition is a straightforward
adaptation of the zipper for binary trees discussed in [
PTop j PSeqLeft stmt-path stmt j PSeqRight stmt stmt-path j PCondLeft expr stmt-path stmt j PCondRight expr stmt stmt-path j PWhile expr stmt-path
Here, PTop represents the root of the original tree, and for each constructor of stmt and each of its sub-stmt s, there is a \hole" of type stmt-path where a subtree can be tted in. A location in a tree is then a combination of a stmt and a stmt-path: datatype stmt-location = Loc stmt stmt-path
Given a location in a tree, the function reconstruct reconstructs the original tree reconstruct :: stmt ) stmt-path ) stmt, and reconstruct-loc (Loc c sp) = reconstruct c sp does the same for a location. fun reconstruct :: stmt ) stmt-path ) stmt where
reconstruct c PTop = c j reconstruct c (PSeqLeft sp c2 ) = reconstruct (Seq c c2 ) sp j reconstruct c (PSeqRight c1 sp) = reconstruct (Seq c1 c) sp j reconstruct c (PCondLeft e sp c2 ) = reconstruct (Cond e c c2 ) sp j reconstruct c (PCondRight e c1 sp) = reconstruct (Cond e c1 c) sp j reconstruct c (PWhile e sp) = reconstruct (While e c) sp fun reconstruct-loc :: stmt-location ) stmt where
reconstruct-loc (Loc c sp) = reconstruct c sp Our semantics is a small-step operational semantics describing the e ect of the execution a program on a certain program state. For each variable, the state yields Some value associated with the variable, or None if the variable is unassigned. More formally, the state is a mapping vname ) val option. De ning the evaluation of an expression in a state is then standard.
Before commenting the rules of our semantics, let us discuss which kind of structure we are manipulating. The semantics essentially consists in moving around a pointer within the syntax tree. As explained in Section 3.1, a position in the syntax tree is given by a stmt-location. However, during the traversal of the syntax tree, we visit each position at least twice (and possibly several times, for example in a loop): before executing the corresponding statement, and after nishing the execution. We therefore add a Boolean ag, where True is a marker for \before" and False for \after" execution. #W hile
Seq =)
W hile #Seq
W hile
Seq =) =)
W hile
Seq =)
W hile
Seq x := T y := F x := T y := F #x := T y := F x := T" y := F x := T #y := F
As an example, consider the execution sequence depicted in Figure 5 (with assignments written in a more readable concrete syntax), consisting of the initial steps of the execution of the program While (e; Seq (x := T ; y := F )). The before (resp. after) marker is indicated by a downward arrow before (resp. an upward arrow behind) the current statement. The condition of the loop is omitted because it is irrelevant here. The middle con guration would be coded as ((Loc (x := T ) (PSeqLeft (PWhile e PTop) (y := F ))); True).
Altogether, we obtain a syntactic con guration (synt-con g ) which combines the location and the Boolean ag. The semantic con guration (sem-con g ) manipulated by the semantics adjoins the state, as de ned previously. type-synonym synt-con g = stmt-location type-synonym sem-con g = synt-con g bool state
The rules of the small-step semantics of Figure 7 fall into two categories: before execution of a statement s (of the form ((l ; True); s)) and after execution (of the form ((l ; False); s)); there is only one rule of this latter kind: SFalse.
Let us comment on the rules in detail: { SEmpty executes the Empty statement just by swapping the Boolean ag. { SAssign is similar, but it also updates the state for the assigned variable. fun next-loc :: stmt ) stmt-path ) (stmt-location bool ) where
next-loc c PTop = (Loc c PTop; False) j next-loc c (PSeqLeft sp c2) = (Loc c2 (PSeqRight c sp); True) j next-loc c (PSeqRight c1 sp) = (Loc (Seq c1 c) sp; False) j next-loc c (PCondLeft e sp c2) = (Loc (Cond e c c2) sp; False) j next-loc c (PCondRight e c1 sp) = (Loc (Cond e c1 c) sp; False) j next-loc c (PWhile e sp) = (Loc (While e c) sp; True) { SSeq moves the pointer to the substatement c1, pushing the substatement c2 as continuation to the statement path. { SCondT and SCondF move to the then- respectively else- branch of the conditional, depending on the value of the condition. { SWhileT moves to the body of the loop. { SWhileF declares the execution of the loop as terminated, by setting the
Boolean ag to False. { SFalse comes into play when execution of the current statement is nished.
We then move to the next location, provided we have not already reached the root of the syntax tree and the whole program terminates.
The move to the next relevant location is accomplished by function next-loc (Figure 6) which intuitively works as follows: upon conclusion of the rst substatement in a sequence, we move to the second substatement. When nishing the body of a loop, we move back to the beginning of the loop. In all other cases, we move up the syntax tree, waiting for rule SFalse to relaunch the function. 4 4.1
Syntax
As usual, our automata are a collection of nodes and edges, with a distinguished initial state. In this general de nition, we will keep the node type 0n abstract. It will later be instantiated to synt-con g. An edge connects two nodes; moving along an edge may trigger an assignment to a variable (AssAct ), or have no e ect at all (NoAct ).
An automaton 0n ta is a record consisting of a set of nodes, a set of edges and an initial node init-s. An edge has a source node, an action and a destination node dest. Components of a record are written between (j ::: j). 4.2
Semantics An automaton state is a node, together with a state as in Section 3.2. type-synonym 0n ta-state = 0n
state
Executing a step of an automaton in an automaton state (l ; s) consists of selecting an edge starting in node l, moving to the target of the edge and executing its action. Automata are non-deterministic; in this simpli ed model, we have no guards for selecting edges.
l = source e
e 2 set (edges aut ) l 0 = dest e s 0 = action-e ect (action e) s aut ` (l ; s) ! (l 0; s 0) [Action] 5
The principle of abstracting a statement to an automaton is simple; the novelty resides in the way the automaton is generated via the zipper structure: as nodes, we choose the locations of the statements (with their Boolean ags), and as edges all possible transitions of the semantics.
To make this precise, we need some auxiliary functions. We rst de ne a function all-locations of type stmt ) stmt-path ) stmt-location list which gathers all locations in a statement, and a function nodes-of-stmt-locations which adds the Boolean ags.
As for the edges, the function synt-step-image yields all possible successor con gurations for a given syntactic con guration. This is of course an overapproximation of the behavior of the semantics, since some of the source tree locations may be unreachable during execution. fun synt-step-image :: synt-con g ) synt-con g list where
synt-step-image (Loc Empty sp; True) = [(Loc Empty sp; False)] j synt-step-image (Loc (Assign vr vl ) sp; True) = [(Loc (Assign vr vl ) sp; False)] j synt-step-image (Loc (Seq c1 c2 ) sp; True) = [(Loc c1 (PSeqLeft sp c2 ); True)] j synt-step-image (Loc (Cond e c1 c2 ) sp; True) =
[(Loc c1 (PCondLeft e sp c2 ); True); (Loc c2 (PCondRight e c1 sp); True)] j synt-step-image (Loc (While e c) sp; True) =
[(Loc c (PWhile e sp); True); (Loc (While e c) sp; False)] j synt-step-image (Loc c sp; False) = (if sp = PTop then [] else [next-loc c sp])
Together with the following de nitions: fun action-of-synt-con g :: synt-con g ) action where
action-of-synt-con g (Loc (Assign vn vl ) sp; True) = AssAct vn vl j action-of-synt-con g (Loc c sp; b) = NoAct de nition edge-of-synt-con g :: synt-con g ) synt-con g edge list where edge-of-synt-con g s = map( t: (jsource = s; action = action-of-synt-con g s; dest = tj))(synt-step-image s) de nition edges-of-nodes :: synt-con g list ) synt-con g edge list where edges-of-nodes nds = concat (map edge-of-synt-con g nds)
we can de ne the translation function from statements to automata: fun stmt-to-ta :: stmt ) synt-con g ta where stmt-to-ta c = (let nds = nodes-of-stmt-locations (all-locations c PTop) in (j nodes = nds; edges = edges-of-nodes nds; init-s = ((Loc c PTop); True) j)) 6
We recall that the nodes of the automaton generated by stmt-to-ta are labeled by con gurations (location, Boolean ag) of the syntax tree. The simulation lemma (Lemma 1) holds for automata with appropriate closure properties: a successor con guration wrt. a transition of the semantics is also a label of the automaton (nodes-closed ), and analogously for edges (edges-closed ) or both nodes and edges (synt-step-image-closed ).
The simulation statement is a typical commuting-diagram property: a step of the program semantics can be simulated by a step of the automaton semantics, for corresponding program and automata states. For this correspondence, we use the notation , even though it is just plain syntactic equality in our case.
Assume that synt-step-image-closed aut and (((lc; b); s) ((lca; ba); sa)). If ((lc; b); s) ! ((lc 0; b 0); s 0), then there exist lca 0; ba 0; sa 0 such that (lca 0; ba 0) 2 set (nodes aut ) and the automaton performs the same transition: aut ` ((lca; ba); sa) ! ((lca 0; ba 0); sa 0) and ((lc 0; b 0); s 0) ((lca 0; ba 0); sa 0). The proof is a simple induction over the transition relation of the program semantics and is almost fully automatic in the Isabelle proof assistant.
We now want to get rid of the precondition synt-step-image-closed aut in Lemma 1. The rst subcase (edge closure), is easy to prove. Node closure is more di cult and requires the following key lemma:
If lc 2 set (all-locations c PTop) then set (map fst (synt-step-image (lc; b))) set (all-locations c PTop):
Lemma 3 (Closure of automaton). synt-step-image-closed (stmt-to-ta c)
Let us combine the previous results and write them more succinctly, by using the notation ! for the re exive-transitive closure for the transition relations of the small-step semantics and the automaton. Whenever a state is reachable by executing a program c in its initial con guration, then a corresponding ( ) state is reachable by running the automaton generated with function stmt-to-ta:
If ((Loc c PTop; True); s) ! (cf 0; s 0) then 9 cfa 0 sa 0: stmt-to-ta c ` (init-s (stmt-to-ta c); s) ! (cfa 0; sa 0) ^ (cf 0; s 0) (cfa 0; sa 0):
Obviously, the initial con guration of the semantics and the automaton are in the simulation relation , and for the inductive step, we use Lemma 1. 7
This paper has presented a new kind of small-step semantics for imperative programming languages, based on the zipper data structure. Our primary aim is to show that this semantics has decisive advantages for abstracting programming language semantics to automata. Even if the generated automata have a great number of silent transitions, these can be removed.
We are currently in the process of adopting this semantics in a larger
formalization from Java to Timed Automata [
Renaming nodes from source tree locations to numbers is nevertheless easy
to carry out, see the code snippet provided on the web page [