topical media & game development

---

[] readme course(s) preface I 1 2 II 3 4 III 5 6 7 IV 8 9 10 V 11 12 afterthought(s) appendix reference(s) example(s) resource(s) _

---

object-oriented programming

On the notion of behavior

The assertion logic presented in the previous section allows us to reason about the behavior of a system without explicitly generating the possible sequences of states resulting from the execution of the program. However, underlying the inference rules of our assertion logic we need a mathematical model for the operational behavior of a system. An operational model is needed to prove the soundness of the inference rules. Further, an operational model may aid in understanding the meaning of particular language constructs and their associated correctness rules. In the following we will sketch the construction of a transition system modeling the behavior of an object-based program. Studying the formal semantics is relevant to understanding object orientation only in so far as it provides a means with which to characterize the desired behavior of object creation and message passing in an unambiguous manner.

Transition system

A transition system for a program is a collection of rules that collectively describe the effect of executing the statements of the program. A labeled transition system is one that enables us to label the transition from one state to another by some label indicating the observable behavior of a program step. In the transition system defined below, we will employ states $\%f$, which may be decorated by object identifiers $\%a$, as in $\%f^\{\%a\}$. Object identifiers are created when creating a new instance of an object type $\%t$. We assume newly created object identifiers to be unique. We assume that each object type $\%t$ has a constructor (which is a, possibly empty, statement that we write as $S\_\{\%t\}$) and an arbitrary number of methods m. Each method m is assumed to be defined by some statement, which we write as $S\_m\; (e)$, for method calls of the form $m(e)$. Also we allow an object $\%a$ of type $\%t$ to have attributes or instance variables v that may be accessed (read-only) as $\%a.v$ for an object identifier $\%a$ or $x.v$ for an object variable x (which must have $\%a$ as its value). To determine the visible behavior of a program, we will employ labels of the form $\%a$ (to denote the creation of an object $\%a$) and $m\_\{\%a\}$ (to indicate the invocation of a method m for object $\%a$). We allow transitions to be labeled by sequences of labels that we write as $\%l$ and which are concatenated in the usual way. We will define a transition system for a simple language of which the syntax is defined in slide 10-syntax.

---

Expressions

syntax

• $e\; ::=\; v\; |\; x.v$

Elementary statements

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

Compound statement

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

---

slide: The syntax of a simple OO language

---

Expressions are either local variables v or object instance variables that we write as $x.v$, where x is an object variable. As elementary statements we have $v\; =\; e$ (indicating the assignment of (the value of) an expression e to a local variable v), $x\; =\; new\; \%t$ (which stands for the creation of a new object of type $\%t$), and $x.m(e)$ (which calls a method m with arguments e for object x). The object variable x is associated with an object identifier $\%a$ by the state $\%f$ in which the statement in which x occurs is executed. As compound statements we have an empty statement $\%e$ (which is needed for technical reasons), an elementary statement s (as defined above), a sequential composition statement, a conditional statement and an iteration statement, similar to that in the previous section. The transition rules for elementary statements are given in slide 10-rules.

---

Assignment

rules

Object creation

• \ffrac{}{ }

Method call

• \ffrac{}{ }

---

slide: Transition system -- rules

---

