Skip to content

docs(research): GenApp LGACDB01: two independent translations, scanned and proven #4176

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
squid-protocol merged 5 commits into from
Oct 2, 2026
Merged

docs(research): GenApp LGACDB01: two independent translations, scanned and proven #4176

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
0361bb0
docs(research): GenApp LGACDB01, two independent translations, scanne…
squid-protocol Oct 2, 2026
260b1db
merge main
squid-protocol Oct 2, 2026
2498349
docs(wiki): 05-18 -- the model ports' 46 TODOs are mostly the scaffol…
squid-protocol Oct 2, 2026
e7c8768
merge main
squid-protocol Oct 2, 2026
77e69f0
docs(research): LGACDB01 -- harness results for IBM's Java (#4177), o…
squid-protocol Oct 2, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
231 changes: 231 additions & 0 deletions docs/research/lgacdb01-four-way.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,231 @@
# One program, two independent translations: GenApp LGACDB01, scanned and proven

*A post-hoc comparison. Status: draft for review, 2026-10-02.*

## Abstract

GenApp's LGACDB01 (the add-customer program in IBM's CICS General Insurance sample) has been translated to Java twice, independently:
- **by IBM's watsonx Code Assistant for Z (WCA4Z)**, as published with IBM Research's validation papers (Kumar et al., ASE 2024; Hans et al., 2025);
- **by GitGalaxy's deterministic translator ("det port")**, as part of this project.

We compare four files: the original COBOL, the COBOL that IBM's refactoring step produced, IBM's Java, and our det port. We use three lenses:
1. IBM's published validation results;
2. our end-to-end equivalence harness;
3. GitGalaxy's static scanner.

The two translations make opposite trade-offs:
- **IBM's Java** is compact and readable. It covers one of the program's five paragraphs, and leaves the date of birth and the error path in commented-out lines.
- **Our det port** covers the whole program and the two programs it LINKs to, and is proven against real Db2 on four scenarios. But it is about 7× the COBOL's code lines, and its scenarios reach only 6 of 14 branches.

**Harness result.** We ran IBM's published `insertCustomer` unmodified, inside our proven det port, against real Db2. It was not equivalent on any of our four scenarios:
- Db2 refused every INSERT, because the date-of-birth parameter is never bound.
- The failure was swallowed.
- No CUSTOMER row was written, and the task carried on as if it had succeeded.

IBM's published JUnit test does not compile against the published Java. IBM's own recorded run in the same repository shows 2 passes (both skipped tests) and 2 failures, not the 4/4 the papers report.

