Skip to content

Commit ed0f32a

Browse files
committed
docs(formal): add table ordering convention, fix project_name key and change_history arg
Apply table ordering guidance to all formal document headers. Sort scannable reference tables (definitions, constraints, packages) alphabetically by first column. Fix project-name -> project_name key and add missing change_history arg to formal_doc.with() where needed. All documents compile cleanly against current core.typ.
1 parent 326854d commit ed0f32a

3 files changed

Lines changed: 54 additions & 27 deletions

File tree

docs/formal/software_design_specification.typ

Lines changed: 24 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,12 @@
88
// Modification Policy:
99
// - Edit this file for project-specific SDS content.
1010
// - Keep shared presentation logic in core.typ.
11+
// Table Ordering:
12+
// Sort any table whose rows a reader might scan to locate a specific
13+
// entry — definitions, acronyms, constraints, packages, interfaces,
14+
// and similar reference tables. Sort alphabetically by the first
15+
// column. Tables with an inherent sequence (requirement IDs within
16+
// a section, change history, workflow steps) retain their logical order.
1117
// SPDX-License-Identifier: BSD-3-Clause
1218
// ============================================================================
1319

@@ -100,19 +106,20 @@ This document covers:
100106

101107
== Dependency Rules
102108

109+
// Sort rows alphabetically by the first column.
103110
#table(
104111
columns: (auto, 1fr, auto),
105112
table.header([*Package*], [*Dependencies*], [*SPARK_Mode*]),
106113
[Functional], [None], [On],
107-
[Functional.Result], [Functional], [On],
108-
[Functional.Option], [Functional], [On],
109114
[Functional.Either], [Functional], [On],
115+
[Functional.Option], [Functional], [On],
116+
[Functional.Result], [Functional], [On],
117+
[Functional.Scoped], [Ada.Finalization], [Off],
110118
[Functional.Try], [Ada.Exceptions, Result, Option], [Off],
111119
[Functional.Try.Map_To_Result], [Try], [Off],
112120
[Functional.Try.Map_To_Result_With_Param], [Try], [Off],
113-
[Functional.Try.To_Result], [Try, Result], [Off],
114121
[Functional.Try.To_Option], [Try, Option], [Off],
115-
[Functional.Scoped], [Ada.Finalization], [Off],
122+
[Functional.Try.To_Result], [Try, Result], [Off],
116123
[Functional.Version], [None], [On],
117124
)
118125

@@ -145,19 +152,20 @@ src/
145152

146153
== Package Descriptions
147154

155+
// Sort rows alphabetically by the first column.
148156
#table(
149157
columns: (auto, 1fr, auto),
150158
table.header([*Package*], [*Purpose*], [*SPARK*]),
151159
[`Functional`], [Root namespace, common declarations.], [On],
152-
[`Functional.Result`], [Success/failure discriminated union with combinators.], [On],
153-
[`Functional.Option`], [Presence/absence discriminated union with combinators.], [On],
154160
[`Functional.Either`], [Left/right discriminated union with combinators.], [On],
161+
[`Functional.Option`], [Presence/absence discriminated union with combinators.], [On],
162+
[`Functional.Result`], [Success/failure discriminated union with combinators.], [On],
163+
[`Functional.Scoped`], [RAII guard generics.], [Off],
155164
[`Functional.Try`], [Exception-to-Result/Option bridge infrastructure.], [Off],
156165
[`Functional.Try.Map_To_Result`], [Declarative exception mapping (no extra parameter).], [Off],
157166
[`Functional.Try.Map_To_Result_With_Param`], [Declarative exception mapping (parameterized action).], [Off],
158-
[`Functional.Try.To_Result`], [Procedural exception mapping (legacy).], [Off],
159167
[`Functional.Try.To_Option`], [Exception-to-Option for probe operations.], [Off],
160-
[`Functional.Scoped`], [RAII guard generics.], [Off],
168+
[`Functional.Try.To_Result`], [Procedural exception mapping (legacy).], [Off],
161169
[`Functional.Version`], [Library version constants.], [On],
162170
)
163171

