🚀 go-pugleaf

Let me address the apparent difference between our experience of
Cleanroom in CICS and that of the COBOL/SF project.  This was queried
by Dan Craigen after my talk at the last Z User Meeting.  After consulting
the Cleanroom Software Technology Center, I can now respond.

The discrepancy was in the area of cost-effectiveness.  I maintain
that using Cleanroom with the Z language is not generally cost-effective
in a commercial environment whereas the COBOL/SF project documented by
Dan Craigen showed a reasonable productivity.

Of course, it is impossible to compare productivity levels on different
projects with any accuracy especially given the differences between the
two projects and the teams which worked on them.  However, the
differences are significant, so I will try to offer an explanation.

Where we have been able to apply Cleanroom techniques. our productivity
has been reasonable and we met our target dates.  In other areas, we
have written Z specifications but have found the process of refinement,
documenting correctness criteria, and proving them correct in a team
review to be unachievable for a number of reasons:

1. CICS/ESA is a 20-year old software product.  To restructure a
   component requires equivalent function to be maintained otherwise
   much other old code needs to be reworked, at a large cost.

   This makes the interfaces between restructured components and
   the old code more complex than would have been the case in a
   newer, better structured product such as COBOL/SF.

2. CICS/ESA depends very much on other complex software products such
   as MVS, VTAM, RACF, VSAM, etc.   There are no formal specifications
   of the interfaces to these products which greatly increases the cost
   of formal refinement down onto these interfaces.

   I suspect that similar problems in COBOL/SF are on a much smaller
   scale.  COBOL/SF transforms a Cobol program into another equivalent
   program with better structure, so its main external interfaces are
   for file input and output.  This is an order of magnitude simpler
   than a transaction processor's requirements on other products.

3. The performance of a transaction processor such as CICS is critical
   to its customers' businesses whereas the performance of COBOL/SF is
   not.  So CICS cannot avoid heavy use of features of a programming
   language, such as pointers, which enable good performance.  This
   increases the proof burden considerably.

   We found the proof rules for the assignment statement complex and
   difficult to apply in the presence of pointers, aliasing, and other
   complexities inherent in our target language (a subset of a systems
   programming flavour of PL/1).

   In contrast, Mark Pleszkoch of the Cleanroom Software Technology
   Center comments:

     "In the COBOL/SF project specifically, the use of pointers and
      arrays was quickly encapsulated, so that the vast majority of
      the code dealt in terms of higher-level abstract data types
      such as stacks and queues."

4. CICS code has to deal with concurrency; COBOL/SF is a sequential
   program.

5. Our approach with Z was fairly formal.  We wrote formal specifications
   in Z.  Our refinement approach, which we were unable to afford on a
   large scale, was to document data and operation refinements in Z and
   to write down the correctness criteria as mathematical theorems.  In
   addition, we worked on a denotational semantics of the implementation
   language subset which gave us an understanding of some of the
   underlying complexities of this language.

   Mark Pleszkoch comments:

     "In terms of formality, we are definitely much less formal than
      typical Z users.  There is a formal basis for Cleanroom, and we
      at the CSTC have worked to derive formal proof rules for the
      complications that you mentioned, but we find that most of the
      teams (especially the U.S. based teams) don't apply verification
      at the level of formality where these issues surface.  Instead,
      we concentrate in the Cleanroom education on the intuitive level,
      so that people know a correct intended function when they see
      one."

     "I believe that the key to applying Cleanroom in a cost-effective,
      highly productive manner is to not force developers to go to a
      level of formality beyond their needs (and abilities), while at
      the same time not losing the benefits of precise documentation
      that makes clear what each piece of code is designed to do."

Glyn Normington

CICS Products
IBM Hursley