**The comparison cut both ways.** It also exposed a bug in our det port, on a GenApp error path none of our proofs reach (#4181), and two GitGalaxy scanner defects (#4170, #4171).

## 1. Provenance and independence

This is a post-hoc comparison, not a designed experiment.
- **No reference to IBM's work.** GitGalaxy's translator, its equivalence harness and the GenApp cases were built without reference to IBM's papers, code or tests. We did not assess IBM's method or tests while building ours.
- The first GenApp det ports were proven on 2026-10-01 (commit 3504f767f).
- LGACDB01 was proven on 2026-10-02 (commit 7def28a8a). Its proof needed CICS named counters, which were added for it.
- **How the comparison came about.** Only afterwards, the same day, did we search for published results on the same programs. We found that IBM's validation papers report on LGACDB01 and other GenApp programs, and that IBM published its LGACDB01 Java.
- **What is shared.** The two efforts share only the input program, GenApp, which is public at github.com/cicsdev/cics-genapp.

This document asks one question: *we translated the same program, so how does our result compare with a published one?*

## 2. Subjects

| File | Source | Lines | Notes |
|---|---|---|---|
| Original COBOL | `cics-genapp` `base/src/lgacdb01.cbl` | 328 | What our det port translates. 5 paragraphs: MAINLINE, MAINLINE-EXIT, Obtain-CUSTOMER-Number, INSERT-CUSTOMER, WRITE-ERROR-MESSAGE. |
| IBM's refactored COBOL | `sandeephans/validation-c2j` @ `967d00b` `LGACDB01.cbl` | 418 | Header: "Generated by: IBM watsonx Code Assistant for Z Refactoring Assistant", created 2024-06-11. A slice: INSERT-CUSTOMER and WRITE-ERROR-MESSAGE only, with copybook data inlined. |
| IBM's Java | same repo, `generated_code/java/com/ibm/wcaz/implementation/Lgacdb01.java`, plus 21 data-model/record classes | 184 | Model-written. One business method, `insertCustomer`; the rest is boilerplate (getters, `equals`, byte conversion). |
| Our det port | `det_port.py run genapp-lgacdb01` at main 582caf5f7, `Lgacdb01Service.java` | 1,629 | Rule-translated, statement for statement, over the cobolrt runtime. LGACVS01 and LGACDB02, which it LINKs to, are translated alongside it. |

IBM's repository carries no licence. We fetch it at a pinned commit and do not redistribute it. This document quotes only a few lines.

## 3. Methods

### 3.1 IBM's published validation (as reported; not reproduced here)
IBM's method validates a single paragraph:
- **COBOL tests.** Tests are generated by symbolic execution and run on a real z/OS system, with resource access (SQL, CICS) handled by debugger scripts.
- **Java tests.** The recorded inputs and outputs become JUnit tests. Resource calls are mocked in order, and their arguments are asserted.

For LGACDB01, they selected the INSERT-CUSTOMER paragraph and reported (Kumar et al. 2024, Table 1):
- 100% of paths and branches covered, with 4 paths;
- 11 program outputs and 6 resource outputs;
- 22 assertions (3 on program variables, 19 on resource arguments);
- 4/4 JUnit tests passing.

Across 33 GenApp and IMS Bank programs (105 paragraphs), 84% of the multi-path paragraphs reached full branch coverage (Hans et al. 2025).

### 3.2 Our equivalence harness
Our method validates a whole program in its task:
- **Reference.** The reference behaviour is GnuCOBOL 3 (IBM dialect, EBCDIC signs, TRUNC(STD)) running the original program under our CICS model. SQL goes through our precompiler stub to IBM Db2 Community Edition.
- **The Java side.** The Java port runs the same scenarios against the same Db2 schema.
- **What is compared, byte for byte.** CICS events, the returned COMMAREA, written datasets and every compared table.
- **Case contents.** The LGACDB01 case runs LGACVS01 and LGACDB02 in the same task, and includes named counters. Its four scenarios are hand-written: `add-with-counter`, `add-without-counter`, `add-blank-optional-fields`, `add-long-email`.
- **Limits.** Where our reference may differ from z/OS is listed in `docs/language_status/oracle_assumptions.md`.

### 3.3 GitGalaxy static scan
Each file was scanned on its own with `galaxyscope` at main 582caf5f7, with default settings. The det port is admitted by its provenance header (#4164). We report `file_data` and `function_data` readings.

## 4. Results

### 4.1 What each translation covers

| COBOL paragraph | Original | IBM's refactored COBOL | IBM's Java | Our det port |
|---|---|---|---|---|
| MAINLINE (commarea checks, counter or identity choice, LINKs) | yes | removed | none | `p0` |
| MAINLINE-EXIT | yes | removed | none | `p1` |
| Obtain-CUSTOMER-Number (GET COUNTER) | yes | removed | none | `p2` |
| INSERT-CUSTOMER | yes | yes | `insertCustomer` | `p3` |
| WRITE-ERROR-MESSAGE | yes | yes | call commented out | `p4` |
| LINKed LGACVS01, LGACDB02 | called | — | — | translated, run in the same task |

IBM's papers describe validating one paragraph per program, and this repository reflects that scope. The comparison below is therefore uneven by design: a paragraph translation against a program translation. We note where that matters.

### 4.2 Validation results

| | IBM (reported) | Ours |
|---|---|---|
| Unit | INSERT-CUSTOMER paragraph | Whole task: LGACDB01, LGACVS01, LGACDB02 |
| Reference | z/OS (real) | GnuCOBOL, CICS model, real Db2 LUW |
| Resources on the Java side | Mocked (in-order call stubs) | Real Db2 tables, named counters, VSAM model |
| Tests / scenarios | 4 generated (one per path) | 4 hand-written |
| Coverage | 100% of the paragraph's paths and branches | 3/4 paragraphs, 6/14 branches of the program |
| Outcome | 4/4 pass | Proven: every scenario's events, COMMAREA, datasets and tables equal |

IBM's coverage is complete for the unit it chose. Ours is lower but spans the whole program: the INSERT failure path (`MOVE '90' TO CA-RETURN-CODE`, `PERFORM WRITE-ERROR-MESSAGE`) is never reached, because our harness doesn't inject SQL failures (#4173). IBM's symbolic test generation is the stronger approach to coverage (#4175).

### 4.3 IBM's Java run through our harness
Full record: `docs/language_status/ibm_wca4z_lgacdb01.md`, tooling in #4177.

**Setup.** IBM's `Lgacdb01.insertCustomer` (validation-c2j @967d00b) runs unmodified, in place of our det port's INSERT-CUSTOMER method. The rest of the task is our proven det-port code: LGACDB01's other paragraphs, LGACVS01 and LGACDB02. A thin adapter, committed separately, does three things:
- marshals the paragraph's host variables through IBM's own setters;
- registers a JDBC driver for IBM's placeholder URL `endpoint_url`, returning the task's transaction-bound Db2 connection;
- adds a JZOS compile shim that is never called at run time.

The adapter judges only the paragraph IBM translated.

**Which COBOL to compare against.** IBM's refactored INSERT-CUSTOMER is textually identical to the stock paragraph, and uses the same data layout on its success path. The refactored program cannot run as a reference itself: it has no mainline, its COMMAREA is in WORKING-STORAGE, and every run falls through into WRITE-ERROR-MESSAGE. So the stock case's scenarios test exactly what IBM translated.

| Scenario | Stock COBOL (reference) | With IBM's INSERT-CUSTOMER |
|---|---|---|
| add-with-counter | Return code '00'; CUSTOMER row 1000011 | Db2 -4461, "Invalid parameter 4: Parameter is not set nor registered"; printed and swallowed; no row |
| add-without-counter | '00'; row 1000001 | -4461 on parameter 3; no row; CA-CUSTOMER-NUM returned as 0 |
| add-blank-optional-fields | '00'; row 1000020 | -4461 on parameter 4; no row |
| add-long-email | '00'; row 1000030 | -4461 on parameter 4; no row |

**Not proven on any scenario.** In every run the task continues as if the insert had worked. LGACDB02's CUSTOMER_SECURE insert then violates its foreign key to CUSTOMER, and the run ends on GenApp's LGSTSQ error path.

**Root causes, verified in IBM's code:**
1. DATEOFBIRTH is never bound: `// ps.setDate(4, …getDateofbirth());`, and `ps.setDate(3, …)` in the branch that takes the key from Db2.
2. The failure is swallowed: `// caReturnCode = 90;` and `// errorMsg.writeErrorMessage();`, with `System.out.println("[EXCEPTION CAUGHT] " + exception);` in their place.
3. In the branch that takes the key from Db2, a failure leaves the customer number at 0.

**IBM's own test artifacts.** The generated JUnit test calls `insertCustomer()` with no arguments, while the published method takes three, so it does not compile against the published Java. The repository's recorded run (`generated_code/cache/Lgacdb01.insertCustomer.json`) shows:
- tests 1 and 3 passing: these are the SQL-error paths, and their bodies are skipped;
- tests 2 and 4 failing with `expected:<[xxxxxxxx]> but was:<[]>`.

Test 2 asserts every CUSTOMER column, DATEOFBIRTH included, so IBM's method, when it runs, does appear to flag this translation. The papers' 4/4 may come from a different version of the Java (the cache file points at another working copy). We note the mismatch; we do not infer the cause.

**A bug in our own det port.** Forcing the error path exposed it. `LINK LGSTSQ COMMAREA(ERROR-MSG)` passes a 71-byte record, but the det port marshals it with a wider record layout and reads past the end (#4181). None of our proofs reach this path, because the harness injects no SQL failures (#4173). A clamp in the scratch copy made it possible to observe IBM's results; the clamp was not committed.

### 4.4 GitGalaxy scan, file level

| Reading | Original COBOL | IBM refactored COBOL | IBM Java | Det port |
|---|---|---|---|---|
| Code lines | 213 | 320 | 143 | 1,495 |
| Functions / paragraphs | 5 | 2 | 22 (1 business) | 32 |
| Branch points | 11 | 8 | 22 † | 126 † |
| State mutations | 30 | 10 | 24 | 331 |
| Guards (safety) | 3 | 2 | 11 | 12 |
| I/O signals | 6 | 3 | 4 | 4 |
| Inter-program calls (IPC) | 14 | 8 | 0 | 10 |
| API signals | 1 | 1 | 24 | 8 |
| Print statements | 1 | 1 | 2 | 0 |
| Imports / copybooks | 3 | 0 | 8 | 23 |
| Token mass | 2,764 | 4,718 | 1,539 | 89,943 |
| Risk: tech debt | 21 | 12 | **84** | 10 |
| Risk: cognitive load | 76 | 22 | 59 | 29 |

† Java branch counts are inflated by #4170. In IBM's Java, 19 of the 22 come from `?` placeholders in its two SQL strings. In the det port, its 22 ternaries count twice.

### 4.5 The shared paragraph: INSERT-CUSTOMER

| | Lines | Complexity as scanned | Complexity corrected |
|---|---|---|---|
| COBOL (both versions identical in this paragraph's logic) | 73 | 4 | 4 |
| IBM `insertCustomer` | 55 | 21 | ≈2–3 (#4170) |
| Det `p3` | 65 | 7 | lower once #4170 is fixed |

### 4.6 Static reading of IBM's `insertCustomer`
Eleven lines of IBM's `Lgacdb01.java` are commented-out code. They include, in both INSERT branches:
```java
// ps.setDate(4, caCustomerRequest.getGenasa1Customer().getDateofbirth());
```
and, in both exception handlers:
```java
// caReturnCode = 90;
// errorMsg.writeErrorMessage();
```
In their place is `System.out.println("[EXCEPTION CAUGHT] " + exception);`. The connection is the placeholder `DriverManager.getConnection("endpoint_url")`.

Reading the code alone predicts that, against a real database, the unset DATEOFBIRTH parameter makes the INSERT fail, and that the failure is printed and swallowed, so the caller sees no error return. Section 4.3 confirms each part of that prediction.

GitGalaxy's tech-debt risk reads 84 for this file, against 10 for the det port. But its commented-out-code signal reads 0, because the Java rule only recognises commented lines that begin with a keyword (#4171).

## 5. What each lens can and cannot see

| Lens | Sees | Misses |
|---|---|---|
| IBM validation (as published) | Every path of the chosen paragraph. The arguments passed to each resource call: test 2 asserts DATEOFBIRTH, so it should flag the unbound parameter whenever it compiles and runs. A real z/OS reference. | Other paragraphs. How the real database reacts, such as refusing an unset parameter, because resources are mocked. Its SQL-error tests were skipped in the published run. |
| Our harness | The whole task against real Db2 and a CICS model, compared byte for byte. | Branches no scenario reaches, such as SQL error paths (#4173). Reference differences listed in the oracle register (GnuCOBOL, not z/OS). |
| GitGalaxy scan | Scope (functions, IPC dropping to 0), debt pressure, output by print, size and token cost, all without running anything. | Behaviour. Equivalence. Commented-out statements in Java (#4171). Its Java complexity is unreliable around SQL strings and ternaries until #4170 is fixed. |

The lenses complement each other:
- **The scan** flagged IBM's file in seconds, without running it: inter-program calls 14 → 0, tech-debt 84, errors handled by printing.
- **Our harness** settled the question against a real database. The program was not equivalent, and the reason traced to exact lines.
- **IBM's path-complete test generation** covers the branches our hand-written scenarios miss. Our missing error-path coverage is also why our own ERROR-MSG bug (#4181) went unproven.

## 6. Threats to validity
- **One program, and an uneven comparison.** This is a single program, and IBM's published Java is a single paragraph. We do not generalise to WCA4Z's quality.
- **IBM's code is old.** It dates from 2024 (COBOL slice 2024-06-11, repository 2024-10-11) and may not reflect the current product.
- **The published artifacts may not match what the paper evaluated.** The recorded test run points at another working copy of the Java.
- **The adapter is ours.** It is committed and documented separately, and it touches only the marshalling and the connection.
- **IBM's reported validation passes on its own terms.** Any divergence we find concerns behaviour outside its mocked scope; it does not show their tests were wrong for what they assert.
- **Our reference is not z/OS.** See `oracle_assumptions.md`.
- **Our coverage is modest.** 6/14 branches.
- **Scanner readings carry the bugs in #4170 and #4171.** They will be re-measured after those fixes.

## 7. Follow-ups
- #4170: Java `?`/`:` overcount (fix in progress).
- #4171: Java commented-out-code detection.
- #4173: SQL fault injection in the harness.
- #4174: det port of LGIPVS01, to complete the overlap with IBM's published GenApp set.
- #4175: solver-driven scenario generation.
- #4179: remove the scaffold's TODO docstrings from adopted model ports.
- #4181: det port marshals LINK COMMAREA(ERROR-MSG) past its 71 bytes.

## 8. Reproducing
```sh
# det port and proof (see .claude/skills/det-port/SKILL.md for the environment)
python tests/tools/det_port.py run genapp-lgacdb01 --faults all --work <scratch>
# scans: each file in its own committed git tree, then
python -m gitgalaxy.galaxyscope <tree>
# IBM's code through the harness (fetches validation-c2j at 967d00b, never committed)
python tests/tools/ibm_wca4z_port.py --work <scratch> --junit # see docs/language_status/ibm_wca4z_lgacdb01.md for the per-scenario run
```

## References
- A. Kumar, D. Saha, T. Yasue, K. Ono, S. Krishnan, S. Hans, F. Satoh, G. Mitchell, S. Kumar. *Automated Validation of COBOL to Java Transformation.* ASE 2024 (tool demo). arXiv:2506.10999.
- S. Hans, A. Kumar, et al. *Automated Testing of COBOL to Java Transformation.* arXiv:2504.10548.
- S. Froimovich, R. Gal, W. Ibraheem, A. Ziv. *Quality Evaluation of COBOL to Java Code Transformation.* arXiv:2507.23356.
- IBM. *General insurance application (GenApp) for IBM CICS TS.* github.com/cicsdev/cics-genapp.
- sandeephans/validation-c2j @ 967d00b: WCA4Z validation inputs and generated Java for LGACDB01.
- GitGalaxy: `docs/wiki/05-18-cobol-java-scan-parity.md`, `docs/wiki/05-19-proven-cobol-to-java-ports.md`, `docs/language_status/oracle_assumptions.md`.
Loading
Loading