# FEEDBACK: Restoring Expressive Power for Cross-Operation Behavioral Contracts

**From**: Arbiter Team (Production user of Apophis v2.0)
**Date**: 2026-04-26
**Related**: arXiv:2602.23922v1 - "Invariant-Driven Automated Testing" (Ribeiro, 2021)

---

## Executive Summary

We have integrated Apophis v2.0 into a production Fastify application (Arbiter — 531 routes, 2,414-line monolithic server, complex OAuth 2.1 + billing + graph infrastructure). After migrating all contracts from APOSTL to Justin and attempting to write "strict" contracts for our routes, we've encountered a fundamental limitation: **Justin enables us to write assertions about a single response, but it cannot express the behavioral relationships between operations that make contract testing valuable.**

This feedback is informed by Ribeiro's thesis on APOSTL/PETIT, which we recently studied. The paper clarifies what we have lost in the v2.0 transition and suggests a path forward that preserves Justin's usability while restoring APOSTL's expressive power.

---

## 1. The Problem: Tautological Contracts

### What We're Writing (Justin v2.0)

After migrating to Justin, our contracts look like this:

```javascript
// GET /health
'x-ensures': [
  'statusCode == 200',
  'response.body.data.status == "ok"'
]

// GET /login  
'x-ensures': [
  'statusCode == 200',
  'response.body.controls.self == "/login"'
]
```

**The problem**: Every one of these assertions is already enforced by JSON Schema. `statusCode == 200` is implied by the `response: { 200: {...} }` block. `response.body.data.status == "ok"` is enforced by `{ const: 'ok' }` in the schema.

We are not testing **behavior**. We are redundantly asserting **structure**.

### What We Want to Write (APOSTL-style)

Ribeiro's thesis (Chapter 4) shows the original vision: contracts express **relationships between operations**:

```apostl
// POST /players (constructor)
// Precondition: player does not exist
response_code(GET /players/{playerNIF}) == 404

// Postcondition: player now exists
response_code(GET /players/{playerNIF}) == 200
response_body(this) == request_body(this)
```

This expresses a **causal behavioral contract**: "Creating a resource causes it to become retrievable." No JSON Schema can express this.

---

## 2. Concrete Examples from Our Codebase

### Example 1: User Lifecycle (user-directory routes)

**Current Justin contracts** (tautological):
```javascript
// POST /tenant/users
'x-ensures': [
  'statusCode != 201 || response.body.data.user_key != null',
  'statusCode != 201 || response.body.data.email != null'
]

// GET /tenant/users/:userKey
'x-ensures': [
  'statusCode != 200 || response.body.data.key != null',
  'statusCode != 200 || response.body.data.email != null'
]
```

**What we need to express** (cross-operation):
```javascript
// POST /tenant/users
'x-ensures': [
  // If creation succeeded, the user must be retrievable
  'statusCode != 201 || check("GET", "/tenant/users/" + response.body.data.user_key).status == 200',
  // The retrieved user must match what we created
  'statusCode != 201 || check("GET", "/tenant/users/" + response.body.data.user_key).body.data.email == request.body.email'
]

// DELETE /tenant/users/:userKey
'x-ensures': [
  // After deletion, the user must NOT be retrievable
  'statusCode != 200 || check("GET", "/tenant/users/" + request.params.userKey).status == 404'
]
```

### Example 2: Application Lifecycle (tenant-applications routes)

**Current Justin**:
```javascript
// POST /tenant/applications
'x-ensures': [
  'statusCode != 201 || response.body.data.application_id != null',
  'statusCode != 201 || response.body.data.name != null'
]
```

**What we need**:
```javascript
// POST /tenant/applications
'x-ensures': [
  // The created app must appear in the collection
  'statusCode != 201 || check("GET", "/tenant/applications").body.data.some(app => app.id == response.body.data.application_id)',
  // The app must be individually retrievable
  'statusCode != 201 || check("GET", "/tenant/applications/" + response.body.data.application_id).status == 200'
]
```