@@ -299,14 +307,15 @@ Consumers of the Functional library use Result and Option types for all expected
299307

300308
== Module Responsibilities
301309

310+
// Sort rows alphabetically by the first column.
302311
#table(
303312
columns: (auto, 1fr),
304313
table.header([*Module*], [*Error Handling Role*]),
305-
[Result], [Carry success/failure values through combinators.],
306-
[Option], [Carry present/absent values through combinators.],
307314
[Either], [Carry left/right values through combinators.],
308-
[Try], [Catch exceptions at boundaries and convert to Result or Option.],
315+
[Option], [Carry present/absent values through combinators.],
316+
[Result], [Carry success/failure values through combinators.],
309317
[Scoped], [Suppress exceptions from cleanup actions to prevent double-exception scenarios.],
318+
[Try], [Catch exceptions at boundaries and convert to Result or Option.],
310319
)
311320

312321
== Try Usage Guidelines
@@ -377,14 +386,15 @@ Functional targets a *spark-targeted* assurance posture. Core types (Result, Opt
377386

378387
== Module Assessment
379388

389+
// Sort rows alphabetically by the first column.
380390
#table(
381391
columns: (auto, auto, 1fr),
382392
table.header([*Module*], [*SPARK*], [*Notes*]),
383-
[Result], [On], [Pure functional type, fully provable.],
384-
[Option], [On], [Pure functional type, fully provable.],
385393
[Either], [On], [Pure functional type, fully provable.],
386-
[Try], [Off], [Exception handling is inherently outside SPARK.],
394+
[Option], [On], [Pure functional type, fully provable.],
395+
[Result], [On], [Pure functional type, fully provable.],
387396
[Scoped], [Off], [Ada.Finalization is outside SPARK.],
397+
[Try], [Off], [Exception handling is inherently outside SPARK.],
388398
[Version], [On], [Constants only.],
389399
)
390400

docs/formal/software_requirements_specification.typ

Lines changed: 21 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,12 @@
88
// Modification Policy:
99
// - Edit this file for project-specific SRS content.
1010
// - Keep shared presentation logic in core.typ.
11+
// Table Ordering:
12+
// Sort any table whose rows a reader might scan to locate a specific
13+
// entry — definitions, acronyms, constraints, packages, interfaces,
14+
// and similar reference tables. Sort alphabetically by the first
15+
// column. Tables with an inherent sequence (requirement IDs within
16+
// a section, change history, workflow steps) retain their logical order.
1117
// SPDX-License-Identifier: BSD-3-Clause
1218
// ============================================================================
1319

@@ -79,18 +85,19 @@ This Software Requirements Specification (SRS) defines the functional and non-fu
7985

8086
== Definitions and Acronyms
8187

88+
// Sort rows alphabetically by the first column.
8289
#table(
8390
columns: (auto, 1fr),
8491
table.header([*Term*], [*Definition*]),
85-
[Result], [A discriminated union representing success (Ok) or failure (Error).],
86-
[Option], [A discriminated union representing presence (Some) or absence (None).],
92+
[Discriminated Union], [Ada record type with a discriminant controlling the variant.],
8793
[Either], [A discriminated union representing one of two valid values (Left or Right).],
88-
[Railway-Oriented Programming], [A pattern where operations are chained, with errors automatically propagating through the pipeline.],
94+
[Functor], [Abstraction for transforming wrapped values (Map).],
95+
[Monad], [Abstraction for sequencing computations (Map, And_Then).],
96+
[Option], [A discriminated union representing presence (Some) or absence (None).],
8997
[RAII], [Resource Acquisition Is Initialization — automatic cleanup pattern using Ada finalization.],
98+
[Railway-Oriented Programming], [A pattern where operations are chained, with errors automatically propagating through the pipeline.],
99+
[Result], [A discriminated union representing success (Ok) or failure (Error).],
90100
[SPARK], [A formally verifiable subset of Ada.],
91-
[Discriminated Union], [Ada record type with a discriminant controlling the variant.],
92-
[Monad], [Abstraction for sequencing computations (Map, And_Then).],
93-
[Functor], [Abstraction for transforming wrapped values (Map).],
94101
)
95102