The assignment rule states that the assignment of (the value of) an expression e to a (local) variable v in state $\%f$ decorated by an object identifier $\%a$ results in the empty statement and the state $\%f$ modified by assigning the value of e in $\%f$ (which is written as $e\_\{\%f\}$) to the instance variable v of object $\%a$. Hence, decorations allow us to work in the local environment of the object indicated by the decoration. The object creation rule states that if we assume a transition (which states that the constructor for type $\%t$ executed in state $\%f$ decorated by $\%a$ results in the state $\%f\text{'}$ with behavior $\%l$) then we may interpret the creation of a new $\%t$ object to result in behavior $\%a\; \backslash .\; \%l$ (where $\%a$ is the newly created object identifier) and state $\%f\text{'}$ in which the object variable x has the value $\%a$. Finally, in a similar way, the method call rule states that if we assume a transition (which states that executing the statement $S\_m(e)$, that is the code associated with method m and arguments e, for object $\%a$ in state $\%f$, results in behavior $\%l$ and state $\%f\text{'}$) then we may interpret the method call $x.m(e)$ in $\%f$ as a transition to state $\%f\text{'}$ displaying behavior $m\_\{\%a\}\; \backslash .\; \%l$. The rules for object creation and method call already indicate that transition rules may be used to construct a complex transition from elementary steps. In other words, a transition system defines a collection of proof rules that allow us to derive (state) transitions and to characterize the behavior that may be observed. To obtain a full derivation, we need in addition to the rules for elementary statements the rules for compound statements listed in slide 10-compound.

---

Composition

compound

• \ffrac{ \ifsli{\hspace{-0.5cm}}{\hspace{1cm}} }{ }

Conditional

• if $\%f(b)\; ==\; false$
• \ffrac{ }{ } if \ifsli{$\%f(b)$}{$\%f(b)\; ==\; true$}

Iteration

• if $\%f(b)\; ==\; false$
• \ffrac{ }{ } \ifsli{}{ if $\%f(b)\; ==\; true$ }

---

slide: Transition system -- compound statement

---

The composition rule states that if a statement $S\_1$ transforms $\%f$ into $\%f\text{'}$ with behavior $\%l\_1$ and $S\_2$ transforms $\%f\text{'}$ into $\%f\text{'}\text{'}$ with behavior $\%l\_2$ then the compound statement $S\_1;S\_2$ transforms $\%f$ into $\%f\text{'}\text{'}$ with behavior $\%l\_1\; \backslash .\; \%l\_2$. The conditional rules state that, dependent on the value of the boolean b, the statement $if\; (b)\; S$ has either no effect or results in a state $\%f\text{'}$ assuming that S transforms $\%f$ into $\%f\text{'}$ with behavior $\%l$. The iteration rules state that dependent on the value of the boolean b the statement $while\; (b)\; S$ has either no effect or results in a state $\%f\text{'}$ assuming that S transforms $\%f$ into $\%f\text{'}$ with behavior $\%l$. In contrast to the conditional, an iteration statement is repeated when b is true, in accordance with our operational understanding of iteration.

Example

In our rules we have made a distinction between unadorned states $\%f$ and states $\%f^\{\%a\}$ decorated with an object identifier $\%a$. This reflects the distinction between the execution of a program fragment in a global context and a local context, within the confines of a particular object $\%a$. Assume, for example, that we have defined a counter type ctr with a method inc that adds one to an instance variable n. In slide 10-t-example, a derivation is given of the behavior resulting from a program fragment consisting of the creation of an instance of ctr, a method call to inc and the assignment of the value of the attribute n of the counter to a variable v.

---

Program

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

Transitions

$[1]$




$[2]$



• $\backslash apijl\{inc\_\{\%a\}$

$[2\text{'}]$




$[3]$

Trace

• $\%f\; \backslash apijl\{\%l\}\; \%f\text{'}$ with $\%f\; =\; \%f\_1$, $\%f\text{'}\; =\; \%f\_3$ and $\%l\; =\; ctr\_1\; \backslash .\; inc\_\{\; \%a\; \}$

---

slide: Transitions -- example

---

To derive the transition $\%f\; \backslash apijl\{\%l\}\; \%f\text{'}$ corresponding with the program fragment $x\; =\; new\; ctr;\; x.inc();\; v\; =\; x.n$ we must dissect the fragment and construct transitions for each of its (elementary) statements as shown in $[1]$, $[2]$ and $[3]$. The second statement, the method call $x.inc()$, needs two transitions $[2]$ and $[2\text{'}]$, of which the first represents the execution of the body of inc in the local context of the object created in $[1]$ and the second represents the effect of the method call from a global perspective. For the first statement, we have assumed that the constructor for ctr is empty and may hence be omitted. Notice that the object identifier $\%a$ (introduced in $[1]$) is assumed in $[2]$ to effect the appropriate local changes to n. After constructing the transitions for the individual statements we may compose these transitions by applying the composition rule and, in this case, identifying $\%f\_2$ with $\%f\_1[x\; :=\; \%a\; ]$ and $\%f\_3$ with $\%f\_2[\; \%a.n\; :=\; \%a.n\; +\; 1]$. As observable behavior we obtain $ctr\_1\; \backslash .\; inc\_\{\%a\}$ (where $ctr\_1\; =\; \%a$), which represents the creation of a counter and its subsequent modification by inc.

Discussion

Transition systems, such as the one given above, were originally introduced as a means to model the behavior of CSP. They have been extensively used to model the operational semantics of programming languages, including concurrent and object-oriented languages. See, for example,  [ABKR89] and  [Eliens92]. In  [AptO], transition systems have been used as a model to prove the soundness and completeness of correctness rules for concurrent programming constructs. Also in  [AmBo93], transition systems are used to demonstrate the validity of a proof system for a parallel object-oriented programming language. The interested reader is invited to explore the sources mentioned for further study.

---

[] readme course(s) preface I 1 2 II 3 4 III 5 6 7 IV 8 9 10 V 11 12 afterthought(s) appendix reference(s) example(s) resource(s) _

---

(C) Æliens 04/09/2009

You may not copy or print any of this material without explicit permission of the author or the publisher. In case of other copyright issues, contact the author.