### Example 3: Auth Session (auth-login routes)

**What we need** (not expressible in Justin at all):
```javascript
// POST /auth/:tenantId/:projectId/login
'x-ensures': [
  // After login, the account endpoint must return the authenticated user
  'statusCode != 200 || check("GET", "/account", { headers: { cookie: response.headers["set-cookie"] } }).body.data.userKey != null',
  // The session cookie must be present
  'statusCode != 200 || response.headers["set-cookie"] != null'
]
```

### Example 4: Billing Plans (billing routes)

**What we need**:
```javascript
// POST /billing/plans
'x-ensures': [
  // Creating a plan must increment the plan count
  'statusCode != 201 || previous(check("GET", "/billing/plans").body.total_items) + 1 == check("GET", "/billing/plans").body.total_items'
]
```

---

## 3. What APOSTL Got Right (From the Paper)

Ribeiro's thesis (Section 4.2) states:

> *"APOSTL's main feature is the ability of writing logical conditions based on pure (without side-effects) API operations... APOSTL also provides an API with semantic, i.e., with these annotations one can easily understand each operation's logic."*

The key capabilities we lost:

### 3.1 Cross-Operation References
APOSTL allowed calling `GET` endpoints **inside** pre/postconditions:
```apostl
response_code(GET /players/{playerNIF}) == 404
```
This made it possible to verify state transitions.

### 3.2 Temporal Operator: `previous()`
```apostl
response_body(this) == previous(response_body(GET /players/{playerNIF}))
```
This compared the state before and after an operation.

### 3.3 Quantifiers with Readable Syntax
```apostl
for t in response_body(GET /tournaments) :-
  response_body(GET /tournaments/{t.tournamentId}/enrollments).length <=
  response_body(GET /tournaments/{t.tournamentId}/capacity)
```

### 3.4 Logical Implication
```apostl
response_code(this) == 201 => response_body(this).data.ok == true
```

---

## 4. Why This Matters for Real-World Adoption

### The Empty-Promise Problem

When we demo Apophis to stakeholders, they ask: *"What can contract testing catch that unit tests can't?"*

With Justin-only contracts, the honest answer is: *"Not much, because we're just asserting what JSON Schema already enforces."*

With cross-operation contracts, the answer becomes: *"We can verify that creating a user makes them retrievable, that deleting a plan removes it from listings, that login issues a valid session — all without writing test code."*

### The Incentive Problem

Developers write trivial contracts because:
1. Justin makes it easy to write `statusCode == 200`
2. Justin makes it hard to express anything deeper
3. Schema inference already covers the structural checks

The result: contracts become **checkbox compliance** rather than **behavioral specifications**.

---

## 5. Proposed Solution: Hybrid Approach

We propose a **hybrid contract system** that preserves Justin's familiarity while restoring APOSTL's expressive power:

### 5.1 Core Principle

Keep Justin for inline assertions. Add a **declarative macro system** for cross-operation contracts.

### 5.2 Proposal: `x-behavior` Annotations

Introduce a new annotation for **behavioral contracts** that are compiled to Justin + Apophis runtime calls:

```javascript
// Schema-level invariant (checked after every operation)
'x-invariants': [
  'forall users in GET /tenant/users: user.email matches /^[^\s@]+@[^\s@]+\.[^\s@]+$/',
  'forall apps in GET /tenant/applications: app.tenantId == request.headers["x-tenant-id"]'
]

// Operation-level behavioral contract
app.post('/tenant/users', {
  schema: {
    'x-category': 'constructor',
    'x-ensures': ['statusCode == 201'],
    'x-behavior': [
      // Precondition: email must not exist
      'require: GET /tenant/users?q={request.body.email} returns 0 items',
      // Postcondition: created user must be retrievable
      'ensure: GET /tenant/users/{response.body.data.user_key} returns 200',
      // Postcondition: user must appear in collection
      'ensure: GET /tenant/users contains item with key == response.body.data.user_key'
    ]
  }
})
```

