John Dvorak
2657 lines
82 KiB
Plaintext
2657 lines
82 KiB
Plaintext
# APOPHIS Architecture (Revised)
|
|
|
|
## Overview
|
|
|
|
APOPHIS is a Fastify plugin that extends `@fastify/swagger` with contract-driven testing capabilities inspired by APOSTL (API PrOperty SpecificaTion Language) and PETIT (aPi tEsTIng Tool). It enables developers to write API contracts directly in their Fastify route schemas using OpenAPI custom properties (`x-*`), making the API self-documenting and self-testing.
|
|
|
|
This revision addresses header-sensitive APIs, safe hook ordering, escape hatches, formula safety, scope registries, and symbolic derivation of test properties from contracts.
|
|
|
|
## Core Concepts
|
|
|
|
### Design by Contract for APIs
|
|
|
|
APOPHIS brings Design by Contract principles to REST APIs through OpenAPI extensions:
|
|
|
|
- **Invariants** (`x-invariants`): Properties that must always hold across the entire API
|
|
- **Preconditions** (`x-requires`): Conditions that must hold before an operation executes
|
|
- **Postconditions** (`x-ensures`): Conditions that must hold after an operation executes
|
|
- **Data Generation** (`x-regex`): Regular expressions for generating valid test data
|
|
- **Category Override** (`x-category`): Override PETIT's default HTTP-method-based categorization
|
|
- **Header Access** (`request_headers(this).name`, `response_headers(this).name`): Access request/response headers in APOSTL formulas using property syntax. `request_headers(this).x-foo` checks incoming headers (preconditions), `response_headers(this).x-bar` checks outgoing headers (postconditions)
|
|
|
|
### Operation Categories
|
|
|
|
Following PETIT's methodology, operations are categorized for testing. APOPHIS uses **path-semantic inference** with HTTP method as fallback:
|
|
|
|
**Path-Semantic Rules** (checked in order):
|
|
- **Utility**: Paths containing `/reset`, `/health`, `/ping`, `/login`, `/logout`, `/auth`, `/callback`, `/purge`, `/clear`, `/initialize`, `/setup`, `/webhook`
|
|
- **Observer**: `GET` requests, paths ending with `/search`, `/count`, `/stats`, `/status`
|
|
- **Constructor**: `POST` to paths that look like collections (no path parameter after the resource name: `/players`, `/tournaments`)
|
|
- **Mutator**: `PUT`, `PATCH`, `DELETE`, or `POST` to specific resources (has path parameter: `/players/{id}`, `/tournaments/{id}/enrollments`)
|
|
|
|
**HTTP Method Fallback** (if no path-semantic match):
|
|
- **Constructors** (POST): Create resources
|
|
- **Mutators** (PUT, DELETE): Modify resources
|
|
- **Observers** (GET): Read resources without side effects
|
|
- **Utility** (arbitrary): Escape hatch for operations that don't fit
|
|
|
|
**Override with `x-category`:**
|
|
```yaml
|
|
paths:
|
|
/reset:
|
|
post:
|
|
x-category: utility
|
|
x-requires: [T]
|
|
x-ensures: [T]
|
|
```
|
|
|
|
This ensures `POST /reset` is automatically categorized as `utility` without requiring an explicit override, while `POST /players` correctly becomes a `constructor`.
|
|
|
|
## Architecture Components
|
|
|
|
### 1. Schema Extensions (`lib/schema-extensions.js`)
|
|
|
|
Extends Fastify's JSON Schema with APOSTL annotations:
|
|
|
|
```javascript
|
|
// Example route schema with APOSTL annotations
|
|
fastify.post('/players/:playerNIF', {
|
|
schema: {
|
|
description: 'Create a new player',
|
|
tags: ['players'],
|
|
// Preconditions: what must be true before execution (including headers)
|
|
'x-requires': [
|
|
'response_code(GET /players/{playerNIF}) == 404',
|
|
// Request header MUST be present (upset if missing)
|
|
'request_headers(this).x-tenant-id != null',
|
|
// Request header MUST have specific value
|
|
'request_headers(this).content-type == "application/json"'
|
|
],
|
|
// Postconditions: what must be true after execution (including headers)
|
|
'x-ensures': [
|
|
'response_code(GET /players/{playerNIF}) == 200',
|
|
'response_body(this) == request_body(this)',
|
|
// Response header postcondition
|
|
'response_headers(this).x-ledger-status == "finalized"'
|
|
],
|
|
params: {
|
|
type: 'object',
|
|
properties: {
|
|
playerNIF: {
|
|
type: 'string',
|
|
'x-regex': '(1|2)[0-9]{8}' // Data generation pattern
|
|
}
|
|
}
|
|
},
|
|
body: {
|
|
type: 'object',
|
|
properties: {
|
|
playerNIF: { type: 'string' },
|
|
firstName: { type: 'string' },
|
|
lastName: { type: 'string' },
|
|
email: { type: 'string', format: 'email' }
|
|
}
|
|
},
|
|
response: {
|
|
201: {
|
|
description: 'Player created',
|
|
type: 'object'
|
|
}
|
|
}
|
|
}
|
|
}, handler)
|
|
```
|
|
|
|
### 2. APOSTL Formula Parser (`lib/formula-parser.js`)
|
|
|
|
Parses and evaluates APOSTL formulas written in route schemas:
|
|
|
|
**Extended Grammar (APOSTL + Headers + Arbiter):**
|
|
|
|
```
|
|
formula ::= quantifiedFormula | booleanExpression | conditionalFormula
|
|
quantifiedFormula ::= quantifier string in call :- booleanExpression
|
|
quantifier ::= for | exists
|
|
conditionalFormula ::= if comparison then formula else formula
|
|
booleanExpression ::= booleanExpression booleanOperator booleanExpression | clause
|
|
clause ::= T | F | comparison
|
|
comparison ::= term comparator term
|
|
term ::= operation | operationPrevious | param
|
|
operationPrevious ::= previous(operation)
|
|
operation ::= operationHeader(operationParameter) function?
|
|
operationHeader ::= request_body | response_body | response_code | request_headers | response_headers | query_params | cookies | response_time
|
|
operationParameter ::= httpRequest | this
|
|
httpRequest ::= method url
|
|
comparator ::= == | != | <= | >= | < | > | matches
|
|
booleanOperator ::= && | || | =>
|
|
```
|
|
|
|
**Key Features:**
|
|
- Pure operations only (GET requests for conditions)
|
|
- `previous()` keyword to access state before operation
|
|
- `this` keyword to reference current request/response
|
|
- `request_headers(this).name` to reference incoming request headers
|
|
- `response_headers(this).name` to reference outgoing response headers
|
|
- `response_headers(GET /url).name` to reference headers from a GET request
|
|
- `query_params(this).name` to reference query parameters
|
|
- `query_params(GET /url).name` to reference query params from another request
|
|
- `cookies(this).name` to reference cookies
|
|
- `response_time(this)` to reference response time in milliseconds
|
|
- `response_time(GET /url)` to reference response time of another request
|
|
- `matches` comparator for regex matching
|
|
- Conditional formulas: `if condition then formula else formula`
|
|
- Quantifiers: `for` (universal), `exists` (existential)
|
|
|
|
### 3. Scope Registry (`lib/scope-registry.js`)
|
|
|
|
Manages tenant/application scope for header-sensitive APIs automatically:
|
|
|
|
```javascript
|
|
class ScopeRegistry {
|
|
constructor(options = {}) {
|
|
this.scopes = new Map()
|
|
this.defaultScope = {
|
|
tenantId: options.defaultTenantId || 'default',
|
|
applicationId: options.defaultApplicationId || 'service-a',
|
|
headers: options.defaultHeaders || {}
|
|
}
|
|
|
|
// Auto-discover scopes from environment
|
|
this.discoverFromEnvironment()
|
|
}
|
|
|
|
// Auto-discover scopes from environment variables
|
|
discoverFromEnvironment() {
|
|
// APOPHIS_SCOPE_tenant-a={"tenantId":"tenant-a",...}
|
|
for (const [key, value] of Object.entries(process.env)) {
|
|
if (key.startsWith('APOPHIS_SCOPE_')) {
|
|
const scopeName = key.replace('APOPHIS_SCOPE_', '').toLowerCase()
|
|
try {
|
|
const config = JSON.parse(value)
|
|
this.register(scopeName, config)
|
|
} catch (e) {
|
|
console.warn(`Invalid APOPHIS scope config for ${scopeName}: ${e.message}`)
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
// Derive scope from request headers automatically
|
|
deriveFromRequest(request) {
|
|
const tenantId = request.headers['x-tenant-id']
|
|
const applicationId = request.headers['x-application-id']
|
|
|
|
if (!tenantId) return this.defaultScope
|
|
|
|
const scopeName = `${tenantId}-${applicationId || 'default'}`
|
|
|
|
if (!this.scopes.has(scopeName)) {
|
|
// Auto-register derived scope
|
|
this.register(scopeName, {
|
|
tenantId,
|
|
applicationId: applicationId || 'default',
|
|
headers: Object.fromEntries(
|
|
Object.entries(request.headers)
|
|
.filter(([k]) => k.startsWith('x-'))
|
|
)
|
|
})
|
|
}
|
|
|
|
return this.get(scopeName)
|
|
}
|
|
|
|
register(scopeName, scopeConfig) {
|
|
this.scopes.set(scopeName, {
|
|
tenantId: scopeConfig.tenantId,
|
|
applicationId: scopeConfig.applicationId,
|
|
headers: scopeConfig.headers || {},
|
|
auth: scopeConfig.auth || null
|
|
})
|
|
}
|
|
|
|
get(scopeName) {
|
|
return this.scopes.get(scopeName) || this.defaultScope
|
|
}
|
|
|
|
// Generate headers for a given scope
|
|
getHeaders(scopeName, overrides = {}) {
|
|
const scope = this.get(scopeName)
|
|
return {
|
|
'x-tenant-id': scope.tenantId,
|
|
'x-application-id': scope.applicationId,
|
|
...scope.headers,
|
|
...overrides
|
|
}
|
|
}
|
|
|
|
// Get auth header for scope
|
|
getAuth(scopeName) {
|
|
const scope = this.get(scopeName)
|
|
return scope.auth
|
|
}
|
|
}
|
|
|
|
// Usage in APOPHIS - automatic, no manual registration needed:
|
|
// Scopes auto-derived from requests or environment variables
|
|
// Optional: manually register for test setup
|
|
fastify.apophis.scope.register('tenant-a', {
|
|
tenantId: 'tenant-a',
|
|
applicationId: 'app-1'
|
|
})
|
|
```
|
|
|
|
### 4. Safe Hook Ordering (`lib/contract-validator.js`)
|
|
|
|
Validates API contracts at runtime with safe hook placement:
|
|
|
|
```javascript
|
|
// Validates preconditions before route handler
|
|
async function validatePreconditions(request, reply, routeSchema) {
|
|
const preconditions = routeSchema['x-requires']
|
|
if (!preconditions) return true
|
|
|
|
for (const condition of preconditions) {
|
|
const result = await evaluateFormula(condition, { request })
|
|
if (!result) {
|
|
throw new Error(`Precondition failed: ${condition}`)
|
|
}
|
|
}
|
|
return true
|
|
}
|
|
|
|
// Validates postconditions BEFORE serialization (onResponse, not onSend)
|
|
// Handles both body and header postconditions via unified APOSTL DSL
|
|
async function validatePostconditions(request, reply, routeSchema) {
|
|
const postconditions = routeSchema['x-ensures']
|
|
if (!postconditions) return true
|
|
|
|
for (const condition of postconditions) {
|
|
const result = await evaluateFormula(condition, { request, reply })
|
|
if (!result) {
|
|
throw new Error(`Postcondition failed: ${condition}`)
|
|
}
|
|
}
|
|
return true
|
|
}
|
|
```
|
|
|
|
**Hook Placement:**
|
|
|
|
```javascript
|
|
// SAFE: preHandler for preconditions (before handler)
|
|
// Validates x-requires including request_headers() conditions
|
|
fastify.addHook('preHandler', async (request, reply) => {
|
|
await validatePreconditions(request, reply, request.routeSchema)
|
|
})
|
|
|
|
// SAFE: onResponse for postconditions (after handler, before serialization)
|
|
// Validates x-ensures including response_headers() conditions
|
|
fastify.addHook('onResponse', async (request, reply) => {
|
|
await validatePostconditions(request, reply, request.routeSchema)
|
|
})
|
|
|
|
// UNSAFE: onSend may have already serialized the payload
|
|
// DO NOT USE: fastify.addHook('onSend', ...)
|
|
```
|
|
|
|
### 5. Formula Parameter Substitution (`lib/formula-substitutor.js`)
|
|
|
|
Safe parameter substitution with proper escaping and validation:
|
|
|
|
```javascript
|
|
class FormulaSubstitutor {
|
|
constructor() {
|
|
this.paramPattern = /\{([^}]+)\}/g
|
|
this.validationPattern = /^[a-zA-Z0-9_.-]+$/
|
|
}
|
|
|
|
// Safely substitute parameters in a formula
|
|
substitute(formula, params) {
|
|
if (!formula || typeof formula !== 'string') {
|
|
throw new Error('Formula must be a non-empty string')
|
|
}
|
|
|
|
return formula.replace(this.paramPattern, (match, paramName) => {
|
|
// Validate parameter name (prevent injection)
|
|
if (!this.validationPattern.test(paramName)) {
|
|
throw new Error(`Invalid parameter name: ${paramName}`)
|
|
}
|
|
|
|
// Get parameter value
|
|
const value = this.resolveParam(params, paramName)
|
|
|
|
if (value === undefined || value === null) {
|
|
throw new Error(`Missing parameter: ${paramName}`)
|
|
}
|
|
|
|
// Escape the value for safe insertion
|
|
return this.escapeValue(value)
|
|
})
|
|
}
|
|
|
|
// Resolve nested parameters (e.g., "t.tournamentId")
|
|
resolveParam(params, path) {
|
|
const parts = path.split('.')
|
|
let current = params
|
|
|
|
for (const part of parts) {
|
|
if (current === null || current === undefined) {
|
|
return undefined
|
|
}
|
|
current = current[part]
|
|
}
|
|
|
|
return current
|
|
}
|
|
|
|
// Escape values to prevent formula injection
|
|
escapeValue(value) {
|
|
if (typeof value === 'string') {
|
|
// Escape quotes and backslashes
|
|
return '"' + value.replace(/\\/g, '\\\\').replace(/"/g, '\\"') + '"'
|
|
}
|
|
if (typeof value === 'number' || typeof value === 'boolean') {
|
|
return String(value)
|
|
}
|
|
// For objects/arrays, serialize to JSON
|
|
return JSON.stringify(value)
|
|
}
|
|
|
|
// Validate that all required parameters are present
|
|
validateParams(formula, params) {
|
|
const required = new Set()
|
|
let match
|
|
|
|
while ((match = this.paramPattern.exec(formula)) !== null) {
|
|
required.add(match[1])
|
|
}
|
|
|
|
const missing = []
|
|
for (const param of required) {
|
|
if (this.resolveParam(params, param) === undefined) {
|
|
missing.push(param)
|
|
}
|
|
}
|
|
|
|
if (missing.length > 0) {
|
|
throw new Error(`Missing required parameters: ${missing.join(', ')}`)
|
|
}
|
|
|
|
return true
|
|
}
|
|
}
|
|
```
|
|
|
|
### 6. Cleanup Mechanism (`lib/cleanup-manager.js`)
|
|
|
|
Automatic resource cleanup with deterministic rollback:
|
|
|
|
```javascript
|
|
class CleanupManager {
|
|
constructor(fastify) {
|
|
this.fastify = fastify
|
|
this.createdResources = []
|
|
this.scope = null
|
|
this.autoCleanup = true
|
|
this.registered = false
|
|
}
|
|
|
|
// Set scope for cleanup operations
|
|
setScope(scopeName) {
|
|
this.scope = scopeName
|
|
}
|
|
|
|
// Automatically track resources from constructor responses
|
|
autoTrack(response, routeSchema) {
|
|
if (!this.autoCleanup) return
|
|
|
|
// Only track constructors (POST to collections)
|
|
const category = routeSchema?.['x-category'] || this.inferCategory(routeSchema)
|
|
if (category !== 'constructor') return
|
|
|
|
// Extract resource ID and URL from response
|
|
const resourceId = this.extractResourceId(response)
|
|
const deleteUrl = this.buildDeleteUrl(routeSchema.path, resourceId)
|
|
|
|
if (resourceId && deleteUrl) {
|
|
this.track(routeSchema.path, resourceId, deleteUrl)
|
|
}
|
|
}
|
|
|
|
extractResourceId(response) {
|
|
try {
|
|
const body = typeof response.payload === 'string'
|
|
? JSON.parse(response.payload)
|
|
: response.payload
|
|
|
|
// Common ID fields: id, uuid, tournamentId, playerNIF, etc.
|
|
return body?.id || body?.uuid || body?.tournamentId || body?.playerNIF
|
|
} catch {
|
|
return null
|
|
}
|
|
}
|
|
|
|
buildDeleteUrl(pathTemplate, resourceId) {
|
|
// Convert /players/:playerNIF to /players/123456789
|
|
return pathTemplate.replace(/:\w+/g, resourceId)
|
|
}
|
|
|
|
inferCategory(schema) {
|
|
// Path-semantic inference
|
|
const path = schema?.path || ''
|
|
if (/\/(reset|health|ping|login|logout|auth|callback|purge|clear|initialize|setup|webhook)/.test(path)) return 'utility'
|
|
if (schema?.method === 'GET') return 'observer'
|
|
if (schema?.method === 'POST' && !/\{\w+\}/.test(path)) return 'constructor'
|
|
return 'mutator'
|
|
}
|
|
|
|
// Track a created resource for later cleanup
|
|
track(resourceType, identifier, deleteUrl) {
|
|
this.createdResources.push({
|
|
type: resourceType,
|
|
id: identifier,
|
|
url: deleteUrl,
|
|
timestamp: Date.now()
|
|
})
|
|
}
|
|
|
|
// Cleanup all tracked resources in reverse order
|
|
async cleanup() {
|
|
const headers = this.scope
|
|
? this.fastify.apophis.scope.getHeaders(this.scope)
|
|
: {}
|
|
|
|
const errors = []
|
|
|
|
// Delete in reverse order (LIFO)
|
|
for (let i = this.createdResources.length - 1; i >= 0; i--) {
|
|
const resource = this.createdResources[i]
|
|
try {
|
|
await this.fastify.inject({
|
|
method: 'DELETE',
|
|
url: resource.url,
|
|
headers
|
|
})
|
|
} catch (error) {
|
|
errors.push({ resource, error: error.message })
|
|
}
|
|
}
|
|
|
|
this.createdResources = []
|
|
|
|
if (errors.length > 0) {
|
|
console.warn('Cleanup errors:', errors)
|
|
}
|
|
|
|
return errors
|
|
}
|
|
|
|
// Register cleanup on process exit (called automatically)
|
|
registerExitHandler() {
|
|
if (this.registered) return
|
|
this.registered = true
|
|
|
|
const cleanup = async () => {
|
|
await this.cleanup()
|
|
process.exit(0)
|
|
}
|
|
|
|
process.on('SIGINT', cleanup)
|
|
process.on('SIGTERM', cleanup)
|
|
process.on('exit', cleanup)
|
|
}
|
|
|
|
// Explicit cleanup call for manual control
|
|
async cleanup() {
|
|
return this.cleanup()
|
|
}
|
|
}
|
|
```
|
|
|
|
### 7. Test Data Generator (`lib/test-data-generator.js`)
|
|
|
|
Generates valid test data based on `x-regex` annotations with scope-aware headers:
|
|
|
|
```javascript
|
|
// Generates test data from regex patterns
|
|
function generateFromRegex(pattern) {
|
|
// Uses randexp or similar library
|
|
return randexp.generate(pattern)
|
|
}
|
|
|
|
// Generates complete request objects from schema
|
|
function generateTestData(schema, scope = null) {
|
|
const data = {}
|
|
for (const [key, propSchema] of Object.entries(schema.properties)) {
|
|
if (propSchema['x-regex']) {
|
|
data[key] = generateFromRegex(propSchema['x-regex'])
|
|
} else if (propSchema.type === 'string') {
|
|
data[key] = generateRandomString(propSchema)
|
|
} else if (propSchema.type === 'integer') {
|
|
data[key] = generateRandomInteger(propSchema)
|
|
}
|
|
// ... handle other types
|
|
}
|
|
return data
|
|
}
|
|
|
|
// Generate headers for a request based on scope
|
|
function generateHeaders(schema, scopeName, scopeRegistry) {
|
|
const headers = scopeRegistry.getHeaders(scopeName)
|
|
|
|
// Extract required headers from x-requires formulas
|
|
// Pattern: request_headers(this).header-name
|
|
if (schema['x-requires']) {
|
|
for (const condition of schema['x-requires']) {
|
|
const headerMatches = condition.matchAll(/request_headers\(this\)\.([a-zA-Z0-9_-]+)/g)
|
|
for (const match of headerMatches) {
|
|
const headerName = match[1]
|
|
if (!headers[headerName]) {
|
|
// Generate default value if not in scope
|
|
headers[headerName] = generateDefaultHeader(headerName)
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
return headers
|
|
}
|
|
```
|
|
|
|
### 8. PETIT Test Runner (`lib/petit-runner.js`)
|
|
|
|
Automated testing engine with category override and scope support:
|
|
|
|
```javascript
|
|
class PetitRunner {
|
|
constructor(fastify, options = {}) {
|
|
this.fastify = fastify
|
|
this.strategy = options.strategy || 'CMO'
|
|
this.verbose = options.verbose || false
|
|
this.objectPool = new Map()
|
|
this.scope = options.scope || null
|
|
this.cleanupManager = new CleanupManager(fastify)
|
|
}
|
|
|
|
async run() {
|
|
const apis = this.discoverAPIs()
|
|
const results = []
|
|
|
|
try {
|
|
for (const api of apis) {
|
|
results.push(await this.testAPI(api))
|
|
}
|
|
} finally {
|
|
// Always cleanup, even on failure
|
|
await this.cleanupManager.cleanup()
|
|
}
|
|
|
|
return results
|
|
}
|
|
|
|
categorizeOperations(api) {
|
|
const categories = {
|
|
constructors: [],
|
|
mutators: [],
|
|
observers: [],
|
|
utility: []
|
|
}
|
|
|
|
for (const op of api.operations) {
|
|
// Check for x-category override first
|
|
const override = op.schema?.['x-category']
|
|
if (override) {
|
|
categories[override].push(op)
|
|
continue
|
|
}
|
|
|
|
// Default categorization by HTTP method
|
|
switch (op.method.toUpperCase()) {
|
|
case 'POST':
|
|
categories.constructors.push(op)
|
|
break
|
|
case 'PUT':
|
|
case 'DELETE':
|
|
categories.mutators.push(op)
|
|
break
|
|
case 'GET':
|
|
categories.observers.push(op)
|
|
break
|
|
default:
|
|
categories.utility.push(op)
|
|
}
|
|
}
|
|
|
|
return categories
|
|
}
|
|
|
|
async testOperation(operation) {
|
|
const headers = this.scope
|
|
? this.fastify.apophis.scope.getHeaders(this.scope)
|
|
: {}
|
|
|
|
// 1. Verify invariants
|
|
// 2. Generate or recycle test data
|
|
// 3. Verify preconditions (including header preconditions)
|
|
// 4. Execute request with proper headers
|
|
// 5. Verify postconditions (including header postconditions)
|
|
// 6. Track created resources for cleanup
|
|
// 7. Store results
|
|
}
|
|
}
|
|
```
|
|
|
|
### 9. Plugin Entry Point (`index.js`)
|
|
|
|
Main Fastify plugin registration with scope registry:
|
|
|
|
```javascript
|
|
const fp = require('fastify-plugin')
|
|
|
|
async function apophisPlugin(fastify, options) {
|
|
// Initialize scope registry
|
|
const scopeRegistry = new ScopeRegistry()
|
|
|
|
// Register with @fastify/swagger if not already registered
|
|
if (!fastify.swagger) {
|
|
await fastify.register(require('@fastify/swagger'), {
|
|
...options.swagger,
|
|
transform: apophisTransform
|
|
})
|
|
}
|
|
|
|
// Decorate fastify with APOPHIS utilities
|
|
fastify.decorate('apophis', {
|
|
// Scope registry for header-sensitive APIs (auto-derived + manual override)
|
|
scope: scopeRegistry,
|
|
|
|
// Generate OpenAPI with APOSTL annotations
|
|
spec: () => generateApophisSpec(fastify),
|
|
|
|
// Single test entry point: runs contract + property + stateful tests optimized
|
|
test: async (opts = {}) => {
|
|
const {
|
|
mode = 'all', // 'all' | 'contract' | 'property' | 'stateful'
|
|
depth = 'standard', // 'quick' | 'standard' | 'thorough'
|
|
...runnerOpts
|
|
} = opts
|
|
|
|
const config = {
|
|
quick: { contractRuns: 10, propertyRuns: 50, statefulRuns: 5, maxCommands: 10 },
|
|
standard: { contractRuns: 50, propertyRuns: 100, statefulRuns: 20, maxCommands: 30 },
|
|
thorough: { contractRuns: 200, propertyRuns: 1000, statefulRuns: 100, maxCommands: 50 }
|
|
}[depth]
|
|
|
|
const results = { mode, depth, contract: null, property: null, stateful: null }
|
|
const cleanupManager = new CleanupManager(fastify)
|
|
cleanupManager.setScope(runnerOpts.scope || null)
|
|
|
|
try {
|
|
if (mode === 'all' || mode === 'contract') {
|
|
results.contract = await new PetitRunner(fastify, {
|
|
...runnerOpts,
|
|
...config,
|
|
cleanupManager
|
|
}).run()
|
|
}
|
|
|
|
if (mode === 'all' || mode === 'property') {
|
|
results.property = await new ApophisPropertyTester(fastify, {
|
|
...runnerOpts,
|
|
...config,
|
|
cleanupManager
|
|
}).runPropertyTests()
|
|
}
|
|
|
|
if (mode === 'all' || mode === 'stateful') {
|
|
results.stateful = await new ApophisStatefulRunner(fastify, {
|
|
...runnerOpts,
|
|
...config,
|
|
cleanupManager
|
|
}).run()
|
|
}
|
|
} finally {
|
|
// Always cleanup, even on failure
|
|
await cleanupManager.cleanup()
|
|
}
|
|
|
|
return results
|
|
},
|
|
|
|
// Explicit cleanup for manual resource management
|
|
cleanup: async () => {
|
|
const cleanupManager = new CleanupManager(fastify)
|
|
return cleanupManager.cleanup()
|
|
},
|
|
|
|
// Validate a specific route's contracts
|
|
validate: (routePath) => validateRouteContracts(fastify, routePath),
|
|
|
|
// Generate test data for a route
|
|
generateTestData: (routePath) => generateRouteTestData(fastify, routePath)
|
|
})
|
|
|
|
// Add hooks for runtime contract validation (optional, with per-route opt-out)
|
|
if (options.validateRuntime !== false) {
|
|
// preHandler: validate preconditions before route handler
|
|
fastify.addHook('preHandler', async (request, reply) => {
|
|
// Per-route opt-out via x-validate-runtime: false
|
|
if (request.routeSchema?.['x-validate-runtime'] === false) return
|
|
await validatePreconditions(request, reply, request.routeSchema)
|
|
})
|
|
|
|
// onResponse: validate postconditions after handler, before serialization
|
|
fastify.addHook('onResponse', async (request, reply) => {
|
|
// Per-route opt-out via x-validate-runtime: false
|
|
if (request.routeSchema?.['x-validate-runtime'] === false) return
|
|
await validatePostconditions(request, reply, request.routeSchema)
|
|
})
|
|
}
|
|
}
|
|
|
|
module.exports = fp(apophisPlugin, {
|
|
name: 'apophis-fastify',
|
|
dependencies: ['@fastify/swagger']
|
|
})
|
|
```
|
|
|
|
## Data Flow
|
|
|
|
### 1. Schema Definition Flow
|
|
|
|
```
|
|
Developer writes route schema with x-* annotations
|
|
|
|
|
v
|
|
Fastify validates route schema (ignores x-* properties)
|
|
|
|
|
v
|
|
@fastify/swagger generates OpenAPI spec
|
|
|
|
|
v
|
|
apophisTransform preserves x-* annotations in output
|
|
|
|
|
v
|
|
OpenAPI spec contains self-documenting contracts
|
|
```
|
|
|
|
### 2. Runtime Validation Flow
|
|
|
|
```
|
|
Request arrives
|
|
|
|
|
v
|
|
preHandler hook: validate x-requires preconditions
|
|
|
|
|
v
|
|
Route handler executes
|
|
|
|
|
v
|
|
Handler sets response headers/body
|
|
|
|
|
v
|
|
onResponse hook: validate x-ensures postconditions
|
|
| (before serialization - safe!)
|
|
v
|
|
Serialization (onSend)
|
|
|
|
|
v
|
|
Response sent
|
|
```
|
|
|
|
### 3. Test Execution Flow (PETIT)
|
|
|
|
```
|
|
Developer calls fastify.apophis.test({ scope: 'tenant-a' })
|
|
|
|
|
v
|
|
Discover all routes with x-* annotations
|
|
|
|
|
v
|
|
Categorize: Constructors / Mutators / Observers / Utility
|
|
| (respecting x-category overrides)
|
|
v
|
|
Apply order strategy (e.g., CMO)
|
|
|
|
|
v
|
|
For each operation:
|
|
- Get headers from scope registry
|
|
- Verify API invariants
|
|
- Generate/recycle test data (using x-regex)
|
|
- Verify preconditions (x-requires including request_headers() conditions)
|
|
- Execute HTTP request with scope headers
|
|
- Verify postconditions (x-ensures including response_headers() conditions)
|
|
- Track created resources for cleanup
|
|
|
|
|
v
|
|
Cleanup: Remove all generated test data (reverse order)
|
|
|
|
|
v
|
|
Return test results
|
|
```
|
|
|
|
## OpenAPI Extensions Reference
|
|
|
|
### `x-invariants`
|
|
|
|
API-level invariants that must always hold:
|
|
|
|
```yaml
|
|
paths:
|
|
/tournaments:
|
|
x-invariants:
|
|
- for t in response_body(GET /tournaments) :-
|
|
response_body(GET /tournaments/{t.tournamentId}/enrollments).length <=
|
|
response_body(GET /tournaments/{t.tournamentId}/capacity)
|
|
```
|
|
|
|
### `x-requires`
|
|
|
|
Operation preconditions:
|
|
|
|
```yaml
|
|
paths:
|
|
/players/{playerNIF}:
|
|
delete:
|
|
x-requires:
|
|
- response_code(GET /players/{playerNIF}) == 200
|
|
```
|
|
|
|
### `x-ensures`
|
|
|
|
Operation postconditions:
|
|
|
|
```yaml
|
|
paths:
|
|
/players/{playerNIF}:
|
|
delete:
|
|
x-ensures:
|
|
- response_code(GET /players/{playerNIF}) == 404
|
|
- response_body(this) == previous(response_body(GET /players/{playerNIF}))
|
|
```
|
|
|
|
### Header Access in APOSTL Formulas
|
|
|
|
APOPHIS extends APOSTL with `request_headers` and `response_headers` accessors that use property syntax (via the `function` rule):
|
|
|
|
**Request headers** (available in preconditions and postconditions):
|
|
```yaml
|
|
x-requires:
|
|
# Request MUST have x-tenant-id header (upset if missing)
|
|
- request_headers(this).x-tenant-id != null
|
|
|
|
# Request content-type MUST be application/json
|
|
- request_headers(this).content-type == "application/json"
|
|
|
|
# Request MUST have either authorization OR txn-token
|
|
- request_headers(this).authorization != null || request_headers(this).txn-token != null
|
|
|
|
# Optional header: if present must be valid; if absent, ok
|
|
- request_headers(this).x-explain == null || request_headers(this).x-explain == "true"
|
|
```
|
|
|
|
**Response headers** (only available in postconditions):
|
|
```yaml
|
|
x-ensures:
|
|
# Response MUST include x-ledger-status header
|
|
- response_headers(this).x-ledger-status != null
|
|
|
|
# Response x-ledger-status MUST be "finalized"
|
|
- response_headers(this).x-ledger-status == "finalized"
|
|
|
|
# Response content-type MUST be application/json
|
|
- response_headers(this).content-type == "application/json"
|
|
```
|
|
|
|
**Header invariants** (must hold for ALL operations):
|
|
```yaml
|
|
x-invariants:
|
|
# Every request must have tenant identification
|
|
- request_headers(this).x-tenant-id != null
|
|
|
|
# Every response must include request ID for tracing
|
|
- response_headers(this).x-request-id != null
|
|
```
|
|
|
|
**Headers from other requests** (in quantifiers and comparisons):
|
|
```yaml
|
|
x-requires:
|
|
# Verify a GET request returns specific headers
|
|
- response_headers(GET /players/{playerNIF}).content-type == "application/json"
|
|
```
|
|
|
|
### Arbiter-Specific DSL Extensions
|
|
|
|
APOPHIS extends APOSTL with additional accessors needed for header-sensitive, multi-tenant APIs like Arbiter and Operator:
|
|
|
|
**Query Parameters:**
|
|
```yaml
|
|
x-requires:
|
|
# Pagination parameter must be present
|
|
- query_params(this).page != null
|
|
|
|
# Page size must be within limits
|
|
- query_params(this).limit <= 100
|
|
|
|
# Format override check
|
|
- query_params(this).format == null || query_params(this).format == "json" || query_params(this).format == "html"
|
|
|
|
x-ensures:
|
|
# Response respects requested format
|
|
- if query_params(this).format == "json" then response_headers(this).content-type == "application/json" else T
|
|
```
|
|
|
|
**Cookies:**
|
|
```yaml
|
|
x-requires:
|
|
# Session cookie must exist for authenticated endpoints
|
|
- cookies(this).session_id != null
|
|
|
|
# CSRF token validation
|
|
- cookies(this).csrf_token == request_headers(this).x-csrf-token
|
|
```
|
|
|
|
**Response Time (Performance Contracts):**
|
|
```yaml
|
|
x-ensures:
|
|
# Response must be fast enough
|
|
- response_time(this) < 500
|
|
|
|
# Rate limit check: if too fast, must be rate limited
|
|
- if response_time(GET /health) < 50 then response_headers(this).x-ratelimit-remaining != null else T
|
|
```
|
|
|
|
**Request Body of Other Operations:**
|
|
```yaml
|
|
x-ensures:
|
|
# Verify the POST body we sent matches what the GET returns
|
|
- response_body(GET /players/{playerNIF}) == request_body(POST /players)
|
|
```
|
|
|
|
**Regex Matching:**
|
|
```yaml
|
|
x-requires:
|
|
# Email format validation
|
|
- request_body(this).email matches "^[a-zA-Z0-9._%+-]+@[a-zA-Z0-9.-]+\\.[a-zA-Z]{2,}$"
|
|
|
|
# UUID format check
|
|
- response_body(this).id matches "^[0-9a-f]{8}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12}$"
|
|
```
|
|
|
|
**Conditional Postconditions (Multi-step Flows):**
|
|
```yaml
|
|
x-ensures:
|
|
# Challenge flow: if challenge required, specific response; otherwise success
|
|
- if response_code(this) == 403 then response_body(this).challenge_type != null else response_code(this) == 200
|
|
|
|
# Tenant boundary: regular users get 403, admins bypass
|
|
- if request_headers(this).x-user-role == "admin" then response_code(this) == 200 else response_code(this) != 403
|
|
```
|
|
|
|
**State Transition Verification:**
|
|
```yaml
|
|
x-requires:
|
|
# Before MFA challenge, user must not be MFA-verified
|
|
- response_body(GET /users/{userId}).mfa_verified == false
|
|
|
|
x-ensures:
|
|
# After submitting MFA code, user is verified
|
|
- response_body(GET /users/{userId}).mfa_verified == true
|
|
|
|
# Previous state preserved for rollback check
|
|
- previous(response_body(GET /users/{userId}).mfa_verified) == false
|
|
```
|
|
|
|
### `x-regex`
|
|
|
|
Data generation patterns for properties:
|
|
|
|
```yaml
|
|
paths:
|
|
/players/{playerNIF}:
|
|
get:
|
|
parameters:
|
|
- name: playerNIF
|
|
schema:
|
|
type: string
|
|
x-regex: "(1|2)[0-9]{8}"
|
|
```
|
|
|
|
### `x-category`
|
|
|
|
Override PETIT's default categorization:
|
|
|
|
```yaml
|
|
paths:
|
|
/reset:
|
|
post:
|
|
x-category: utility
|
|
x-requires: [T]
|
|
x-ensures: [T]
|
|
```
|
|
|
|
Valid values: `constructor`, `mutator`, `observer`, `utility`
|
|
|
|
## Arbiter Auto-Testing Coverage
|
|
|
|
### What APOPHIS Can Auto-Test
|
|
|
|
With the extended DSL, APOPHIS can now automatically verify:
|
|
|
|
**1. Header Contract Compliance**
|
|
- Tenant boundary enforcement (`x-tenant-id` mismatch → 403)
|
|
- Token transport rules (ADR-052: txn-token in Authorization rejected)
|
|
- Required headers present (`x-application-id`, `content-type`)
|
|
- Response headers correct (`X-Ledger-Status`, `X-Request-Id`)
|
|
|
|
**2. Authentication Flows**
|
|
- Access token vs transaction token paths
|
|
- Missing auth → 401/403
|
|
- Invalid delegation tokens rejected
|
|
- S2S workload identity headers validated
|
|
|
|
**3. Challenge/Remediation Flows**
|
|
- Step-up authentication sequences
|
|
- MFA challenge → response with challenge options → MFA code → success
|
|
- WebAuthn assertion handling
|
|
- Conditional postconditions based on challenge state
|
|
|
|
**4. Rate Limiting**
|
|
- Response time checks (`response_time(this) < 500`)
|
|
- Rate limit headers present when expected (`X-RateLimit-Remaining`)
|
|
- 429 responses after threshold
|
|
|
|
**5. Tenant Isolation**
|
|
- Cross-tenant access blocked (JWT tenant != header tenant → 403)
|
|
- Admin bypass rules (`masterInternal`/`rootInternal` scopes)
|
|
- Graph store selection per scope
|
|
|
|
**6. Ledger Operations**
|
|
- Billing headers on metered endpoints
|
|
- Finalization status tracking
|
|
- Resource consumption reporting
|
|
|
|
**7. Content Negotiation**
|
|
- Accept header respected (`text/html` → HTML, `application/json` → JSON)
|
|
- Format query parameter overrides (`?format=markdown`)
|
|
- HTMX fragment responses (`HX-Request: true` → `html-fragment`)
|
|
|
|
### What Requires External Testing
|
|
|
|
Some Arbiter behaviors need specialized testing beyond contract DSL:
|
|
|
|
**1. Cryptographic Verification**
|
|
- HTTP Message Signature validation (`signature`, `signature-input`)
|
|
- Workload identity token proof verification
|
|
- Certificate chain validation
|
|
- *Why*: Requires crypto libraries, not expressible in HTTP contracts
|
|
|
|
**2. Database State Verification**
|
|
- Transaction isolation levels
|
|
- Deadlock detection
|
|
- Replication lag
|
|
- *Why*: Requires direct DB access, not API surface
|
|
|
|
**3. Infrastructure Behaviors**
|
|
- Load balancer health checks
|
|
- Graceful shutdown sequences
|
|
- Connection pool exhaustion
|
|
- *Why*: Requires system-level access
|
|
|
|
**4. Browser-Specific Flows**
|
|
- OAuth2 redirect flows (browser cookies, `sec-fetch-mode`)
|
|
- WebAuthn browser integration
|
|
- CORS preflight handling
|
|
- *Why*: Requires real browser or Playwright
|
|
|
|
**5. Eventual Consistency**
|
|
- Async ledger finalization timing
|
|
- Cache invalidation delays
|
|
- Graph store replication lag
|
|
- *Why*: Time-dependent, flaky in contract tests
|
|
|
|
**6. Security Penetration**
|
|
- SQL injection attempts
|
|
- XSS payload handling
|
|
- Path traversal
|
|
- *Why*: Requires adversarial input generation, not contract validation
|
|
|
|
### Recommended Test Pyramid for Arbiter
|
|
|
|
```
|
|
Top: Browser/Integration Tests (Playwright)
|
|
- OAuth flows
|
|
- HTMX interactions
|
|
- Full user journeys
|
|
|
|
Middle: APOPHIS Contract Tests (PETIT + fast-check)
|
|
- Header contracts
|
|
- Auth flows
|
|
- Challenge sequences
|
|
- Rate limiting
|
|
- Tenant isolation
|
|
- Ledger tracking
|
|
|
|
Bottom: Unit Tests + DB Tests
|
|
- Crypto verification
|
|
- DB transactions
|
|
- Business logic
|
|
```
|
|
|
|
## Testing Strategies
|
|
|
|
### Order Strategies
|
|
|
|
Following PETIT's approach:
|
|
|
|
- **COM**: Constructors → Observers → Mutators
|
|
- **CMO**: Constructors → Mutators → Observers
|
|
- **MCO**: Mutators → Constructors → Observers
|
|
- **MOC**: Mutators → Observers → Constructors
|
|
- **OCM**: Observers → Constructors → Mutators
|
|
- **OMC**: Observers → Mutators → Constructors
|
|
- **RND**: Random order
|
|
|
|
### Test Outcomes
|
|
|
|
| Preconditions | Response | Result |
|
|
|--------------|----------|--------|
|
|
| True | 200 OK | OK (if postconditions pass) |
|
|
| True | 4XX | Failed (analyze execution trace) |
|
|
| False | 200 | NOT OK (should have failed) |
|
|
| False | 4XX | Failed (as expected) |
|
|
|
|
## Stateful Testing Mechanics
|
|
|
|
Stateful testing in APOPHIS uses **model-based testing** with fast-check's `fc.modelBased` or command-based testing. The system generates random sequences of API operations, executes them against both a derived state machine model and the real API, and verifies they remain synchronized.
|
|
|
|
### Core Concepts
|
|
|
|
**Model State vs Real State**
|
|
- **Model State**: An in-memory abstraction tracking what "should" exist (derived from schema + invariants)
|
|
- **Real State**: The actual Fastify server state (database, cache, etc.)
|
|
- **Synchronization**: After each command, model predictions are verified against real API responses
|
|
|
|
**Commands**
|
|
Each API operation becomes a `Command` in the state machine:
|
|
|
|
```javascript
|
|
class ApiCommand {
|
|
constructor(operation, params, headers) {
|
|
this.operation = operation // Route schema + metadata
|
|
this.params = params // Generated parameters (path, query, body)
|
|
this.headers = headers // Scope headers + generated headers
|
|
this.category = operation.category // constructor | mutator | observer | utility
|
|
}
|
|
|
|
// Check if this command can run in current model state (preconditions)
|
|
check(modelState) {
|
|
// Evaluate x-requires against model state
|
|
return evaluatePreconditionsOnModel(this.operation['x-requires'], modelState, this.params)
|
|
}
|
|
|
|
// Run the command against the REAL API
|
|
async run(realState) {
|
|
const response = await realState.fastify.inject({
|
|
method: this.operation.method,
|
|
url: substituteParams(this.operation.path, this.params),
|
|
payload: this.params.body,
|
|
query: this.params.query,
|
|
headers: this.headers
|
|
})
|
|
return response
|
|
}
|
|
|
|
// Update the MODEL state based on command execution
|
|
runModel(modelState) {
|
|
// Apply state transition based on operation category and x-ensures
|
|
return applyModelTransition(modelState, this.operation, this.params, this.category)
|
|
}
|
|
|
|
// Fast-check shrinking: how to simplify this command
|
|
shrink() {
|
|
// Shrink parameters while maintaining schema validity
|
|
return shrinkParams(this.operation.schema, this.params)
|
|
}
|
|
}
|
|
```
|
|
|
|
### State Machine Definition
|
|
|
|
The state machine is derived from the API schema and invariants:
|
|
|
|
```javascript
|
|
class ApophisStateMachine {
|
|
constructor(fastify, options = {}) {
|
|
this.fastify = fastify
|
|
this.scope = options.scope || null
|
|
this.model = this.buildInitialModel()
|
|
this.commands = this.discoverCommands()
|
|
this.invariants = this.extractInvariants()
|
|
}
|
|
|
|
// Initial model state derived from schema structure
|
|
buildInitialModel() {
|
|
const model = new Map()
|
|
|
|
// Discover all resource collections from schemas
|
|
for (const [path, route] of Object.entries(this.fastify.getSchemas())) {
|
|
if (route.response?.[201] || route.response?.[200]) {
|
|
const resourceName = this.extractResourceName(path)
|
|
model.set(resourceName, {
|
|
items: new Map(),
|
|
relationships: new Map(),
|
|
counters: new Map()
|
|
})
|
|
}
|
|
}
|
|
|
|
return model
|
|
}
|
|
|
|
// Discover all possible commands from registered routes
|
|
discoverCommands() {
|
|
const commands = []
|
|
|
|
for (const route of this.fastify.routes) {
|
|
const category = route.schema?.['x-category'] || this.inferCategory(route.method)
|
|
const schema = route.schema || {}
|
|
|
|
// Build parameter arbitrary from schema
|
|
const paramsArb = this.buildParamsArbitrary(route)
|
|
|
|
commands.push({
|
|
name: `${route.method} ${route.path}`,
|
|
category,
|
|
path: route.path,
|
|
method: route.method,
|
|
schema,
|
|
paramsArb,
|
|
// Weight for random selection (observers more frequent than mutators)
|
|
weight: category === 'observer' ? 5 : category === 'constructor' ? 2 : 3
|
|
})
|
|
}
|
|
|
|
return commands
|
|
}
|
|
|
|
// Extract invariants from x-invariants declarations
|
|
extractInvariants() {
|
|
const invariants = []
|
|
|
|
for (const route of this.fastify.routes) {
|
|
if (route.schema?.['x-invariants']) {
|
|
invariants.push(...route.schema['x-invariants'])
|
|
}
|
|
}
|
|
|
|
// Also derive invariants from schema constraints
|
|
invariants.push(...this.deriveSchemaInvariants())
|
|
|
|
return invariants
|
|
}
|
|
}
|
|
```
|
|
|
|
### Command Generation Strategy
|
|
|
|
fast-check generates command sequences by:
|
|
|
|
1. **Filtering valid commands**: Only commands whose `check()` passes in current model state
|
|
2. **Category-aware generation**: Ensure resource exists before mutating it
|
|
3. **Biased selection**: Favor observers (safer) over constructors/mutators
|
|
|
|
```javascript
|
|
function generateCommandSequence(stateMachine, maxCommands = 50) {
|
|
return fc.array(
|
|
fc.constantFrom(...stateMachine.commands)
|
|
.chain(command => {
|
|
// Generate valid parameters for this command
|
|
return command.paramsArb.map(params => ({
|
|
...command,
|
|
params,
|
|
headers: stateMachine.scope
|
|
? stateMachine.fastify.apophis.scope.getHeaders(stateMachine.scope)
|
|
: {}
|
|
}))
|
|
})
|
|
.filter(command => {
|
|
// Only include commands that can run in current state
|
|
return command.check(stateMachine.model)
|
|
}),
|
|
{ minLength: 1, maxLength: maxCommands }
|
|
)
|
|
}
|
|
```
|
|
|
|
### Model-Real Synchronization Verification
|
|
|
|
After each command executes, verify the model prediction matches reality:
|
|
|
|
```javascript
|
|
async function verifySynchronization(modelState, realResponse, command) {
|
|
const discrepancies = []
|
|
|
|
// 1. Response code matches prediction
|
|
const predictedCode = predictResponseCode(modelState, command)
|
|
if (predictedCode !== realResponse.statusCode) {
|
|
discrepancies.push({
|
|
type: 'status_code_mismatch',
|
|
predicted: predictedCode,
|
|
actual: realResponse.statusCode
|
|
})
|
|
}
|
|
|
|
// 2. Response body structure matches schema
|
|
if (realResponse.statusCode < 400) {
|
|
const schema = command.schema.response?.[realResponse.statusCode]
|
|
if (schema) {
|
|
const validation = validateAgainstSchema(realResponse.json(), schema)
|
|
if (!validation.valid) {
|
|
discrepancies.push({
|
|
type: 'schema_violation',
|
|
errors: validation.errors
|
|
})
|
|
}
|
|
}
|
|
}
|
|
|
|
// 3. Invariants still hold in real state
|
|
for (const invariant of stateMachine.invariants) {
|
|
const holds = await evaluateInvariantOnReal(invariant, realResponse, command)
|
|
if (!holds) {
|
|
discrepancies.push({
|
|
type: 'invariant_violation',
|
|
invariant
|
|
})
|
|
}
|
|
}
|
|
|
|
// 4. Model-derived postconditions
|
|
if (command.schema?.['x-ensures']) {
|
|
for (const postcondition of command.schema['x-ensures']) {
|
|
const holds = await evaluatePostcondition(postcondition, realResponse, command)
|
|
if (!holds) {
|
|
discrepancies.push({
|
|
type: 'postcondition_failed',
|
|
condition: postcondition
|
|
})
|
|
}
|
|
}
|
|
}
|
|
|
|
return discrepancies
|
|
}
|
|
```
|
|
|
|
### Complete Stateful Test Runner
|
|
|
|
```javascript
|
|
class ApophisStatefulRunner {
|
|
constructor(fastify) {
|
|
this.fastify = fastify
|
|
this.cleanupManager = new CleanupManager(fastify)
|
|
}
|
|
|
|
async run(options = {}) {
|
|
const {
|
|
numRuns = 100,
|
|
maxCommands = 50,
|
|
scope = null,
|
|
seed = undefined // For deterministic replay
|
|
} = options
|
|
|
|
const stateMachine = new ApophisStateMachine(this.fastify, { scope })
|
|
|
|
return fc.assert(
|
|
fc.property(
|
|
generateCommandSequence(stateMachine, maxCommands),
|
|
async (commands) => {
|
|
// Setup: Start with empty state or seed state
|
|
await this.setupInitialState(stateMachine)
|
|
|
|
try {
|
|
for (const command of commands) {
|
|
// 1. Check preconditions on model
|
|
if (!command.check(stateMachine.model)) {
|
|
// Skip command if preconditions don't hold
|
|
continue
|
|
}
|
|
|
|
// 2. Execute on REAL API
|
|
const realResponse = await command.run({
|
|
fastify: this.fastify,
|
|
cleanupManager: this.cleanupManager
|
|
})
|
|
|
|
// 3. Execute on MODEL
|
|
const newModelState = command.runModel(stateMachine.model)
|
|
|
|
// 4. Verify synchronization
|
|
const discrepancies = await verifySynchronization(
|
|
newModelState, realResponse, command
|
|
)
|
|
|
|
if (discrepancies.length > 0) {
|
|
throw new StatefulTestError({
|
|
command: command.name,
|
|
params: command.params,
|
|
discrepancies,
|
|
commandHistory: commands.slice(0, commands.indexOf(command) + 1)
|
|
})
|
|
}
|
|
|
|
// 5. Update model state
|
|
stateMachine.model = newModelState
|
|
|
|
// 6. Track resources for cleanup
|
|
if (command.category === 'constructor') {
|
|
this.trackResourceForCleanup(command, realResponse)
|
|
}
|
|
}
|
|
} finally {
|
|
// Always cleanup
|
|
await this.cleanupManager.cleanup()
|
|
}
|
|
|
|
return true
|
|
}
|
|
),
|
|
{ numRuns, seed }
|
|
)
|
|
}
|
|
|
|
setupInitialState(stateMachine) {
|
|
// Reset model to initial state
|
|
stateMachine.model = stateMachine.buildInitialModel()
|
|
|
|
// Optionally seed with existing data
|
|
// (e.g., if testing against non-empty database)
|
|
}
|
|
|
|
trackResourceForCleanup(command, response) {
|
|
// Extract resource ID from response for later deletion
|
|
const resourceId = response.json()?.id || response.json()?.tournamentId
|
|
if (resourceId) {
|
|
this.cleanupManager.track(
|
|
command.operation.path,
|
|
resourceId,
|
|
command.operation.path.replace(/{.*?}/g, resourceId)
|
|
)
|
|
}
|
|
}
|
|
}
|
|
```
|
|
|
|
### Handling Stateful Test Failures
|
|
|
|
When a stateful test fails, APOPHIS provides detailed diagnostics:
|
|
|
|
```javascript
|
|
class StatefulTestError extends Error {
|
|
constructor({ command, params, discrepancies, commandHistory }) {
|
|
super(`Stateful test failed at command: ${command}`)
|
|
this.command = command
|
|
this.params = params
|
|
this.discrepancies = discrepancies
|
|
this.commandHistory = commandHistory
|
|
}
|
|
|
|
toString() {
|
|
let msg = `Stateful Test Failure\n`
|
|
msg += `===================\n\n`
|
|
msg += `Failed at command: ${this.command}\n`
|
|
msg += `Parameters: ${JSON.stringify(this.params, null, 2)}\n\n`
|
|
msg += `Command sequence (${this.commandHistory.length} commands):\n`
|
|
this.commandHistory.forEach((cmd, i) => {
|
|
msg += ` ${i + 1}. ${cmd.name} ${JSON.stringify(cmd.params)}\n`
|
|
})
|
|
msg += `\nDiscrepancies:\n`
|
|
this.discrepancies.forEach(d => {
|
|
msg += ` - [${d.type}]: ${JSON.stringify(d)}\n`
|
|
})
|
|
return msg
|
|
}
|
|
}
|
|
```
|
|
|
|
### Deterministic Replay
|
|
|
|
Failed stateful tests can be replayed exactly:
|
|
|
|
```javascript
|
|
// On failure, fast-check provides the seed and path
|
|
const failedRun = {
|
|
seed: 12345,
|
|
path: "0:1:2:3:4", // Which branches were taken
|
|
counterexample: [/* commands that failed */]
|
|
}
|
|
|
|
// Replay the exact same test
|
|
await runner.run({
|
|
seed: failedRun.seed,
|
|
// fast-check handles path replay internally
|
|
})
|
|
```
|
|
|
|
### Example: Tournament Stateful Test
|
|
|
|
```javascript
|
|
// Derived from the Tournament API schema
|
|
const tournamentStatefulTest = async (fastify) => {
|
|
const runner = new ApophisStatefulRunner(fastify)
|
|
|
|
return runner.run({
|
|
numRuns: 100,
|
|
maxCommands: 30,
|
|
scope: 'tenant-a'
|
|
})
|
|
}
|
|
|
|
// A failing test might produce:
|
|
// Stateful Test Failure
|
|
// ===================
|
|
// Failed at command: POST /tournaments/{tournamentId}/enrollments
|
|
// Parameters: { tournamentId: "550e8400-e29b-41d4-a716-446655440000", playerNIF: "123456789" }
|
|
//
|
|
// Command sequence (5 commands):
|
|
// 1. POST /tournaments { name: "Spring Cup", capacity: 2 }
|
|
// 2. POST /players { playerNIF: "123456789", ... }
|
|
// 3. POST /players { playerNIF: "987654321", ... }
|
|
// 4. POST /tournaments/{id}/enrollments { tournamentId: "550e...", playerNIF: "123456789" }
|
|
// 5. POST /tournaments/{id}/enrollments { tournamentId: "550e...", playerNIF: "987654321" }
|
|
// 6. POST /tournaments/{id}/enrollments { tournamentId: "550e...", playerNIF: "111111111" } <-- FAILED
|
|
//
|
|
// Discrepancies:
|
|
// - [postcondition_failed]: enrollments.length <= capacity
|
|
// Actual: 3 enrollments, capacity: 2
|
|
```
|
|
|
|
### Invariant Checking Across Command Sequences
|
|
|
|
Invariants are verified after EVERY command, not just at the end:
|
|
|
|
```javascript
|
|
async function verifyInvariants(stateMachine, modelState, realResponse) {
|
|
for (const invariant of stateMachine.invariants) {
|
|
// Check invariant on model state
|
|
const modelHolds = evaluateInvariantOnModel(invariant, modelState)
|
|
|
|
// Check invariant on real state via API calls
|
|
const realHolds = await evaluateInvariantOnReal(invariant, realResponse, stateMachine.fastify)
|
|
|
|
if (modelHolds !== realHolds) {
|
|
return {
|
|
type: 'invariant_divergence',
|
|
invariant,
|
|
modelHolds,
|
|
realHolds
|
|
}
|
|
}
|
|
|
|
if (!modelHolds || !realHolds) {
|
|
return {
|
|
type: 'invariant_violation',
|
|
invariant,
|
|
violatedIn: !modelHolds ? 'model' : 'real'
|
|
}
|
|
}
|
|
}
|
|
|
|
return null
|
|
}
|
|
```
|
|
|
|
### Integration with Schema-Driven Derivation
|
|
|
|
Stateful testing combines all previous layers:
|
|
|
|
1. **Schema-derived model structure** determines model state shape
|
|
2. **Schema-derived arbitraries** generate valid command parameters
|
|
3. **Derived preconditions** (`check()`) ensure commands are valid in current state
|
|
4. **Derived postconditions** verify real API behavior
|
|
5. **x-invariants** are checked after every command
|
|
6. **x-category** determines valid command transitions
|
|
|
|
This guarantees that stateful tests explore meaningful state spaces with valid data, catching bugs like:
|
|
- Race conditions in resource creation/deletion
|
|
- State machine violations (e.g., enrolling in full tournament)
|
|
- Missing cleanup or resource leaks
|
|
- Invariant violations across multi-step operations
|
|
|
|
## Symbolic Analysis: Deriving Properties from Contracts
|
|
|
|
Instead of requiring developers to write redundant `x-properties` and `x-stateful-test` annotations, APOPHIS derives property-based tests and stateful models directly from `x-requires`, `x-ensures`, and `x-invariants` using symbolic analysis.
|
|
|
|
### Three-Point Pipeline
|
|
|
|
```
|
|
Parser -> Validator -> Extractor
|
|
```
|
|
|
|
**1. Parser**: Parse APOSTL formulas into AST
|
|
**2. Validator**: Validate formula well-formedness and type consistency
|
|
**3. Extractor**: Extract fast-check properties and stateful models
|
|
|
|
### Example Derivation
|
|
|
|
Given:
|
|
```yaml
|
|
x-invariants:
|
|
- for t in response_body(GET /tournaments) :-
|
|
response_body(GET /tournaments/{t.tournamentId}/enrollments).length <=
|
|
response_body(GET /tournaments/{t.tournamentId}/capacity)
|
|
```
|
|
|
|
**Derived fast-check property:**
|
|
```javascript
|
|
fc.property(
|
|
fc.array(fc.record({
|
|
tournamentId: fc.integer(),
|
|
capacity: fc.integer({ min: 0 })
|
|
})),
|
|
fc.array(fc.record({
|
|
tournamentId: fc.integer(),
|
|
playerNIF: fc.stringMatching(/(1|2)[0-9]{8}/)
|
|
})),
|
|
(tournaments, enrollments) => {
|
|
// Group enrollments by tournament
|
|
const enrollmentCounts = {}
|
|
for (const e of enrollments) {
|
|
enrollmentCounts[e.tournamentId] = (enrollmentCounts[e.tournamentId] || 0) + 1
|
|
}
|
|
|
|
// Check invariant
|
|
for (const t of tournaments) {
|
|
const count = enrollmentCounts[t.tournamentId] || 0
|
|
if (count > t.capacity) return false
|
|
}
|
|
return true
|
|
}
|
|
)
|
|
```
|
|
|
|
**Derived stateful model:**
|
|
```javascript
|
|
class TournamentModel {
|
|
constructor() {
|
|
this.tournaments = new Map()
|
|
this.enrollments = new Map()
|
|
}
|
|
|
|
createTournament(id, capacity) {
|
|
this.tournaments.set(id, { id, capacity, enrollments: 0 })
|
|
}
|
|
|
|
enrollPlayer(tournamentId, playerNIF) {
|
|
const tournament = this.tournaments.get(tournamentId)
|
|
if (!tournament) return { success: false }
|
|
if (tournament.enrollments >= tournament.capacity) {
|
|
return { success: false }
|
|
}
|
|
tournament.enrollments++
|
|
return { success: true }
|
|
}
|
|
|
|
checkInvariant() {
|
|
for (const [id, tournament] of this.tournaments) {
|
|
if (tournament.enrollments > tournament.capacity) {
|
|
return false
|
|
}
|
|
}
|
|
return true
|
|
}
|
|
}
|
|
```
|
|
|
|
### QuickLogic Integration
|
|
|
|
APOPHIS can leverage QuickLogic3 from `~/Business/workspace/Operator/libs/QuickLogic` for advanced symbolic analysis:
|
|
|
|
```javascript
|
|
// lib/symbolic-analyzer.js
|
|
const { ESSContextQueryEngine } = require('~/Business/workspace/Operator/libs/QuickLogic/core/ContextRuntime')
|
|
const { NodeFactory } = require('~/Business/workspace/Operator/libs/QuickLogic/src/ast')
|
|
|
|
class ApophisSymbolicAnalyzer {
|
|
constructor() {
|
|
this.engine = new ESSContextQueryEngine()
|
|
this.parser = new APOSTLParser()
|
|
}
|
|
|
|
// Parse APOSTL formula into QuickLogic AST
|
|
parseToAST(formula) {
|
|
const apophisAST = this.parser.parse(formula)
|
|
return this.convertToQuickLogic(apophisAST)
|
|
}
|
|
|
|
// Convert APOSTL AST to QuickLogic PredicateApplication
|
|
convertToQuickLogic(ast) {
|
|
switch (ast.type) {
|
|
case 'comparison':
|
|
return NodeFactory.PredicateApplication({
|
|
predicate: 'equals',
|
|
args: [
|
|
this.convertToQuickLogic(ast.left),
|
|
this.convertToQuickLogic(ast.right)
|
|
]
|
|
})
|
|
case 'quantified':
|
|
return NodeFactory.ForAll({
|
|
variable: ast.variable,
|
|
body: this.convertToQuickLogic(ast.expression)
|
|
})
|
|
case 'operation':
|
|
return NodeFactory.PredicateApplication({
|
|
predicate: ast.header,
|
|
args: [ast.parameter]
|
|
})
|
|
default:
|
|
return ast
|
|
}
|
|
}
|
|
|
|
// Extract properties from contracts using QuickLogic inference
|
|
extractProperties(contracts) {
|
|
const properties = []
|
|
|
|
for (const contract of contracts) {
|
|
const ast = this.parseToAST(contract)
|
|
|
|
// Use QuickLogic to analyze the formula
|
|
const result = this.engine.query(ast)
|
|
|
|
if (result.truthValue === 'TRUE') {
|
|
// Extract property from proven contract
|
|
properties.push(this.generateProperty(ast))
|
|
} else if (result.truthValue === 'UNKNOWN') {
|
|
// Generate questions for unresolved parts
|
|
const questions = result.remainingQuestions
|
|
properties.push(...this.generatePropertiesFromQuestions(questions))
|
|
}
|
|
}
|
|
|
|
return properties
|
|
}
|
|
|
|
// Generate fast-check property from AST
|
|
generateProperty(ast) {
|
|
// Analyze AST structure to determine property type
|
|
if (this.isInvariant(ast)) {
|
|
return this.generateInvariantProperty(ast)
|
|
}
|
|
if (this.isPrecondition(ast)) {
|
|
return this.generatePreconditionProperty(ast)
|
|
}
|
|
if (this.isPostcondition(ast)) {
|
|
return this.generatePostconditionProperty(ast)
|
|
}
|
|
return null
|
|
}
|
|
|
|
// Generate stateful model from invariants
|
|
generateStatefulModel(invariants) {
|
|
const model = new Map()
|
|
|
|
for (const invariant of invariants) {
|
|
const ast = this.parseToAST(invariant)
|
|
|
|
// Extract collection and constraint
|
|
const collection = this.extractCollection(ast)
|
|
const constraint = this.extractConstraint(ast)
|
|
|
|
// Add to model
|
|
model.set(collection.name, {
|
|
type: 'collection',
|
|
constraint: constraint,
|
|
operations: this.deriveOperations(collection, constraint)
|
|
})
|
|
}
|
|
|
|
return model
|
|
}
|
|
}
|
|
```
|
|
|
|
## Implementation Phases
|
|
|
|
### Phase 1: Core Schema Extensions
|
|
- Implement `x-requires`, `x-ensures`, `x-invariants`, `x-regex`, `x-category` support
|
|
- Integrate with `@fastify/swagger` transform to preserve annotations
|
|
- Basic formula parser for simple comparisons
|
|
- Safe hook ordering (preHandler + onResponse, NOT onSend)
|
|
- Per-route opt-out via `x-validate-runtime: false`
|
|
|
|
### Phase 2: Header-Sensitive API Support
|
|
- Extend APOSTL grammar with `request_headers` and `response_headers` accessors
|
|
- Scope registry with auto-discovery from environment (`APOPHIS_SCOPE_*`)
|
|
- Automatic scope derivation from incoming request headers
|
|
- Header generation from `request_headers(this).x-foo` formulas
|
|
- Support for Arbiter/Operator header patterns
|
|
|
|
### Phase 3: Formula Safety
|
|
- Safe parameter substitution with validation and escaping
|
|
- Formula injection prevention
|
|
- Parameter completeness checking
|
|
|
|
### Phase 4: Cleanup Mechanism
|
|
- Automatic resource tracking from constructor responses
|
|
- Path-semantic inference for resource URL construction
|
|
- LIFO cleanup with scope-aware deletion
|
|
- Automatic cleanup on test completion / process exit
|
|
- Explicit `cleanup()` API for manual control
|
|
|
|
### Phase 5: PETIT Test Runner
|
|
- Path-semantic operation categorization (automatic utility detection)
|
|
- HTTP method fallback categorization
|
|
- `x-category` override support
|
|
- Strategy-based ordering
|
|
- Scope-aware test execution
|
|
- Single `test()` entry point with mode selection
|
|
|
|
### Phase 6: Symbolic Analysis
|
|
- Parser-Validator-Extractor three-point pipeline
|
|
- Derive fast-check properties from contracts
|
|
- Derive stateful models from invariants
|
|
- QuickLogic3 integration for advanced inference
|
|
|
|
### Phase 7: fast-check Integration
|
|
- Schema-to-arbitrary conversion
|
|
- Automatic edge case discovery
|
|
- Shrinking support for minimal counterexamples
|
|
- Named arbitraries for better error messages
|
|
|
|
### Phase 8: Stateful Testing
|
|
- Model-based stateful testing with derived models
|
|
- Command registration and discovery from schemas
|
|
- Invariant checking across command sequences
|
|
- Model-API synchronization verification
|
|
- Deterministic replay with seed support
|
|
|
|
### Phase 9: DX Polish
|
|
- Single `test()` with `mode` and `depth` options
|
|
- Automatic cleanup integration
|
|
- Per-route opt-out support
|
|
- Environment-based scope configuration
|
|
- Path-semantic category inference
|
|
- Better error messages with derived context
|
|
|
|
## File Structure
|
|
|
|
```
|
|
apophis-fastify/
|
|
├── lib/
|
|
│ ├── formula-parser.js # APOSTL formula parsing and evaluation
|
|
│ ├── formula-substitutor.js # Safe parameter substitution
|
|
│ ├── schema-extensions.js # Schema validation and extension handling
|
|
│ ├── openapi-transform.js # Transform for @fastify/swagger integration
|
|
│ ├── contract-validator.js # Runtime contract validation (safe hooks)
|
|
│ ├── test-data-generator.js # Test data generation from x-regex
|
|
│ ├── petit-runner.js # PETIT automated test runner
|
|
│ ├── cleanup-manager.js # Resource cleanup and rollback
|
|
│ ├── scope-registry.js # Tenant/application scope management
|
|
│ ├── symbolic-analyzer.js # Derive properties from contracts
|
|
│ ├── fast-check-integration.js # Property-based testing with fast-check
|
|
│ ├── stateful-test-runner.js # Model-based stateful testing
|
|
│ └── utils.js # Shared utilities
|
|
├── models/ # Built-in stateful testing models
|
|
│ └── tournament-model.js # Example: Tournament domain model
|
|
├── index.js # Main plugin entry point
|
|
├── package.json
|
|
└── README.md
|
|
```
|
|
|
|
## Dependencies
|
|
|
|
- `@fastify/swagger`: Core swagger integration
|
|
- `fastify-plugin`: Plugin wrapper for Fastify
|
|
- `randexp`: Regex-based string generation (optional)
|
|
- `fast-check`: Property-based testing framework (optional)
|
|
- `ajv`: JSON Schema validation (peer dependency via Fastify)
|
|
- `quicklogic3`: Symbolic analysis engine (optional, from Operator/libs/QuickLogic)
|
|
|
|
## Usage Example
|
|
|
|
```javascript
|
|
const fastify = require('fastify')()
|
|
|
|
// Register APOPHIS (registers @fastify/swagger automatically)
|
|
await fastify.register(require('apophis-fastify'), {
|
|
swagger: {
|
|
openapi: '3.0.0',
|
|
info: { title: 'Tournaments API', version: '1.0.0' }
|
|
},
|
|
validateRuntime: true // Enable runtime contract validation globally
|
|
})
|
|
|
|
// Scopes auto-derived from requests, but can be pre-registered for testing
|
|
fastify.apophis.scope.register('tenant-a', {
|
|
tenantId: 'tenant-a',
|
|
applicationId: 'app-1'
|
|
})
|
|
|
|
// Define routes with contracts
|
|
fastify.post('/players/:playerNIF', {
|
|
schema: {
|
|
'x-requires': [
|
|
'response_code(GET /players/{playerNIF}) == 404',
|
|
// Request header MUST be present (upset if missing)
|
|
'request_headers(this).x-tenant-id != null',
|
|
// Request header MUST have specific value
|
|
'request_headers(this).content-type == "application/json"'
|
|
],
|
|
'x-ensures': [
|
|
'response_code(GET /players/{playerNIF}) == 200',
|
|
'response_body(this) == request_body(this)',
|
|
// Response header postcondition
|
|
'response_headers(this).x-ledger-status == "finalized"'
|
|
],
|
|
params: {
|
|
type: 'object',
|
|
properties: {
|
|
playerNIF: {
|
|
type: 'string',
|
|
'x-regex': '(1|2)[0-9]{8}'
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}, async (request, reply) => {
|
|
// Handler implementation
|
|
})
|
|
|
|
// POST /reset auto-categorized as utility (path-semantic inference)
|
|
// No x-category override needed!
|
|
fastify.post('/reset', {
|
|
schema: {
|
|
'x-requires': [T],
|
|
'x-ensures': [T]
|
|
}
|
|
}, async (request, reply) => {
|
|
// Reset implementation
|
|
})
|
|
|
|
// Opt-out of runtime validation for specific routes
|
|
fastify.get('/health', {
|
|
schema: {
|
|
'x-validate-runtime': false, // Skip contract validation
|
|
response: {
|
|
200: {
|
|
type: 'object',
|
|
properties: {
|
|
status: { type: 'string' }
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}, async (request, reply) => {
|
|
return { status: 'ok' }
|
|
})
|
|
|
|
// Generate OpenAPI spec with contracts
|
|
const spec = fastify.apophis.spec()
|
|
console.log(JSON.stringify(spec, null, 2))
|
|
|
|
// Single test entry point: runs contract + property + stateful tests
|
|
const results = await fastify.apophis.test({
|
|
mode: 'all', // 'all' | 'contract' | 'property' | 'stateful'
|
|
depth: 'standard', // 'quick' | 'standard' | 'thorough'
|
|
scope: 'tenant-a',
|
|
verbose: true
|
|
})
|
|
|
|
// Results structure:
|
|
// {
|
|
// mode: 'all',
|
|
// depth: 'standard',
|
|
// contract: { passed: 45, failed: 2, ... },
|
|
// property: { passed: 100, failed: 0, ... },
|
|
// stateful: { passed: 20, failed: 1, sequences: [...] }
|
|
// }
|
|
|
|
// Automatic cleanup runs after tests complete (or on failure)
|
|
// Explicit cleanup if needed:
|
|
await fastify.apophis.cleanup()
|
|
|
|
await fastify.listen({ port: 3000 })
|
|
```
|
|
|
|
## Schema-Driven Derivation
|
|
|
|
APOPHIS extracts maximal testing value from standard JSON Schema and OpenAPI constructs. The `x-*` annotations provide semantic intent, but the schema itself defines the shape, constraints, and relationships of data. By driving fast-check arbitrary generation, implicit precondition/postcondition derivation, and stateful model structure directly from standard schema properties, we guarantee that generated tests are type-safe, boundary-aware, and semantically valid even when no explicit contracts are written.
|
|
|
|
### Schema-to-Arbitrary Mapping
|
|
|
|
Every JSON Schema property maps directly to a `fast-check` arbitrary. This ensures generated test data respects the API's own validation rules.
|
|
|
|
| JSON Schema Property | fast-check Arbitrary | Notes |
|
|
|---|---|---|
|
|
| `type: string` | `fc.string()` | Base arbitrary for strings |
|
|
| `minLength: n` | `.filter(s => s.length >= n)` | Applied after generation |
|
|
| `maxLength: n` | `fc.string({ maxLength: n })` | Direct fast-check support |
|
|
| `pattern: "regex"` | `fc.stringMatching(/regex/)` | Standard JSON Schema pattern (not just `x-regex`) |
|
|
| `format: email` | `fc.emailAddress()` | Semantic format → semantic arbitrary |
|
|
| `format: uuid` | `fc.uuid()` | v4 UUID generation |
|
|
| `format: date-time` | `fc.date().map(d => d.toISOString())` | ISO 8601 strings |
|
|
| `format: uri` | `fc.webUrl()` | Valid URL generation |
|
|
| `enum: ["a", "b"]` | `fc.constantFrom("a", "b")` | Exhaustive or sampled |
|
|
| `type: integer` | `fc.integer()` | Whole numbers |
|
|
| `minimum: 0` | `fc.integer({ min: 0 })` | Lower bound |
|
|
| `maximum: 100` | `fc.integer({ max: 100 })` | Upper bound |
|
|
| `exclusiveMinimum: true` + `minimum: 0` | `fc.integer({ min: 1 })` | Exclusive bounds |
|
|
| `multipleOf: 5` | `fc.integer().map(n => n * 5)` | Step values |
|
|
| `type: number` | `fc.float()` | Floating point |
|
|
| `type: boolean` | `fc.boolean()` | True/false |
|
|
| `type: array` | `fc.array(itemArb)` | Collection arbitrary |
|
|
| `minItems: 1` | `fc.array(itemArb, { minLength: 1 })` | Non-empty arrays |
|
|
| `maxItems: 10` | `fc.array(itemArb, { maxLength: 10 })` | Bounded arrays |
|
|
| `uniqueItems: true` | `.filter(arr => new Set(arr).size === arr.length)` | Set semantics |
|
|
| `type: object` + `properties` | `fc.record({ ... })` | Structured objects |
|
|
| `required: ["a", "b"]` | All required keys always present in record | Schema enforcement |
|
|
| `additionalProperties: false` | `fc.record({ ... }, { withDeletedKeys: false })` | Strict shape |
|
|
| `nullable: true` | `fc.option(arb, { nil: null })` | Null distribution |
|
|
| `default: "x"` | Bias toward default value in arbitrary | Edge case coverage |
|
|
| `readOnly: true` | Excluded from request body generation | Client cannot set |
|
|
| `writeOnly: true` | Excluded from response validation arbitrary | Server-only field |
|
|
|
|
**Implementation (`lib/schema-to-arbitrary.js`):**
|
|
|
|
```javascript
|
|
const fc = require('fast-check')
|
|
|
|
class SchemaToArbitrary {
|
|
convert(schema, context = 'request') {
|
|
if (schema.$ref) {
|
|
return this.resolveRef(schema.$ref)
|
|
}
|
|
|
|
// Handle nullable: type can be ["string", "null"] or nullable: true
|
|
const isNullable = schema.nullable === true ||
|
|
(Array.isArray(schema.type) && schema.type.includes('null'))
|
|
|
|
const baseArb = this.convertBaseType(schema, context)
|
|
|
|
if (isNullable) {
|
|
return fc.option(baseArb, { nil: null, freq: 5 })
|
|
}
|
|
|
|
return baseArb
|
|
}
|
|
|
|
convertBaseType(schema, context) {
|
|
const type = Array.isArray(schema.type)
|
|
? schema.type.find(t => t !== 'null')
|
|
: schema.type
|
|
|
|
switch (type) {
|
|
case 'string':
|
|
return this.stringArbitrary(schema)
|
|
case 'integer':
|
|
return this.integerArbitrary(schema)
|
|
case 'number':
|
|
return this.numberArbitrary(schema)
|
|
case 'boolean':
|
|
return fc.boolean()
|
|
case 'array':
|
|
return this.arrayArbitrary(schema, context)
|
|
case 'object':
|
|
return this.objectArbitrary(schema, context)
|
|
default:
|
|
// Union types (anyOf, oneOf)
|
|
if (schema.anyOf) {
|
|
return fc.oneof(...schema.anyOf.map(s => this.convert(s, context)))
|
|
}
|
|
if (schema.oneOf) {
|
|
return fc.oneof(...schema.oneOf.map(s => this.convert(s, context)))
|
|
}
|
|
return fc.anything()
|
|
}
|
|
}
|
|
|
|
stringArbitrary(schema) {
|
|
// format takes precedence over pattern
|
|
if (schema.format) {
|
|
switch (schema.format) {
|
|
case 'email': return fc.emailAddress()
|
|
case 'uuid': return fc.uuid()
|
|
case 'date-time': return fc.date().map(d => d.toISOString())
|
|
case 'date': return fc.date().map(d => d.toISOString().split('T')[0])
|
|
case 'uri': return fc.webUrl()
|
|
case 'hostname': return fc.domain()
|
|
case 'ipv4': return fc.ipV4()
|
|
case 'ipv6': return fc.ipV6()
|
|
}
|
|
}
|
|
|
|
if (schema.pattern) {
|
|
return fc.stringMatching(new RegExp(schema.pattern))
|
|
}
|
|
|
|
if (schema.x-regex) {
|
|
return fc.stringMatching(new RegExp(schema['x-regex']))
|
|
}
|
|
|
|
// Handle length constraints
|
|
const minLength = schema.minLength || 0
|
|
const maxLength = schema.maxLength || 100
|
|
|
|
if (minLength === maxLength) {
|
|
return fc.string({ minLength, maxLength })
|
|
}
|
|
|
|
return fc.string({ minLength, maxLength })
|
|
}
|
|
|
|
integerArbitrary(schema) {
|
|
const min = schema.minimum !== undefined ? schema.minimum : Number.MIN_SAFE_INTEGER
|
|
const max = schema.maximum !== undefined ? schema.maximum : Number.MAX_SAFE_INTEGER
|
|
|
|
// Handle exclusive bounds
|
|
const effectiveMin = schema.exclusiveMinimum ? min + 1 : min
|
|
const effectiveMax = schema.exclusiveMaximum ? max - 1 : max
|
|
|
|
let arb = fc.integer({ min: effectiveMin, max: effectiveMax })
|
|
|
|
if (schema.multipleOf) {
|
|
arb = arb.map(n => Math.round(n / schema.multipleOf) * schema.multipleOf)
|
|
.filter(n => n >= effectiveMin && n <= effectiveMax)
|
|
}
|
|
|
|
return arb
|
|
}
|
|
|
|
numberArbitrary(schema) {
|
|
const min = schema.minimum !== undefined ? schema.minimum : -1e308
|
|
const max = schema.maximum !== undefined ? schema.maximum : 1e308
|
|
|
|
let arb = fc.float({ min, max })
|
|
|
|
if (schema.multipleOf) {
|
|
arb = arb.map(n => Math.round(n / schema.multipleOf) * schema.multipleOf)
|
|
}
|
|
|
|
return arb
|
|
}
|
|
|
|
arrayArbitrary(schema, context) {
|
|
const itemArb = schema.items
|
|
? this.convert(schema.items, context)
|
|
: fc.anything()
|
|
|
|
const minItems = schema.minItems || 0
|
|
const maxItems = schema.maxItems || 10
|
|
|
|
let arb = fc.array(itemArb, { minLength: minItems, maxLength: maxItems })
|
|
|
|
if (schema.uniqueItems) {
|
|
arb = arb.filter(arr => new Set(arr).size === arr.length)
|
|
}
|
|
|
|
return arb
|
|
}
|
|
|
|
objectArbitrary(schema, context) {
|
|
const properties = {}
|
|
const required = new Set(schema.required || [])
|
|
|
|
for (const [key, propSchema] of Object.entries(schema.properties || {})) {
|
|
// Skip readOnly properties in request context, writeOnly in response context
|
|
if (context === 'request' && propSchema.readOnly) continue
|
|
if (context === 'response' && propSchema.writeOnly) continue
|
|
|
|
properties[key] = this.convert(propSchema, context)
|
|
}
|
|
|
|
// Handle additionalProperties
|
|
const withDeletedKeys = schema.additionalProperties === false
|
|
? false
|
|
: true
|
|
|
|
return fc.record(properties, {
|
|
withDeletedKeys,
|
|
requiredKeys: Array.from(required)
|
|
})
|
|
}
|
|
|
|
resolveRef(refPath) {
|
|
// Resolve $ref against OpenAPI components/schemas
|
|
return this.refResolver.resolve(refPath)
|
|
}
|
|
}
|
|
```
|
|
|
|
### Implicit Precondition Derivation
|
|
|
|
Standard schema properties encode preconditions that APOPHIS can extract automatically. These augment explicit `x-requires` annotations.
|
|
|
|
| Schema Property | Derived Precondition | APOSTL Formula Equivalent |
|
|
|---|---|---|
|
|
| `required: ["field"]` | Field must be present in request | `request_body(this).field != null` |
|
|
| `type: string` on param | Parameter must be string | `typeof request_body(this).field == "string"` |
|
|
| `format: email` | Must match email format | `request_body(this).field matches "^[^@]+@[^@]+$"` |
|
|
| `minimum: 0` | Must be non-negative | `request_body(this).field >= 0` |
|
|
| `enum: ["a", "b"]` | Must be one of allowed values | `request_body(this).field == "a" \|\| request_body(this).field == "b"` |
|
|
| `readOnly: true` on property | Must NOT be present in request | `request_body(this).field == null` |
|
|
| `maxLength: 255` | Must not exceed length | `request_body(this).field.length <= 255` |
|
|
| `pattern: "^[A-Z]+$"` | Must match pattern | `request_body(this).field matches "^[A-Z]+$"` |
|
|
|
|
**Example - Full Schema with Derived Preconditions:**
|
|
|
|
```yaml
|
|
paths:
|
|
/players/{playerNIF}:
|
|
post:
|
|
parameters:
|
|
- name: playerNIF
|
|
in: path
|
|
required: true
|
|
schema:
|
|
type: string
|
|
pattern: "^(1|2)[0-9]{8}$"
|
|
requestBody:
|
|
content:
|
|
application/json:
|
|
schema:
|
|
type: object
|
|
required: [firstName, lastName, email]
|
|
properties:
|
|
firstName:
|
|
type: string
|
|
minLength: 1
|
|
maxLength: 100
|
|
lastName:
|
|
type: string
|
|
minLength: 1
|
|
maxLength: 100
|
|
email:
|
|
type: string
|
|
format: email
|
|
age:
|
|
type: integer
|
|
minimum: 0
|
|
maximum: 150
|
|
nullable: true
|
|
role:
|
|
type: string
|
|
enum: [player, coach, referee]
|
|
default: player
|
|
createdAt:
|
|
type: string
|
|
format: date-time
|
|
readOnly: true
|
|
```
|
|
|
|
**Derived preconditions (automatically added to `x-requires`):**
|
|
|
|
```javascript
|
|
// From path parameter
|
|
'request_body(this).playerNIF matches "^(1|2)[0-9]{8}$"'
|
|
|
|
// From required fields
|
|
'request_body(this).firstName != null'
|
|
'request_body(this).lastName != null'
|
|
'request_body(this).email != null'
|
|
|
|
// From type constraints
|
|
'typeof request_body(this).firstName == "string"'
|
|
'typeof request_body(this).age == "integer" || request_body(this).age == null'
|
|
|
|
// From format constraints
|
|
'request_body(this).email matches "^[^@]+@[^@]+$"'
|
|
|
|
// From length constraints
|
|
'request_body(this).firstName.length >= 1'
|
|
'request_body(this).firstName.length <= 100'
|
|
|
|
// From numeric bounds
|
|
'request_body(this).age >= 0 || request_body(this).age == null'
|
|
'request_body(this).age <= 150 || request_body(this).age == null'
|
|
|
|
// From enum
|
|
'request_body(this).role == "player" || request_body(this).role == "coach" || request_body(this).role == "referee"'
|
|
|
|
// From readOnly (MUST NOT be sent by client)
|
|
'request_body(this).createdAt == null'
|
|
```
|
|
|
|
### Implicit Postcondition Derivation
|
|
|
|
Response schemas implicitly define postconditions about the shape and constraints of returned data.
|
|
|
|
| Schema Property | Derived Postcondition | APOSTL Formula Equivalent |
|
|
|---|---|---|
|
|
| `type: object` with `properties` | Response has expected shape | `response_body(this).field != null` (for required) |
|
|
| `readOnly: true` | Field preserved from creation | `response_body(this).field == previous(response_body(this).field)` |
|
|
| `format: uuid` on response | Returned ID is valid UUID | `response_body(this).id matches "^[0-9a-f-]{36}$"` |
|
|
| `nullable: false` | Field must be present | `response_body(this).field != null` |
|
|
| `writeOnly: true` | Field must NOT appear in response | `response_body(this).password == null` |
|
|
| `default: "x"` | If not set, defaults to x | `response_body(this).status == "x"` (when not explicitly set) |
|
|
|
|
### Model Structure Derivation
|
|
|
|
The schema topology itself defines the stateful model's structure, resource graph, and valid state transitions.
|
|
|
|
**Resource Graph from Schema Relationships:**
|
|
|
|
```yaml
|
|
components:
|
|
schemas:
|
|
Tournament:
|
|
type: object
|
|
properties:
|
|
tournamentId:
|
|
type: string
|
|
format: uuid
|
|
readOnly: true
|
|
name:
|
|
type: string
|
|
capacity:
|
|
type: integer
|
|
minimum: 1
|
|
enrollments:
|
|
type: array
|
|
items:
|
|
$ref: '#/components/schemas/Enrollment'
|
|
readOnly: true
|
|
organizer:
|
|
$ref: '#/components/schemas/Player'
|
|
|
|
Enrollment:
|
|
type: object
|
|
properties:
|
|
playerNIF:
|
|
type: string
|
|
pattern: "^(1|2)[0-9]{8}$"
|
|
tournamentId:
|
|
type: string
|
|
format: uuid
|
|
status:
|
|
type: string
|
|
enum: [pending, confirmed, cancelled]
|
|
default: pending
|
|
```
|
|
|
|
**Derived stateful model:**
|
|
|
|
```javascript
|
|
class TournamentModel {
|
|
constructor() {
|
|
// From schema properties + types
|
|
this.tournaments = new Map() // tournamentId -> Tournament
|
|
this.enrollments = new Map() // compositeKey -> Enrollment
|
|
this.players = new Map() // playerNIF -> Player
|
|
|
|
// Track relationships implied by schema structure
|
|
this.tournamentEnrollments = new Map() // tournamentId -> Set<playerNIF>
|
|
}
|
|
|
|
// Constructor derived from POST /tournaments schema
|
|
createTournament(name, capacity, organizerNIF) {
|
|
// Implicit precondition: capacity >= 1 (from minimum: 1)
|
|
if (capacity < 1) return { success: false, error: 'capacity < 1' }
|
|
|
|
// Implicit precondition: organizer must exist (from $ref relationship)
|
|
if (!this.players.has(organizerNIF)) return { success: false, error: 'organizer not found' }
|
|
|
|
const tournamentId = generateUUID() // from format: uuid
|
|
this.tournaments.set(tournamentId, {
|
|
tournamentId,
|
|
name,
|
|
capacity,
|
|
organizer: organizerNIF,
|
|
enrollments: [], // derived from array property
|
|
status: 'active'
|
|
})
|
|
this.tournamentEnrollments.set(tournamentId, new Set())
|
|
|
|
return { success: true, tournamentId }
|
|
}
|
|
|
|
// Mutator derived from POST /tournaments/{id}/enrollments
|
|
enrollPlayer(tournamentId, playerNIF) {
|
|
// Implicit precondition: tournament exists (from path param reference)
|
|
if (!this.tournaments.has(tournamentId)) return { success: false, error: 'tournament not found' }
|
|
|
|
// Implicit precondition: player exists (from $ref: '#/components/schemas/Player')
|
|
if (!this.players.has(playerNIF)) return { success: false, error: 'player not found' }
|
|
|
|
const tournament = this.tournaments.get(tournamentId)
|
|
const currentEnrollments = this.tournamentEnrollments.get(tournamentId)
|
|
|
|
// Invariant derived from x-invariants or schema constraints
|
|
if (currentEnrollments.size >= tournament.capacity) {
|
|
return { success: false, error: 'tournament full' }
|
|
}
|
|
|
|
// Implicit postcondition: enrollment status defaults to "pending"
|
|
const enrollment = {
|
|
playerNIF,
|
|
tournamentId,
|
|
status: 'pending' // from default: pending
|
|
}
|
|
|
|
this.enrollments.set(`${tournamentId}:${playerNIF}`, enrollment)
|
|
currentEnrollments.add(playerNIF)
|
|
tournament.enrollments.push(enrollment)
|
|
|
|
return { success: true, enrollment }
|
|
}
|
|
|
|
// Observer derived from GET /tournaments/{id}
|
|
getTournament(tournamentId) {
|
|
return this.tournaments.get(tournamentId) || null
|
|
}
|
|
|
|
// Invariant check derived from schema + x-invariants
|
|
checkInvariants() {
|
|
for (const [id, tournament] of this.tournaments) {
|
|
// Schema-derived: capacity must be >= 1
|
|
if (tournament.capacity < 1) return false
|
|
|
|
// Schema-derived: tournamentId must be UUID format
|
|
if (!isValidUUID(tournament.tournamentId)) return false
|
|
|
|
// x-invariant-derived: enrollments <= capacity
|
|
const enrollmentCount = this.tournamentEnrollments.get(id).size
|
|
if (enrollmentCount > tournament.capacity) return false
|
|
}
|
|
return true
|
|
}
|
|
}
|
|
```
|
|
|
|
### Semantic Hint Extraction
|
|
|
|
Descriptions and examples provide testing guidance:
|
|
|
|
| Source | Extraction | Testing Use |
|
|
|---|---|---|
|
|
| `description: "Player's fiscal identification number"` | Field semantic meaning | Better error messages, named arbitraries |
|
|
| `example: "123456789"` | Concrete valid value | Seed for fast-check, baseline test case |
|
|
| `description: "Must be unique within tournament"` | Uniqueness constraint | Implicit postcondition / model invariant |
|
|
| `description: "Automatically set on creation"` | readOnly semantic | Skip in request generation |
|
|
|
|
**Named Arbitraries from Descriptions:**
|
|
|
|
```javascript
|
|
// Instead of anonymous fc.string(), generate named arbitraries:
|
|
fc.string().map(s => ({ value: s, _name: 'playerNIF' }))
|
|
|
|
// This enables better shrinking messages:
|
|
// "Property failed with playerNIF = 'abc' (must match /^(1|2)[0-9]{8}$/)"
|
|
```
|
|
|
|
### Integration: Layered Derivation
|
|
|
|
APOPHIS combines standard schema derivation with explicit APOSTL contracts in layers:
|
|
|
|
```
|
|
Layer 1: Standard JSON Schema
|
|
→ Type-safe arbitrary generation
|
|
→ Basic preconditions (required, type, format)
|
|
→ Model structure ($ref, array relationships)
|
|
|
|
Layer 2: x-regex annotations
|
|
→ Refined arbitrary generation (regex instead of format)
|
|
→ Edge case generation (boundary values from regex)
|
|
|
|
Layer 3: x-requires / x-ensures
|
|
→ Semantic pre/postconditions
|
|
→ Cross-resource conditions
|
|
→ Header and state conditions
|
|
|
|
Layer 4: x-invariants
|
|
→ Model invariants
|
|
→ Stateful property generation
|
|
|
|
Layer 5: x-category
|
|
→ Operation classification for test ordering
|
|
```
|
|
|
|
**Complete Example - All Layers Combined:**
|
|
|
|
```yaml
|
|
paths:
|
|
/tournaments/{tournamentId}/enrollments:
|
|
post:
|
|
x-category: constructor
|
|
x-requires:
|
|
# Layer 3: Semantic preconditions
|
|
- response_body(GET /tournaments/{tournamentId}) != null
|
|
x-ensures:
|
|
# Layer 3: Semantic postconditions
|
|
- response_code(this) == 201
|
|
- response_body(this).status == "pending"
|
|
parameters:
|
|
- name: tournamentId
|
|
in: path
|
|
required: true
|
|
schema:
|
|
type: string
|
|
format: uuid # Layer 1: Type constraint
|
|
requestBody:
|
|
content:
|
|
application/json:
|
|
schema:
|
|
type: object
|
|
required: [playerNIF] # Layer 1: Required field
|
|
properties:
|
|
playerNIF:
|
|
type: string
|
|
x-regex: "(1|2)[0-9]{8}" # Layer 2: Refined generation
|
|
description: "Player fiscal ID"
|
|
notes:
|
|
type: string
|
|
maxLength: 500 # Layer 1: Length constraint
|
|
nullable: true
|
|
```
|
|
|
|
**Derived test artifacts:**
|
|
|
|
```javascript
|
|
// Layer 1: Standard schema arbitrary
|
|
const enrollmentRequestArb = fc.record({
|
|
playerNIF: fc.string(), // Base type constraint
|
|
notes: fc.option(fc.string({ maxLength: 500 }), { nil: null })
|
|
}, {
|
|
requiredKeys: ['playerNIF'] // required field enforcement
|
|
})
|
|
|
|
// Layer 2: x-regex refines the arbitrary
|
|
const refinedArb = fc.record({
|
|
playerNIF: fc.stringMatching(/(1|2)[0-9]{8}/), // Refined by x-regex
|
|
notes: fc.option(fc.string({ maxLength: 500 }), { nil: null })
|
|
}, {
|
|
requiredKeys: ['playerNIF']
|
|
})
|
|
|
|
// Layer 1+3: Derived preconditions
|
|
const preconditions = [
|
|
'request_body(this).playerNIF != null', // from required
|
|
'typeof request_body(this).playerNIF == "string"', // from type
|
|
'request_body(this).notes.length <= 500 || request_body(this).notes == null', // from maxLength + nullable
|
|
'response_body(GET /tournaments/{tournamentId}) != null' // from x-requires
|
|
]
|
|
|
|
// Layer 1+3: Derived postconditions
|
|
const postconditions = [
|
|
'response_code(this) == 201', // from x-ensures
|
|
'response_body(this).status == "pending"', // from x-ensures
|
|
'typeof response_body(this).playerNIF == "string"', // from response schema type
|
|
'response_body(this).playerNIF matches "^(1|2)[0-9]{8}$"' // from x-regex on response
|
|
]
|
|
|
|
// Layer 4+5: Derived stateful model
|
|
class EnrollmentStatefulModel {
|
|
constructor() {
|
|
this.tournaments = new Map()
|
|
this.enrollments = new Map() // tournamentId -> Map<playerNIF, enrollment>
|
|
}
|
|
|
|
createEnrollment(tournamentId, playerNIF, notes) {
|
|
// Layer 3: Explicit precondition
|
|
if (!this.tournaments.has(tournamentId)) return { success: false }
|
|
|
|
// Layer 1: Schema-derived model structure
|
|
const enrollment = {
|
|
playerNIF,
|
|
notes,
|
|
status: 'pending', // from x-ensures
|
|
tournamentId
|
|
}
|
|
|
|
if (!this.enrollments.has(tournamentId)) {
|
|
this.enrollments.set(tournamentId, new Map())
|
|
}
|
|
this.enrollments.get(tournamentId).set(playerNIF, enrollment)
|
|
|
|
return { success: true, enrollment }
|
|
}
|
|
}
|
|
|
|
// fast-check property combining all layers
|
|
fc.assert(
|
|
fc.property(
|
|
fc.uuid(), // tournamentId from format: uuid
|
|
fc.stringMatching(/(1|2)[0-9]{8}/), // playerNIF from x-regex
|
|
fc.option(fc.string({ maxLength: 500 }), { nil: null }), // notes from schema
|
|
(tournamentId, playerNIF, notes) => {
|
|
// Execute API call (injected request)
|
|
// Verify all preconditions + postconditions
|
|
// Check model synchronization
|
|
}
|
|
)
|
|
)
|
|
```
|
|
|
|
### Guarantees of Schema-Driven Derivation
|
|
|
|
By deriving from standard schema:
|
|
|
|
1. **No false positives from type mismatches**: Generated data always passes Fastify's own JSON Schema validation
|
|
2. **Boundary coverage**: `minimum`, `maximum`, `minLength`, `maxLength` ensure edge cases are tested
|
|
3. **Semantic validity**: `format`, `pattern`, `enum` guarantee data makes business sense
|
|
4. **Relationship integrity**: `$ref`, array `items` build correct resource graphs in models
|
|
5. **Reduced annotation burden**: APIs with good schemas need fewer `x-*` annotations to be fully testable
|
|
6. **Schema drift detection**: If schema changes, derived tests automatically adapt
|
|
|
|
## Future Extensions
|
|
|
|
- **RAML Support**: Extend beyond OpenAPI to RAML specifications
|
|
- **GraphQL**: Adapt contract concepts to GraphQL schemas
|
|
- **Mutation Testing**: Verify contract completeness
|
|
- **Performance Contracts**: Add latency and throughput requirements
|
|
- **Visual Testing**: Contract-based screenshot comparison for UI APIs
|
|
- **Chaos Engineering**: Inject failures based on contract boundaries
|
|
|
|
## References
|
|
|
|
- Ribeiro, A.C.M. (2021). "Invariant-Driven Automated Testing". MSc Thesis, NOVA University of Lisbon.
|
|
- APOSTL: API PrOperty SpecificaTion Language
|
|
- PETIT: aPi tEsTIng Tool
|
|
- OpenAPI Specification v3.0
|
|
- Fastify Plugin Architecture
|
|
- Design by Contract (Meyer, 1988)
|
|
- Hoare Logic (Hoare, 1969)
|
|
- QuickLogic3: Contextual Four-Valued Reasoning Runtime
|