[docs] Update glossary - weekly full scan

[github-actions]

Glossary Updates

Scan Type: Full scan (weekly — Monday)

Terms Added:

• ArgumentArity: MTP struct defining min/max values a command-line option accepts; important FV target
• DelayBackoffType: Public enum in the Retry extension specifying retry delay strategy (Constant/Exponential)
• Formal Verification (FV): The mathematical proof practice now active in this project via Lean 4
• FV Target: A code component selected for formal verification, progressing through defined phases
• Lean 4: The theorem prover used for FV proofs in formal-verification/lean/FVSquad/
• Lean Squad: The automated agentic workflow managing the FV lifecycle
• TreeNodeFilter: MTP component evaluating Boolean-algebra filter expressions against test nodes

Terms Updated: None

Changes Analyzed:

• Reviewed 1 commit from last 7 days
• Analyzed 17 merged PRs (primarily Lean Squad FV work, performance improvements, and agentic infrastructure)
• Processed formal-verification/TARGETS.md, CORRESPONDENCE.md, and FVSquad/README.md

Related Changes:

• PR [Lean Squad] feat(fv): Task 1 — expand FV targets to include SplitCommandLine and TreeNodeFilter #7849: expand FV targets to include SplitCommandLine and TreeNodeFilter
• PR [Lean Squad] feat(fv): Task 6 — Lean–C# correspondence review for primary targets #7860: Lean–C# correspondence review for primary FV targets
• PR [Lean Squad] feat(ci): Task 9 — skip guard + FVSquad scaffold for lean-proofs workflow #7859: FVSquad directory scaffold and lean-proofs CI skip guard
• PR [Lean Squad] feat(fv): Task 2 — informal spec for CommandLineParser.TryUnescape #7835: informal spec for CommandLineParser.TryUnescape
• PR Avoid LINQ enumerator allocation in FrameworkEngineMetadataProperty hot path #7837: Add unit tests for RetryAttribute (BackoffType validation)

Note

🔒 Integrity filter blocked 3 items

The following items were blocked because they don't meet the GitHub integrity level.

• #7844 search_pull_requests: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• #7827 search_pull_requests: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".
• #7826 search_pull_requests: has lower integrity than agent requires. The agent cannot read data with integrity below "approved".

To allow these resources, lower min-integrity in your GitHub frontmatter:

tools:
  github:
    min-integrity: approved  # merged | approved | unapproved | none

Generated by Glossary Maintainer · ● 1.3M · ◷

• expires on Apr 29, 2026, 12:56 PM UTC

---

Note

This was originally intended as a pull request, but GitHub Actions is not permitted to create or approve pull requests in this repository.
The changes have been pushed to branch docs/glossary-weekly-scan-2026-04-27-07df87ef952674e1.

Click here to create the pull request

To fix the permissions issue, go to Settings → Actions → General and enable Allow GitHub Actions to create and approve pull requests. See also: gh-aw FAQ

Show patch preview (93 of 93 lines)

From 3e77641d3efb4c72a2ab8560cf63eda9ff25837c Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Mon, 27 Apr 2026 12:54:27 +0000
Subject: [PATCH] docs: update glossary with weekly scan terms

Add 7 new terms identified from the last 7 days of changes:
- ArgumentArity: MTP struct for command-line option arity
- DelayBackoffType: Retry extension enum for backoff strategy
- Formal Verification (FV): mathematical proof initiative
- FV Target: code components selected for formal verification
- Lean 4: theorem prover used for FV
- Lean Squad: automated FV agentic workflow
- TreeNodeFilter: MTP test filter by node properties

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 docs/glossary.md | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/docs/glossary.md b/docs/glossary.md
index 85f1008..34725a7 100644
--- a/docs/glossary.md
+++ b/docs/glossary.md
@@ -4,6 +4,10 @@ This glossary defines key terms and concepts used throughout the MSTest and Micr
 
 ## A
 
+### ArgumentArity
+
+An MTP struct (`ArgumentArity.cs`) that defines the minimum and maximum number of values a command-line option accepts. Provides five predefined constants: `Zero` (0,0), `ZeroOrOne` (0,1), `ZeroOrMore` (0,∞), `ExactlyOne` (1,1), and `OneOrMore` (1,∞). Used by `ICommandLineOptionsProvider` implementations to declare option shapes.
+
 ### AzureDevOpsReport
 
 An MTP extension (`Microsoft.Testing.Extensions.AzureDevOpsReport`) that formats and reports test results to Azure DevOps pipelines. It generates pipeline-compatible output including TFM and test name details for richer CI reporting.
@@ -14,12 +18,26 @@ An MTP extension (`Microsoft.Testing.Extensions.AzureDevOpsReport`) that formats
 
 An MTP extension (`Microsoft.Testing.Extensions.CrashDump`) that automatically captures a process memory dump when the test host crashes. Useful for diagnosing unexpected process termination during tes
... (truncated)

[github-actions]

This issue was automatically closed because it expired on 2026-04-29T12:56:23.168Z.

Closed by Workflow