<s5>Æliens</s5> -- slide(s)

Expressions

syntax

$e ::= v | x.v$

Elementary statements

$s ::= v = e | x = new %t | x.m(e)$

Compound statement

$S ::= %e | s | S1;S2 | \! if (b) S | while (b) S$

slide: The syntax of a simple OO language

Assignment

rules

$<< v = e, %f^{%a} >> -> << %e, %f [ %a.v := e_{%f} ] >>$

Object creation

\ffrac{ $<< S_{%t}, %f^{%a} >> \apijl{%l} << %e, %f' >>$ }{ $<< x \! = \! new %t, %f >> \! \apijl{ %a \. %l } \! << %e , %f'[ x \! := %a \! ]>>$ }

Method call

\ffrac{ $<< S_m(e), %f^{%a} >> \apijl{%l} << %e, %f' >>$ }{ $<< x.m(e), %f >> \apijl{ m_{%a} \. %l } << %e, %f' >>$ }

slide: Transition system -- rules

Composition

compound

\ffrac{ $<< S_1, %f >> \apijl{ %l_1 } << %e, %f' >>$ \ifsli{\hspace{-0.5cm}}{\hspace{1cm}} $<< S_2, %f' >> \apijl{ %l_2 } << %e, %f'' >>$ }{ $<< S_1;S_2, %f >> \apijl{ %l_1 \. %l_2 } << %e, %f'' >>$ }

Conditional

$<< \! if (b) S, %f>> -> << %e, %f>>$ if $%f(b) == false$
\ffrac{ $<< S, %f >> \apijl{%l} << %e, %f' >>$ }{ $<< \! if (b) S, %f >> \apijl{%l} << %e, %f' >>$ } if \ifsli{ $%f(b)$ }{ $%f(b) == true$ }

Iteration

$<< while \; (b) S, %f>> -> << %e, %f>>$ if $%f(b) == false$
\ffrac{ $<< S, %f >> \apijl{%l} << %e, %f' >>$ }{ $<< while (b) S, %f >> \apijl{%l} << while (b) S, %f' >>$ } \ifsli{}{ if $%f(b) == true$ }

slide: Transition system -- compound statement

Program

$x = new ctr; x.inc(); v = x.n$

Transitions

$<< x = new ctr, %f_1 >> \apijl{ctr_1} << %e, %f_1[ x := ctr_1 ]>>$

$[1]$

$<< n = n + 1, %f_2^{%a} >> -> <<%e, %f_2[%a.n = %a.n + 1]>>$

$[2]$

$<< x.inc(), %f_2 >>$ $\apijl{inc_{%a}$ $<< %e, %f_2[%f_2(x).n := %f_2(x).n ]>>$

$[2']$

$<< v = x.n, %f_3>> -> << %e, %f_3[v := %f_3(x).n] >>$

$[3]$

Trace

$%f \apijl{%l} %f'$ with $%f = %f_1$ , $%f' = %f_3$ and $%l = ctr_1 \. inc_{ %a }$

slide: Transitions -- example