96103
== References
@@ -134,12 +141,13 @@ Unlike the typical hybrid DDD/Clean/Hexagonal project, Functional does not have
134141

135142
== User Classes
136143

144+
// Sort rows alphabetically by the first column.
137145
#table(
138146
columns: (auto, 1fr),
139147
table.header([*User Class*], [*Description*]),
140-
[Library Consumers], [Ada developers using Functional types in their projects.],
141148
[Domain Developers], [Developers implementing business logic with Result/Option.],
142149
[Infrastructure Developers], [Developers implementing I/O boundaries with Try bridges.],
150+
[Library Consumers], [Ada developers using Functional types in their projects.],
143151
)
144152

145153
== Operating Environment
@@ -158,13 +166,14 @@ Unlike the typical hybrid DDD/Clean/Hexagonal project, Functional does not have
158166

159167
== Constraints
160168

169+
// Sort rows alphabetically by the first column.
161170
#table(
162171
columns: (auto, 1fr),
163172
table.header([*Constraint*], [*Rationale*]),
164173
[Ada 2022], [Required for modern language features.],
165174
[No Heap Allocation], [Stack-based discriminated unions ensure embedded safety.],
166-
[SPARK Subset], [Core types must remain formally verifiable.],
167175
[No Runtime Dependencies], [Only the Ada standard library is permitted.],
176+
[SPARK Subset], [Core types must remain formally verifiable.],
168177
)
169178

170179
= Interface Requirements
@@ -423,13 +432,14 @@ No specific hardware requirements. The library operates within standard Ada runt
423432

424433
== Verification Methods
425434

435+
// Sort rows alphabetically by the first column.
426436
#table(
427437
columns: (auto, 1fr),
428438
table.header([*Method*], [*Description*]),
429-
[Unit Testing], [All public operations of Result, Option, Either, Try, Scoped.],
430-
[SPARK Proof], [Result, Option, Either core operations.],
431-
[Integration Testing], [Try with real exception scenarios.],
432439
[Code Review], [All changes reviewed before merge.],
440+
[Integration Testing], [Try with real exception scenarios.],
441+
[SPARK Proof], [Result, Option, Either core operations.],
442+
[Unit Testing], [All public operations of Result, Option, Either, Try, Scoped.],
433443
)
434444

435445
== Traceability Matrix

docs/formal/software_test_guide.typ

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,12 @@
88
// Modification Policy:
99
// - Edit this file for project-specific STG content.
1010
// - Keep shared presentation logic in core.typ.
11+
// Table Ordering:
12+
// Sort any table whose rows a reader might scan to locate a specific
13+
// entry — definitions, acronyms, constraints, packages, interfaces,
14+
// and similar reference tables. Sort alphabetically by the first
15+
// column. Tables with an inherent sequence (requirement IDs within
16+
// a section, change history, workflow steps) retain their logical order.
1117
// SPDX-License-Identifier: BSD-3-Clause
1218
// ============================================================================
1319

@@ -134,13 +140,14 @@ test/
134140

135141
== Naming Conventions
136142

143+
// Sort rows alphabetically by the first column.
137144
#table(
138145
columns: (auto, auto, 1fr),
139146
table.header([*Element*], [*Convention*], [*Example*]),
147+
[Runner], [`unit_runner.adb`], [`unit_runner.adb`],
140148
[Test file], [`test_<module>.adb`], [`test_result.adb`],
141-
[Test procedure], [`Test_<Operation>_<Scenario>`], [`Test_Map_Success`],
142149
[Test package], [`Test_<Module>`], [`Test_Result`],
143-
[Runner], [`unit_runner.adb`], [`unit_runner.adb`],
150+
[Test procedure], [`Test_<Operation>_<Scenario>`], [`Test_Map_Success`],
144151
)
145152

146153
== Build/Test Projects

0 commit comments

Comments
 (0)