Foundations of analysis
Trust comes from a scoped chain: source and compiler facts, explicit assumptions, a rule-specific decision, and evidence that the implementation handles the claimed cases. A scientific method and an implemented checker need separate justification.
From a program to a model#
Static analysis reasons about a representation of a program rather than executing every possible run. Cousot and Cousot's abstract interpretation paper gives a mathematical framework for approximating program behavior and computing invariants. A sound abstraction can support conclusions under its stated model and assumptions.
That theory is not a proof of Swift Analyzer. The tool must still collect the right facts, model the relevant semantics, handle unsupported behavior, and validate its implementation. These docs make no claim that every rule is a formally verified abstract interpreter.
Follow the evidence chain#
Select a build world and identify its source, compiler, SDK and dependencies.
Admit facts only when their identity and quality satisfy the input contract.
Extract the source forms recognized by the selected rule.
Evaluate observations with the rule's required facts and assumptions.
Report a finding, a supported non-finding, or unknown with its reasons and anchors.
This ordered list is also the text alternative to the analysis pipeline: build world → admitted facts → rule observations → decision and evidence. Missing information at an earlier step limits what a later step may conclude.
Context across a detached task#
The Swift structured-concurrency proposal defines how tasks inherit context and how detached tasks differ. The Swift concurrency guide explains actor isolation and suspension. The tutorial uses a recognized detached boundary leading to a MainActor assertion; the analyzer reports the lost required context as V-EXEC-03.
The method depends on recognizing both the required context and the transition. It does not infer a physical thread hop from every await, and an unresolved callback contract remains unknown. The observed tutorial finding supports that particular source form, not all concurrency code.
State transitions and resource obligations#
A guard check follows recognized acquire, suspension and release events. A resource check follows creation, transfer, use and discharge of an obligation. A missing or opaque event can prevent a complete trace. The current source-scan implementation recognizes bounded forms; it is not a general model of every lock, handle or user-defined ownership protocol.
For negative claims, an incomplete model is especially important: absence of a path in a graph is meaningful only when the relevant graph and entry points are complete. Coverage and unknown explains why absence of findings cannot substitute for that premise.
What validates the implementation#
Read How we validate checks for actual positive, control and unsupported examples, exact revision and profile, and the limits of the measurements. Each rule page states availability, its intended method, required evidence and unknown boundary.