← All specifications

JSF Air Vehicle C++ (JSF++) — ponens Policy Pack

This pack maps the JSF Air Vehicle C++ Coding Standards (“JSF++”) — developed for the Lockheed Martin F-35 Joint Strike Fighter, with input from Bjarne Stroustrup — onto computable ponens policies. Like the MISRA packs it governs the compliance process, not the individual coding rules; but JSF++ has a distinctive three-tier category scheme and a tiered deviation-approval chain that make it a separate pack.

Source: JSF Air Vehicle C++ Coding Standards (Lockheed Martin, Doc. 2RDU00001 Rev C, Dec 2005) — https://www.stroustrup.com/JSF-AV-rules.pdf

Why this maps onto ponens

JSF++‘s 221 numbered rules (AV Rule 1…) are checked by static analysis of source, so ponens does not re-encode them. What ponens governs is JSF++‘s compliance process, which is well-defined and distinctive:

Rule categories (§4.2.1):

Deviation-approval chain (AV Rules 4-7):

Safety-critical (SEAL 1) obligations: run-time checking / defensive programming (AV Rule 15); only DO-178B Level A certifiable libraries (AV Rule 16 — a direct link to the DO-178C pack); no dead code (code not traceable to a requirement).

JSF++ponens
The coding/CI activity recordthe trace
A compliance-process obligationa policy (temporal formula)
Shall / Will (mandatory) vs Should (advisory)error (Red) / warning (Amber)

Trace model

This pack reuses existing vocabulary (StaticAnalysis, Deviation, GitCommit, EditFile) — no new action types. Per-action predicates: should_deviation, shall_deviation, will_deviation, eng_lead_approved, product_manager_approved, documented_in_file, shall_violation, will_violation, should_violation, deviation_approved, recorded, shall_verified, jsf_ruleset, safety_critical, runtime_checking, library_use, certified_library, dead_code, rationale_recorded, approval_recorded.

Worked traces: examples/jsf/governed.json (12/12 Green) and violating.json (9 Red + 2 Amber). Run ponens trace check <file>.

The pack

errorRed; warningAmber.

Deviation Approval — AV 4-7 (conformance / auditability)

PolicyFormulaRAG
jsf_should_deviation_approvedG(should_deviation → eng_lead_approved)A
jsf_shall_will_deviation_dual_approvedG((shall_deviation ∨ will_deviation) → eng_lead_approved ∧ product_manager_approved)R
jsf_shall_deviation_documentedG(shall_deviation → documented_in_file)R

Shall / Will / Should (conformance)

PolicyFormulaRAG
jsf_shall_violation_deviatedG(shall_violation → P(deviation_approved))R
jsf_will_violation_deviatedG(will_violation → P(deviation_approved))R
jsf_should_violation_recordedG(should_violation → recorded)A

Verification & Enforcement (safety / workflow)

PolicyFormulaRAG
jsf_shall_rules_verifiedG(GitCommit → P(shall_verified))R
jsf_static_analysis_before_commitG(GitCommit → P(StaticAnalysis ∧ jsf_ruleset))R

Safety-Critical — SEAL 1 (safety)

PolicyFormulaRAG
jsf_runtime_checking_providedG(safety_critical → runtime_checking)R
jsf_certified_libraries_onlyG(safety_critical ∧ library_use → certified_library)R
jsf_no_dead_codeG(¬dead_code)R

Deviation Records (auditability)

PolicyFormulaRAG
jsf_deviation_record_maintainedG(Deviation → rationale_recorded ∧ approval_recorded)R

Aggregation

ponens trace check aggregates the pack: any error fail ⇒ Red (an undeviated shall/will violation, a singly-approved shall deviation, uncertified safety-critical libraries, or dead code); else any warning fail ⇒ Amber (should-rule deviations and records); else Green.

Relationship to other packs

JSF++ sits alongside the MISRA C/C++ packs (it even cross-references many MISRA rules in its text) and links to DO-178C via AV Rule 16’s certifiable-library requirement — the same way a real F-35 software programme stacks these standards. The 221 individual rules themselves are out of scope; they are enforced by a JSF++-checking static analyzer, and this pack governs the compliance process around that analyzer’s results.