ExecuteAfterPut < SPL

Tags: view all tags
---+ Execute After Put

%TOC%

---++ Context

An API specific design rule for the ==tyRuBa.tdbc== package.

---++ Description

Calls to ==PreparedInsert.put*(..)== should always be followed by a call to ==PreparedInsert.executeInsert()== within the same method context.

---++ Rationale

Putting values into a ==PreparedInsert== is done with the intention of executing the
==PreparedInsert== to add facts to a TyRuBa database.

The _interesting property_ (see DesignRules) we are addressing with this design rule is: did we not forget anywhere to call the =execute= method after putting values into a =PreparedInsert=.

Adopting the design rule makes it feasible to check this property manually, or with a relatively
straightforward intraprocedural analysis, because adherence to the desing rule limits the scope of the  required analysis.

---++ Related Design Rules

A similar design rule could be formulated for ==tyRuBa.tdbc.PreparedQuery==. 

<blockquote>
Calls to ==PreparedQuery.put*(..)== should always be followed by a call to ==PreparedQuery.executeQuery()== within the same method context.
</blockquote>

It may also be possible to distil both of these desing rules into a single rule.

---++ Example

The following code contains a copy-paste bug: =salaryFact= never gets executed whereas =employeeFact= is executed twice.

<verbatim>
class Manager {

   PreparedInsert employeeFact = null; // initialized elsewhere
   PreparedInsert salaryFact = null; // initialized elsewhere
   
   ...
   void addEmployee(String managerID, String employeeID, int employeeSalary) {
       ...

       employeeFact.put("manager",  managerID);
       employeeFact.put("employee", employeeID);
       employeeFact.executeInsert();
      
       salaryFact.put("employee",  employeeID);
       salaryFact.putInt("salary", salary);
       employeeFact.executeInsert();

   }

}   
</verbatim>

This bug could be detected by a checker for our design rule using simple intraprocedural analysis.

---++ Definition

---+++ [[JQuery]]

This rule cannot be expressed in JQuery as is because it requires some dataflow.

A weaker version of the rule can be checked: all methods that call 
==PreparedInsert.put*(..)== must also call PreparedInsert.executeInsert(). 

This weaker version will find some violations of the stronger design rule, but it would not
catch the bug in the example above.

The following JQuery query finds violations of the weaker rule:

<verbatim>
   calls(?methodContext,?put,?), 
   re_name(?put,/^put/), method(?PreparedInsert,?put), name(?PreparedInsert,PreparedInsert),

   NOT( EXISTS ?execute : 
           calls(?methodContext, ?execute, ?), 
           method(?PreparedInsert,?execute), name(?execute,execute) )     
</verbatim>

Note that this would look a lot nicer if we had a nicer pattern syntax to match the method
=PreparedInsert.execute()= and =PreparedInsert.put*(..)= signatures with an AspectJ like
syntax:

<verbatim>
   calls(?methodContext, PreparedInsert.put*(..), ?), 
   NOT( calls(?methodContext, PreparedInsert.execute(), ?) )
</verbatim>

---+++ MetaL

Yes, it can be expressed, but I don't know how. Somebody fill this in?

---+++ AspectJ

Probably cannot be expressed in AspectJ. Perhaps it is possible to implement a dynamic
checker for this, but it is complicated (need to track all instances put into during
calling of a method and then check that they are all executed by the time the method exits).

---+++ HypotheticaL

*Version 1*: Makes use of explicit PCD that specify both calls must be on same instance
and within the same method context.

<verbatim>
   forall 
          calls(PreparedInsert.put*(..)) 
       && targetInstance(?this) 
       && withincode(?methodContext) )
   always followedby( 
              PreparedInsert.executeInsert() 
           && targetInstance(?this)
           && withincode(?methodContext) ) 
</verbatim>

*Version 2*:  Assumes that when a rule talks about calls to non static methods we
are implicitly assuming that calls are on the same instance.

<verbatim>
   forall 
          calls(PreparedInsert.put*(..)) 
       && withincode(?methodContext) )
   always followedby( 
              PreparedInsert.executeInsert() 
           && withincode(?methodContext) ) 
</verbatim>

*Version 3*:  Assumes as in version 2 and also makes similar asumption for the calling context (withincode).

<verbatim>
   forall calls(PreparedInsert.put*(..)) 
   always followedby( PreparedInsert.executeInsert() )
</verbatim>

---++ Ruminations

Looking at this example and in particular the different versions in the hypothethical syntax we observe some interesting ideas:

*LTL?* Forall, always, exists, never etc. seem to be useful. Do we need LTL or something like that?

*Implicit context assumptions*: It looks like a useful trick to simplify rules by implicitly assuming that multiple parts of the rule are implicitly asuming they are talking about same joinpoint and the same context, unless explicitly stating otherwise. This makes this rule look much more like the natural formulation in English.

This trick is in fact also used by AspectJ where a pointcut always implicitly talks about a single joinpoint (thisjoinpoint). The hypothethical syntax above does that as well and in version three generalizes that to all context.

*Principle:* make rules that are harder to verify harder to express. The assumption of implicit, limited methodContext scope does that. It seems like a good principle:

   * By default rules will be easy to verify
   * Presence of specific syntax elements will gives us clues on the type of analysis needed.

The assumption made that target objects for calls are assumed to be the same violates this principle. The principle would dictate that extra syntax is required to express this requirement.

*Good designs are easy to verify?*: Adopting this design rule makes the code easier to understand by people as well as making it easier to analyze. I believe this is exactly what characterizes a good design rule: it imposes limitations on structure that make it easier to convince once self of the codes correctness. Incidentally, this also makes the rule easier to check than the actual property we are trying to prove.

-- Main.kdvolder - 05 May 2005
Raw edit | More topic actions
Topic revision: r4 - 2005-05-07 - KrisDeVolder