Structured Behavioral Programming Idioms

Abstract

Behavioral Programming (BP) is a modelling and programming technique proposed for specifying and for implementing complex reactive systems. While effective, we report on a weakness that stems from the verbosity and from the complexity of the programming constructs in BP. Our analysis, described in this paper, shows that developers who work with BP use specific patterns that allow them to control the complexity of their specification. Thus, the main contribution of this paper is a set of specification constructs that represent those patterns. We report on the design of the new idioms, termed structured constructs for behavioral programming and on an empirical evaluation in a controlled experiment that proved their effectiveness. In particular, the experiment examined the comprehensibility differences between behavioral specifications with non-structured BP programming idioms and with the structured ones. The results indicate that the new structures improve the comprehension of the behavioral specification.

Appendix

While the focus of this work is on empirical evaluation of the idioms, in terms of their usability to programmers, we hereby provide a proof for the expressiveness equivalence of the two sets of idioms.

Claim 1:

Every b-thread developed with the structured idioms can be translated to a semantically equivalent b-thread that applies only the bSync idiom using If last_event==x {} and break .

Proof:

By structural induction.

Induction base: if there is no Break-upon or Blocking structures in the program, replace each request(x) and each wait-for(y) with, respectively, a bSync(x,none,none) and a bSync(none,y,none) .

Induction step: Assume, by induction, that the claim is true for programs with at most $n$ levels of nesting of the Break-upon or Blocking structures. Given a program with $n + 1$ levels of nesting we can replace each block of maximal nesting level as follows. If the nesting level of the block is less than $n + 1$, it can be replaced by a code that uses only bSync by the induction assumption. For a block of the form blocking(x){ P } , where $P$ is some code with $n$ levels of nesting, let $P^{\prime}$ be a code, given by the induction assumption, that is semantically equivalent to $P$ and uses only the bSync idiom. Let $P^{\prime\prime}$ be the code obtained by adding $x$ to the list of blocked events in every bSync in $P^{\prime}.$ We can now replace the code Blocking ( x ) { P } with $P^{\prime\prime}$. Similarly, for a block of the form { P } break-upon( x ) , where $P$ is some code with $n$ levels of nesting, let $P^{\prime}$ be a code, given by the induction assumption, that is semantically equivalent to $P$. Let $P^{\prime\prime}$ be the code obtained by adding $x$ to the list of waited-for events in each bSync in $P^{\prime}.$ Let $\varvec{label}$ be a name that does not appear as a label in $P^{\prime\prime}$ and let $P^{\prime\prime\prime}$ be the code obtained by adding the commands If last_event== x {break $\varvec{label}$ } after each bSync in $P^{{\prime \prime }} .$ We can now replace the code { P } break-upon( x ) with $\varvec{label}$: {$P^{\prime\prime}$}. Clearly, the code obtained after all the above replacements contains only bSync , with no application of the structured idioms, and is semantically equivalent to the original code. This proves our claim. ∎

In fact, the above proof follows the way we have implemented the structured idioms.

Another issue that should be clarified in the above proof is the semantics of waiting-for or requesting an event while, at the same time, blocking it. This can be done with bSync , when some event is specified both in the waited-for or in the requested lists and in the blocked list. It can also be done with the structured idioms, when an event is requested or waited-for in the scope where it is specified as blocked or a break upon event. In this case, one must decide which specification takes priority – whether to ignore the blocking or to ignore the request or wait-for. It easy to verify that the above proof is correct as long as we use the same priority order in both the bSync and in the structured idioms.

Claim 2

Every b-thread developed with bSync idiom can be translated to a semantically equivalent b-thread that uses only the structured idioms.

Proof

Replace each bSync( x , y , z ) with blocking( x ){break-upon( y ) {request( x )}} . ∎