Structured Behavioral Programming Idioms

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.

1. 1.

   The experiment design and execution was also approved by an ethical committee.

2. 2.

   https://bp-new-blockly-exp-2.appspot.com/static/apps/mazeBP/index.html?version=1(version=2). Designed to work with the Firefox web browser.

3. 3.

   The questionnaires can be found in https://tinyurl.com/h3bzphs, https://tinyurl.com/zah4ap3.

This research was partially supported by the Israel Science Foundation, the Philip M. Klutznick Research Fund, and the Dora Joachimowicz research grant.

Authors and Affiliations

1. Ben Gurion University of the Negev, Beer Sheva, Israel

   Adiel Ashrov, Arnon Sturm & Gera Weiss

2. Holon Institute of Technology, Holon, Israel

   Michal Gordon

3. The Weizmann Institute of Science, Rehovot, Israel

   Assaf Marron

Corresponding author

Correspondence to Arnon Sturm .

Editors and Affiliations

1. University of Haifa , Haifa, Israel

   Iris Reinhartz-Berger

2. University of Duisburg-Essen , Duisburg, Germany

   Jens Gulden

3. Université de Paris 1 Panthéon - Sorbonne, Paris, France

   Selmin Nurcan

4. Luxembourg Institute of Science and Technology, Esch-sur-Alzette, Luxembourg

   Wided Guédria

5. Saint Louis University , St. Louis, Missouri, USA

   Palash Bera

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 )}} . ∎

Reprints and permissions

© 2017 Springer International Publishing AG

Policies and ethics