Dynamic Semantics

Here we describe the small-step operational semantics of Olaf.

If you have not seen imperative semantics before, Olaf differs in that we need a heap to store values at addressable locations and we use commands to control evaluation along different branches. Some branches may stop execution but not return a result.

This section details:

what values are;
how we work with heaps and stacks; and
evaluate programs, methods, statements, and expressions.

Values

Values are irreducible terms, which for Olaf are its constants, and heap addresses

v := addr         -- addresses
   | i            -- integers
   | s            -- strings
   | true | false -- booleans
   | unit         -- unit

For method declarations we also need to define a closure, a pair of a function and the global environment at the time of its definition.

c := C m g

Execution Environments

As we have both a stack and a heap we need to keep track of variables/references and their values during execution.

We will use the same definition for both:

env := {} | env, (name, v)

Our environment is either empty, or an existing environment extended with a value associated with a name.

Lookups will be described with the operation:

lookup(name,env)

which will return the value at location pointed to by name in env.

Updating the environment will use the operation:

update(name,new,env)`

which will update the value at location pointed to by name in env with new.

Reduction Form

The form of our dynamic semantics will be:

For expressions:
```
g;l;h |- e ~> v -| h'
```
For statements:
```
g;l;h |- s ~> v -| h'
```
For programs:
```
g |- p ~> v
```

where:

g is the declared methods;
l is the local stack;
h is the old heap;
h' is the new heap;

We use the form |- ... -| to capture changes to the heap arising from evaluating expressions.

Multiple steps are described by ~>*.

We do not include an explicit form for methods as, during a method call, we are reducing the statements within a both by populating the local stack with the evaluated arguments to the method call.

Expressions

Expression are reducible terms that will produce a value. For brevity we will not provide all the reduction rules nor a pure small-step presentation, all rules missing are standard.

Boolean Operations

Evaluating unary operations require we first evaluate the inner expression.

g;l;h |- e ~> e' -| h'

---- [ Unary op Step]

g;l;h |- uop(e) ~> uop(e') -| h'

Binary operations follow, where we evaluate both operands.

g;l;h  |- l ~>* v_{l} -| h'
g;l;h' |- r ~>* v_{r} -| h''

---- [ Binary op Step]

g;l;h |- bop(l,r) ~> bop(v_{l},v_{r}) -| h''

For all operations, once we get to values, we can then call out to existing libraries or features in our host language to evaluate the values.

For example with not:

---- [ Not Reduce ]

g;l;h |- not(b) ~> !b -| h

and for add:

---- [ Add Reduce ]

g;l;h |- add(i_{l}, i_{r})
           ~>
         gmp_add(i_{l}, i_{r})
      -| h

Heaps

Dereferencing the heap requires we first evaluate the expression e to obtain the address of the memory location.

g;l;h |- &e ~> &e' -| h'

---- [ Deferencing Step ]

g;l;h |- &e ~> &e' -| h'

With the address, we can then lookup the value in the heap.

g;l;h |- e ~>* addr -| h'

v = lookup(addr,h')

---- [ Deferencing ]

g;l;h |- &e ~> v -| h'

See later on when discussion statements how the addresses are created.

Method Call

Method calls are a little bit convoluted but make sense when you think about it.

Method definitions are stored on the global stack as closures. First we lookup the closure pointed to by mref and obtain the method definition.

We then evaluate all the method call’s arguments using the current heap, potentially producing a new heap.

Finally, we evaluate the method body with:

the g' as the definition of the global environment at the time of declaration;
a local stack populated by the function call’s arguments; and
the heap taken from when the arguments were evaluated.

We return the resulting value.

lookup(mref,g) = C (\{ xref_{0} : t_{0},..., xref_{n} : t_{n}} => s) g'

g;l;h |- {e_{0},...,e_{n}} ~>* {v_{0},...,v_{n}} -| h'

g', {v_{0},...,v_{n}}, h' |- s ~>* v -| h''

---- [ Method Call]

g;l;h |- mref({e_{0},...,e_{n}}))
         ~>*
         v
      -| h''

Statements

Statements are control structures for sequencing computations. Their evaluation is simple: We evaluate statements, and their expressions, using control flow statements to guide us to the final return statement.

Each statement may potentially modify the heap.

Further we introduce a statement value stop to signify that evaluation of statements has finished.

Halting Statements

Both stop and return stop the flow of statement evaluation.

Although stop does not produce a value, it signifies that we are no longer evaluating this sequence of commands.

---- [ Stop ]

g;l;h |- stop -| h

The return statement halts the computation by returning a value constructed from evaluating e.

g;l;h |- e -| h'

---- [ Intro Return ]

g;l;h |- return e -| h'

Binders

There are two binding statements: let and var. For both bindings, we do substitution occurrences of variables when evaluating a binding’s body. Instead, we perform lookup.

g;l;h           |- e ~>* v  -| h'
g;l,(xref,v);h' |- s ~>* s' -| h''

---- [ Let ]

g;l;h |- let xref : t = e; s
          ~>* s'
      -| h''

Variables also update the heap, inserting the resulting value from evaluating the ‘bound’ the expression e into the heap at a fresh address and adding the address to the local context as the variable being bound.

g;l            ;h           |- e ~>* v  -| h'
g;l,(xref,addr);h',(addr,v) |- s ~>* s' -| h''

fresh(addr)

---- [ Var ]

g;l;h |- var xref : t = e; s
          ~>* s'
      -| h''

Printing and referencing

Printing is our side-effecting operation that requires a system call to display the evaluated e.

g;l;h |- e ~>* v -| h'

system call to print v

---- [ Print ]

g;l;h |- print e ~>* stop -| h'

Mutating references requires us to update the heap with the value produced from evaluating the mutation’s RHS: e. Not to mention, returning the updated heap. We need to obtain the address of the variable by inspecting the local stack and using the address to update the heap itself.

g;l;h  |- e ~>* v       -| h'
g;l;h' |- xref ~>* addr -| h''

h''' = update(addr,h'',v)

---- [ Mutate ]

g,l |- xref = e ~>* stop -| h'''

Control Flow

Sequencing

Sequencing is where we may return early when evaluating statements. First we execute the left operand s_1

g;l;h  |- s_1 ~>* s' -| h'

---- [ Sequence Step left]

g;l;h |- s_1; s_2 ~>* s';s_2 -| h''

If s_1 eventually stop, we then move onto the second operand s_2:

g;l;h' |- s ~>* s    -| h''

---- [ Sequence Stop Left]

g;l;h |- stop; s ~>* s -| h''

If s_1 produces an early return, when return the resulting value from evaluating e and do not explore s_2 at all.

g;l;h' |- return e ~>* v    -| h''

---- [ Sequence Stop Left]

g;l;h |- return e; s ~>* v -| h''

Conditionals

Conditionals require us to evaluate the condition c first before determining which branch to take.

g;l;h |- c ~> c' -| h'

---- [ Conditional Step]

g;l;h |- if c  { tt } else { ff }
           ~>*
         if c' { tt } else { ff }
      -| h'

With a true condition we explore the true branch tt:

g;l;h |- tt ~>* v -| h'

---- [ Conditional Reduce True]

g;l;h |- if true { tt } else { ff }
           ~>*
         v
      -| h'

With a false condition we explore the false branch ff:

g;l;h |- ff ~>* v -| h'

---- [ Conditional Reduce False]

g;l;h |- if true { tt } else { ff }
           ~>*
         v
      -| h'

While

Evaluating while-loops requires that we evaluate the condition.

If the condition is false then we stop:

g;l;h |- c ~> false -| h'

---- [ While Cond False]

g;l;h |- while c { ss } : t
           ~>
         stop
      -| h'

If the condition is true, then sequence the body of the loop paired with the original loop statement.

g;l;h |- c ~> True -| h'

---- [ While Cond True ]

g;l;h |- while c { ss } : t
           ~>
         ss; while c { ss } : t
      -| h'

Methods

Evaluating methods is not terribly exciting, as they are evaluation of the method body with a pre-populated local stack. See method calls for more information.

Programs

Finally, we look at evaluating programs themselves.

Method declarations are stored as closures of the global stack.

g, (mref, C m g) |- p ~> p'

---- [ Method Declarations]

g |- mref = m; p ~>* p

Main methods, which are argument-less in Olaf, will eventually return unit as per their method prototype. When evaluating the main method both the local stack and heap are empty on input, and a populated heap is produced.

g,{},{} |- s ~>* unit -| h

---- [ Main Method]

g |- (\{} => s) ~>* unit