### 5.3 Proposal: Inline `check()` Function

Allow a `check()` helper within Justin expressions:

```javascript
'x-ensures': [
  // Inline cross-operation check
  'statusCode != 201 || check({ method: "GET", url: "/tenant/users/" + response.body.data.user_key }).status == 200',
  
  // Temporal comparison
  'statusCode != 200 || check({ method: "GET", url: "/tenant/applications" }).body.total_items == previous(check({ method: "GET", url: "/tenant/applications" }).body.total_items) + 1'
]
```

### 5.4 Proposal: `previous()` as a Real Operator

Restore `previous(expr)` to evaluate expressions from the **previous stateful test step**:

```javascript
'x-ensures': [
  // After update, the user must differ from before
  'statusCode != 200 || response.body.data.name != previous(response.body.data.name)',
  
  // After delete, the count must decrease
  'statusCode != 200 || check({ method: "GET", url: "/tenant/users" }).body.total_items == previous(check({ method: "GET", url: "/tenant/users" }).body.total_items) - 1'
]
```

---

## 6. Implementation Considerations

### 6.1 Scope Isolation

Cross-operation checks must respect Apophis scopes. If a contract calls `GET /tenant/users` with admin headers, the scope should propagate.

### 6.2 Idempotency & Side Effects

Following APOSTL's design, only `GET` operations should be callable from within contracts. This prevents:
- Test cascades (one contract triggers mutations)
- Non-deterministic failures
- Performance degradation

### 6.3 Stateful Test Integration

Behavioral contracts shine in stateful testing. The `previous()` operator should work across the constructor→mutator→observer sequence:

```javascript
// Stateful test sequence:
// 1. POST /tenant/users (constructor)
//    → captures previous (empty state)
// 2. GET /tenant/users/:key (observer)  
//    → contract: user.name == previous(request.body.name)
// 3. PUT /tenant/users/:key (mutator)
//    → contract: name changed from previous
// 4. DELETE /tenant/users/:key (destructor)
//    → contract: GET returns 404
```

---

## 7. Conclusion

Justin is a pragmatic choice for v2.0. It removed a 915-line parser and made Apophis accessible to JavaScript developers. But in doing so, it also removed the **semantic clarity** and **expressive power** that made contract testing valuable.

Ribeiro's thesis proves that cross-operation contracts are not just nice-to-have — they are the **core value proposition** of specification-driven testing. Without them, Apophis competes with JSON Schema validators. With them, Apophis enables a form of testing that no other tool provides.

We urge the Apophis team to consider a **v2.1 or v3.0** that restores behavioral contract capabilities while keeping Justin's syntax for simple cases. The industry needs contracts that express **"this causes that"** — not just **"this field equals that string."**

---

## References

- Ribeiro, A.C.M. (2021). *Invariant-Driven Automated Testing*. MSc Thesis, NOVA University of Lisbon. arXiv:2602.23922v1 [cs.SE]
- Meyer, B. (1992). *Applying "Design by Contract"*. IEEE Computer, 25(10), 40-51.
- Hoare, C.A.R. (1969). *An Axiomatic Basis for Computer Programming*. Communications of the ACM, 12(10), 576-580.

---

## Appendix: Arbiter Route Inventory with Behavioral Contract Opportunities

| Route Family | Routes | Missing Behavioral Contracts |
|-------------|--------|------------------------------|
| user-directory | 12 | User lifecycle (create→get→update→delete), role changes, stats consistency |
| tenant-applications | 10 | App lifecycle, credential rotation, posture checks |
| auth | 18 | Session lifecycle (login→account→logout), token refresh, magic link redemption |
| billing | 8 | Plan/schedule lifecycle, phase transitions, invoice generation |
| oauth2-provider | 22 | Token lifecycle (issue→introspect→revoke), client registration, consent flows |
| graph | 15 | Node/edge CRUD, graph traversal consistency, query result validity |

**Total**: ~85 routes would benefit from cross-operation behavioral contracts. Currently, 0 can express them.