Test Specification
Test specifications for the affirmatrix requirements (SEG-TS-nnn). Each
one is the docstring of a test under tests/: its first line is the title,
the paragraphs beneath it state the claim, and two docstring fields carry its
identity (:test-id:) and the requirements it verifies (:verifies:).
This page is generated from those docstrings at every build, so it always
shows the tests as they are. The verifies links point at the requirement
specification, whose pages show each requirement’s tests under “is verified
by”; the test report links each result back here under “is reported by”.
tests/specification/test_case_evidence_removal.py
Test Specification: The affirmation store refuses a write that names a test outcome node or an evidence edge. SEG-TS-098
|
A case holds nothing. A write of a requirement node together with a test outcome node is refused, and no file of the case changes. A write of a Confirms edge, a Witnesses edge or an Excuses edge is refused, and no file changes. A write of a Refines edge together with a Confirms edge is refused, and the Refines edge is not written. A write of a waiver node and a write of a Refines edge are accepted. |
Test Specification: Case sync removes every stored outcome and evidence edge, after it writes the derived stream. SEG-TS-099
|
The legacy case holds 10 test outcome nodes, 10 Confirms edges and 12 Witnesses edges. Case sync runs from a stream of the design alone and exits with status 0. Afterwards the case holds no test outcome node and no Confirms or Witnesses edge. The report names each of the 10 outcomes, and each of the 22 edges by its two ends and its kind. The documents of the strong edges, the review events, the stored package and the other node documents are byte for byte as before. The six affirmed edges keep their hashes. |
The legacy case is synced from a stream of the design alone. A second sync from the same stream exits with status 0. Every file of the case is byte for byte as it was after the first sync, and the report names none of the removed outcomes. |
Test Specification: A case sync that cannot write the derived stream changes nothing, evidence included. SEG-TS-101
|
The stream of the design holds one Refines edge that the case does not store, from FX-SREQ-2 to FX-SREQ-1. The legacy case’s copy of the Refines schema does not allow an edge that ends at FX-SREQ-1, and every record the case stores is still valid. Case sync exits with status 2. Every file of the case is byte for byte as before, so the 10 outcomes and the 22 evidence edges are still stored. |
Test Specification: Case sync reports a vanished strong edge and keeps it, and reports no vanished evidence edge. SEG-TS-102
|
The stream of the design lacks the Refines edge from FX-SREQ-2 to FX-SYS-1, which the legacy case stores as pending. Case sync exits with status 0. It reports exactly one vanished edge, that Refines edge, and reports no vanished edge of kind Confirms, Witnesses or Excuses, although the stream holds none of the 22 evidence edges the case stored. The Refines edge is still in the case. |
Test Specification: A package stored before run bundles were recorded is read back as written. SEG-TS-103
|
The legacy case stores one package of four documents, and its evidence manifest has no field for run bundles. The store reads the package and returns the four documents. After a refresh of the case’s schema copy to the packaged schemas, the store reads the same package again and returns the same four documents. |
tests/specification/test_cli_producer_reports.py
The configured producer names a requirement export that does not exist. The reason is the message the library gives when it builds that producer. The output of case check holds that message in full. The output of case check with the machine-readable rendering is a JSON object with that message in one of its string values. |
Test Specification: graph check names what it checked by its location, in both renderings. SEG-TS-181
|
A case is synced from a current stream. So the case and the stream hold the same graph, and every count in the two outputs is the same. The output of graph check over the case holds the root of the case. The output of graph check with the current stream holds the location given to –current. In the machine-readable rendering, each location is in one of the string values of the JSON object. The two outputs differ, and running either command twice gives the same output twice. |
Test Specification: A reader with no usable repository cannot be judged, and the reader is named. SEG-TS-182
|
The requirements and test readers name usable repositories. In one file the implementation reader names none and the file names no default repository. In another file the implementation reader names the repository ghost, which the repository map lacks. For each file, case sync and graph status exit with status 2 and their output names the reader implementations. The case is unchanged. |
Test Specification: case sync cannot judge a stream that cannot be built, or a graph that cannot be built. SEG-TS-183
|
The case is initialized. A configured producer names a requirement export that does not exist. Running case sync with it exits with status 2 and leaves every file of the case as it was. Running case sync with a current stream that holds a refines cycle does the same. |
tests/specification/test_commitment.py
Computing an edge’s hash from a fixed baseline of endpoint identifiers, edge type, and both node hashes, then independently varying each of the five inputs in turn — the source identifier, the target identifier, the edge type, the source node hash, and the target node hash — changes the resulting hash on every variation. No single input can move without the edge hash moving with it. |
Computing a design root over a fixed set of node hashes, edge tuples, and caller metadata, then reordering the node hashes and edges before recomputing, yields the same root — the canonical sort absorbs input order. Independently varying one node hash, one edge’s endpoint or type, or the metadata changes the root; no single member of the design set can move without the root moving with it. |
Computing a node hash from a fixed node type and one named content hash, then independently varying the node type, the content digest, and the content-hash field name, changes the resulting hash on every variation; and the node hash of a single content hash never equals that content hash’s own digest — the type and the name are folded in, not merely passed through. |
tests/specification/test_config_need_ids.py
Test Specification: The loader carries the list of need identifiers of the implementations block. SEG-TS-415
|
A file gives the key need-ids in the implementations block as the list IMPL-ONE, IMPL-TWO. The loaded inputs of the implementations block carry the identifiers IMPL-ONE and IMPL-TWO and no others. A file that gives the same list in another order, and one that gives an identifier twice, carry the same identifiers. A file that does not give the key loads, and its loaded inputs carry no list at all, which is not the same as an empty list. |
Test Specification: A list of need identifiers that is empty or not a list of non-empty text is refused. SEG-TS-416
|
A file gives the key need-ids in the implementations block as the empty list, as a list that holds a number, as a list that holds the empty text, as a list of one good identifier and the empty text, as a list of one good identifier and a number, as one text that is no list, as an object, as a number or as a boolean, one at a time. Loading each file raises a configuration error that names the block producer.implementations. A control that gives the list IMPL-ONE loads. |
Test Specification: A null list of need identifiers is the same as a list that is not given. SEG-TS-417
|
A file gives the key need-ids in the implementations block with no value, so that the value is null. The file loads, and its loaded inputs carry what the inputs of a file without the key carry. A control that gives the list IMPL-ONE carries that identifier. The null key does not narrow the needs: it is not read as an empty list, which would be refused. |
Test Specification: The key need-ids is refused in the requirements block and in the specifications block. SEG-TS-418
|
A file gives the key need-ids with the list IMPL-ONE in the requirements block, or in the specifications block, one at a time. The key is known only in the implementations block, so loading each file raises a configuration error that names the block that holds the key and names the key need-ids. A control that gives the same list in the implementations block loads. |
tests/specification/test_config_need_types.py
Test Specification: A configuration that names an empty list of need types is refused, naming the block. SEG-TS-325
|
A file gives the types of one reader block as an empty list. This is tried for the requirements block, the specifications block and the implementations block, one at a time. Loading the file raises a configuration error that names the block. A control that gives the list [kind] for the same block loads, and the loaded inputs carry the type kind. |
Test Specification: A configuration whose need types are not a list of text is refused, naming the block. SEG-TS-326
|
A file gives the types of one reader block as a list that holds a number, [1], or as a text that is no list, test_case. This is tried for the requirements block, the specifications block and the implementations block, one at a time. Loading each file raises a configuration error that names the block. A control that gives the list [kind] for the same block loads. |
tests/specification/test_config_path_root.py
Test Specification: The loader carries the path root of a specifications block and of an implementations block. SEG-TS-374
|
A file gives the key path-root as include/ in one block, the specifications block or the implementations block, one at a time. The loaded inputs of that block carry a path root that is the text include, with or without its trailing separator. The text is the one the file gives. It does not begin with the directory of the file, so it is not resolved against it. A file that does not give the key, one that gives it as the empty text and one that gives it as null load, and the loaded path root is then empty or none, the same in each of the three cases. |
A file gives the key path-root as a number, a list, an object or a boolean in one block, the specifications block or the implementations block, one at a time. Loading the file raises a configuration error that names the block. A control that gives the text include/ for the same block loads. |
Test Specification: A configuration whose need types hold an empty text is refused, naming the block. SEG-TS-376
|
A file gives the types of one reader block as the list that holds only the empty text, or as the list impl and the empty text. This is tried for the requirements block, the specifications block and the implementations block, one at a time. Loading each file raises a configuration error that names the block. A control that gives the list impl for the same block loads, and the loaded inputs carry the type impl. |
Test Specification: Null need types on a specifications block or an implementations block are not given. SEG-TS-377
|
A file gives the key types of one block, the specifications block or the implementations block, with no value, so that it is null. Loading the file succeeds, and the loaded inputs carry no need types: the same as the inputs loaded from a file that does not give the key. A control that gives the list impl carries the type impl. |
Test Specification: Null need types on the requirements block are refused, naming the block. SEG-TS-378
|
A file gives the key types of the requirements block with no value, so that it is null. Loading the file raises a configuration error that names the block, because the requirements block needs its types. A control that gives the list req loads. |
tests/specification/test_config_reader_shapes.py
A file whose requirements block names the parent field trace and the source directory reqs gives requirements inputs that carry the name trace. |
Test Specification: The need types of the test-case and implementation exports are carried. SEG-TS-175
|
A file names the types test_case and test_manual in its specifications block. It names the type impl in its implementations block. The loaded inputs carry each of those sets of types and no other type. |
A file names the default repository suite, and the requirements block names the repository docs. The requirements inputs carry docs. The specifications block names none, and its inputs carry no repository of their own. |
Test Specification: The Doxygen path prefix is carried for each Doxygen output, as written. SEG-TS-177
|
A file gives the prefix tree-root/ to the test output and the prefix lib-src/ to the implementation output. The loaded inputs carry each prefix as the text written, and the loader does not join either with the directory of the file. |
A file in a subdirectory gives a source map of two docnames, docs/alpha and docs/beta, to the files reqs/alpha.sdoc and reqs/beta.sdoc. The loaded inputs carry the same two docnames. Each value is the subdirectory joined with the path written, as every other relative path is. |
Loading a file whose requirements block names a source directory and a source map raises the configuration error. So does loading a file that names neither. A file that names the source directory only loads, and so does a file that names the source map only. |
tests/specification/test_config_unknown_keys.py
Test Specification: A key at the top of the file that the loader does not know is refused, naming the key. SEG-TS-419
|
A file holds the known top-level keys case and implementation, and one more key at the top: cases, implementations, Case or repository, one at a time. Of these, repository is known only inside the producer block, and Case differs from case by its capital letter. Loading each file raises a configuration error that names the key. A control without the extra key loads. |
Test Specification: A key of the producer block that the loader does not know is refused. SEG-TS-420
|
A file holds a producer block with the known keys root and repository, and one more key: roots, outputs, implementation, Repository or types, one at a time. Loading each file raises a configuration error that names the block producer and the key. A control without the extra key loads. |
Test Specification: A key of a reader block that the loader does not know is refused, naming block and key. SEG-TS-421
|
A file holds one reader block, the requirements block, the specifications block or the implementations block, with the keys that it needs to load and one more key. The extra key is either a mistyped name, such as doxygen_prefix or need_ids, or the name of a key that only another block knows, such as need-ids in the specifications block or doxygen-prefix in the requirements block. Loading each file raises a configuration error that names the block, as producer.<block>, and the key. A control without the extra key loads. |
A file holds every key that the loader knows: at the top, case, implementation, repositories, roles and producer; in producer, root, repository, and the three reader blocks; in each reader block, every key of that block, including path-root, need-ids (in the implementations block only) and either source or source-map in the requirements block. The file loads. A second file that differs in the requirements block, which holds source-map and no source, loads too. Neither load raises a configuration error. |
Test Specification: A producer block that holds the key outcomes is refused for that key, whatever it holds. SEG-TS-423
|
A file holds a producer block with the key outcomes, whose value is an empty list, a list of one run or a text, one at a time. Loading each file raises a configuration error that names the key outcomes and says that run bundles are named on the command line with –bundle. The refusal is the one the loader gave before it refused unknown keys, and it does not say that the key is unknown. |
Test Specification: A mistyped key stops a verb of the command line with exit status 2, naming the key. SEG-TS-424
|
A configuration holds an implementations block over the fixture, with the types {impl}, the prefix of its Doxygen output and the list of need identifiers I-LIB-MAX. Running the verb case sync with that file, with the list spelled need-ids, exits with status 0. The same file with the key spelled need_ids exits with status 2 and prints a message that names the key need_ids. The case holds no record after the second run. |
tests/specification/test_confirming_outcomes.py
Test Specification: An outcome is a confirming outcome only when it has both a Confirms and a Witnesses edge. SEG-TS-362
|
One leaf has an active verifies edge and an active implements edge. Three outcomes passed. The first has a Confirms edge to the test specification and a Witnesses edge to the implementation. The second has a Confirms edge and no Witnesses edge. The third has a Witnesses edge and no Confirms edge. The satisfaction evaluator sets aside the second and the third, and not the first. The leaf is satisfied. With only the second and the third outcome in the graph, the leaf is not satisfied, and both outcomes are still set aside. With only the second outcome, the leaf is not satisfied either. |
Test Specification: The gate reports each outcome that the satisfaction evaluator sets aside as information. SEG-TS-363
|
A graph holds one leaf and three passed outcomes: one with a Confirms edge and a Witnesses edge, one with a Confirms edge only, and one with a Witnesses edge only. The package gate reports exactly one finding of the condition for a discarded outcome for each of the second and the third outcome, with the outcome as its subject and the severity information. It reports no such finding for the first outcome. The set of discarded outcomes in the report holds the second and the third outcome. The report is not blocked, because the first outcome covers the leaf. |
Test Specification: With no implementation export, no outcome confirms, and each is reported once as information. SEG-TS-364
|
The producer reads the frozen evidence fixture and one run bundle, and its block names no implementation export, so no outcome has a Witnesses edge. Running proof check for the golden scope with the strong edges affirmed reports the 24 outcomes of the scope as discarded. Each of them has one finding of the condition for a discarded outcome, with severity information and the outcome as its subject. A leaf of the scope, SD-REQ-001, is a coverage gap and so is not satisfied. The same check over a producer that reads the export, in the next test, discards none. |
Test Specification: With the implementation export, every outcome of the scope confirms and none is discarded. SEG-TS-365
|
The producer reads the frozen evidence fixture, one run bundle and the implementation export, so each outcome has a Witnesses edge to the implementations of what its test verifies. Running proof check for the golden scope with the strong edges affirmed lists no discarded outcome and holds no finding of the condition for a discarded outcome. |
tests/specification/test_content_extractor.py
Test Specification: An Implementation is identified by its implementation need's identifier, verbatim. SEG-TS-022
|
Extracting from the fixture supplies exactly 12 Implementation records whose local identifiers equal, byte for byte, the ids of the implementation export’s needs, among them IMPL-safe_data_init and IMPL-SAFE_CONTAINER_DEFINE. In a copy of the export where the need IMPL-safe_data_init is renamed ZZ-init-1 and names the same symbol, the records carry ZZ-init-1 and no identifier derived from the symbol. |
Test Specification: A TestSpecification is identified by its test-case need's identifier, verbatim. SEG-TS-023
|
Extracting from the fixture supplies exactly 19 TestSpecification records whose local identifiers equal, byte for byte, the ids of the test-case export’s needs, among them TC_SAFE_DATA_INIT_AND_VERIFY. In a copy of the export where that need is renamed TC-renamed-1 and names the same test function, the records carry TC-renamed-1 and no identifier derived from the function’s name. |
Test Specification: Implements edges come from the implementation needs' satisfies links. SEG-TS-024
|
Extracting from the fixture supplies exactly the 16 (implementation need, requirement) pairs the export’s needs declare in satisfies, among them (IMPL-safe_data_update, SD-REQ-008), each an edge of kind Implements in the pending state, running from the implementation to the requirement. In a copy of the header whose @satisfies tag in the comment of safe_data_init names SD-REQ-999, and with a root holding no source at all, the edge set is unchanged. |
Extracting from the fixture supplies exactly the 24 (test-case need, requirement) pairs the export’s needs declare in verifies, among them (TC_SAFE_DATA_INIT_AND_VERIFY, SD-REQ-003), each an edge of kind Verifies in the pending state, running from the test specification to the requirement. In a copy of the test source whose @verifies tag in the comment of test_init_and_verify names SD-REQ-999, the edge set is unchanged. |
Constructing the extractor over a copy of the implementation export that adds a created stamp to its version entry, and separately over a copy of the test-case export that adds it at the top level, raises the extractor’s error before any record is supplied; constructing it over the exports as frozen, whose every timestamp field is null, does not. |
Test Specification: A node is located through the Doxygen member whose name is its symbol. SEG-TS-027
|
For each of the 12 implementations the bodyHash equals the SHA-256 of the run of lines that the location of the member named by its symbol gives (bodyfile, bodystart to bodyend, read by the test from the Doxygen output), and for each of the 19 test specifications the implHash equals the same for its test function; the 12 bodyHash digests are pairwise distinct. In a copy of the Doxygen output where only the bodyend of safe_data_init is one line smaller, the bodyHash of IMPL-safe_data_init is the digest of that shorter run and the other eleven are unchanged. |
Test Specification: An unlocatable or ambiguous symbol is an error for its node, not an omission. SEG-TS-028
|
Extracting from a copy of the implementation export in which IMPL-safe_data_init names the symbol safe_data_absent, which no member of the Doxygen output carries, raises the extractor’s error naming IMPL-safe_data_init; extracting from a copy of the Doxygen output in which a second member named safe_data_init is defined raises it likewise; extracting from the fixture as frozen supplies all 12 Implementation records. |
Test Specification: A location outside the root is an error, and the file outside is not read. SEG-TS-029
|
With a readable file x.c beside the root, in a copy of the Doxygen output where the declaration file of safe_data_init is ../x.c, and separately in one where its body file is ../x.c, extracting raises the extractor’s error naming IMPL-safe_data_init, and x.c is not opened. |
Test Specification: An Implementation's apiHash covers its declaration and the comment above it. SEG-TS-030
|
The apiHash of IMPL-safe_data_init equals the SHA-256 of lines 247 to 263 of include/safe_data/safe_data.h: from the opening of its documentation comment through the line holding the semicolon that ends the declaration. That of IMPL-safe_data_commit equals the digest of lines 378 to 399, the guard line above the opening of its comment lying outside. |
Test Specification: A macro's apiHash covers its definition head and the comment above it. SEG-TS-031
|
The apiHash of IMPL-SAFE_CONTAINER_DEFINE equals the SHA-256 of lines 477 to 498 of include/safe_data/safe_data.h, from the opening of its comment through the #define line, and that of IMPL-SAFE_SECTION equals the digest of lines 595 to 633, the guard line between its comment and its #define lying inside. |
Test Specification: An Implementation's bodyHash covers the lines its body occupies in the source. SEG-TS-032
|
The bodyHash of IMPL-safe_data_init equals the SHA-256 of lines 224 to 237 of src/safe_data.c, the run its member’s location gives, and that of IMPL-SAFE_CONTAINER_DEFINE equals the digest of lines 498 to 506 of include/safe_data/safe_data.h. |
Test Specification: A TestSpecification's specHash covers the documentation comment above the test. SEG-TS-033
|
The specHash of TC_SAFE_DATA_INIT_AND_VERIFY equals the SHA-256 of lines 33 to 43 of tests/safe_data/src/main.c: the comment carrying its @testid, @verifies and @active tags, from its opening to its closing line, and not the ZTEST line that follows. |
Test Specification: A TestSpecification's implHash covers the lines the test's body occupies. SEG-TS-034
|
The implHash of TC_SAFE_DATA_INIT_AND_VERIFY equals the SHA-256 of lines 44 to 48 of tests/safe_data/src/main.c, from the ZTEST line through the closing brace, the run its member’s location gives. |
The apiHash of IMPL-safe_data_init equals the SHA-256 of lines 247 to 263 of the header including the line feed that ends line 263, and equals neither the digest of that run without its final line feed nor that of the run starting one byte after its first line’s start. In a copy of src/safe_data.c whose every line ends in CR LF, the bodyHash of IMPL-safe_data_init equals the digest of lines 224 to 237 with their CR LF terminators. |
Test Specification: A missing documentation comment is an error for its node, never a hash over another comment. SEG-TS-036
|
In a copy of the header where the lines of the comment above safe_data_init are blank, with every line number unchanged, extracting raises the extractor’s error naming IMPL-safe_data_init. |
The apiHash of IMPL-safe_data_init, IMPL-SAFE_CONTAINER_DEFINE and IMPL-SAFE_SECTION and the specHash of TC_SAFE_DATA_INIT_AND_VERIFY each equal the SHA-256 of source lines and none equals the SHA-256 of the UTF-8 text of that member’s brief description in the Doxygen output, raw or with its whitespace collapsed. In a copy of the Doxygen output where the text of every description element is replaced by one word, every hash of every record is unchanged. |
Test Specification: An Implementation's api anchor names the declaration file and the symbol. SEG-TS-038
|
For each of the 12 implementations the apiHash anchor names the repository “toolbox”, a name and not a path, the file holding the symbol’s declaration as its member’s location gives it (include/safe_data/safe_data.h for safe_data_init), and the locator symbol:<symbol>#api, for safe_data_init symbol:safe_data_init#api. |
For each of the 12 implementations the bodyHash anchor names the file holding the symbol’s body as its member’s location gives it (src/safe_data.c for safe_data_init, include/safe_data/safe_data.h for the macro SAFE_CONTAINER_DEFINE) and the locator symbol:<symbol>#body. |
Test Specification: A TestSpecification's spec anchor names the test file and the function. SEG-TS-040
|
For each of the 19 test specifications the specHash anchor names the repository “toolbox”, the file tests/safe_data/src/main.c, and the locator symbol:<function>#spec, for test_init_and_verify symbol:test_init_and_verify#spec. |
Test Specification: A TestSpecification's impl anchor names the test file and the function. SEG-TS-041
|
For each of the 19 test specifications the implHash anchor names the file tests/safe_data/src/main.c and the locator symbol:<function>#impl, for test_init_and_verify symbol:test_init_and_verify#impl. |
Test Specification: A location whose source line lacks its symbol is an error for its node. SEG-TS-042
|
In a copy of the Doxygen output where the declaration line of safe_data_init is that of safe_data_verify, and separately in one where its body start and end are those of safe_data_verify, extracting raises the extractor’s error naming IMPL-safe_data_init, although each run of lines is well formed. |
Loading a configuration file in a subdirectory whose producer block names specifications with the export “needs/test-specification/needs.json” and the Doxygen output “xml/dox-testspec” yields specification inputs whose export and Doxygen output are that subdirectory joined with each relative path. |
Loading a configuration file in a subdirectory whose producer block names implementations with the export “needs/api-traceability/needs.json” and the Doxygen output “xml/dox-api” yields implementation inputs whose export and Doxygen output are that subdirectory joined with each relative path. |
tests/specification/test_content_extractor_need_ids.py
Test Specification: With a list of need identifiers and no need types, a need is read when it is listed. SEG-TS-425
|
The implementation export holds I-ONE, I-TWO and I-THREE of the type impl and I-OTHER of the type other, each over a macro that the Doxygen output locates. The list I-ONE, I-OTHER is configured and no need types are. The extractor supplies a record for I-ONE and for I-OTHER, and for no other need. Each of the two has one Implements edge, and no other need has one. The type of a listed need does not matter when no types are configured. |
Test Specification: With need types and no list of need identifiers, a need is read when its type is one of them. SEG-TS-426
|
The implementation export holds I-ONE, I-TWO and I-THREE of the type impl and I-OTHER of the type other. The types {impl} are configured and no list is. The extractor supplies a record for each of the three needs of the type impl and none for I-OTHER. With the types {other} it supplies one for I-OTHER and for no other need. With the types {impl, other} it supplies all four. |
Test Specification: With need types and a list of need identifiers, a need is read when it is listed and typed. SEG-TS-427
|
The implementation export holds I-ONE, I-TWO and I-THREE of the type impl and I-OTHER of the type other. The types {impl} and the list I-ONE, I-TWO are configured. The extractor supplies a record for I-ONE and I-TWO. It supplies none for I-THREE, which has the type but is not listed, and none for I-OTHER, which has neither. With the types {impl, other} and the list I-ONE, I-OTHER it supplies I-ONE and I-OTHER, and not I-TWO. |
Test Specification: While neither need types nor a list of need identifiers is configured, every need is read. SEG-TS-428
|
The implementation export holds I-ONE, I-TWO and I-THREE of the type impl and I-OTHER of the type other. The configuration names no need types and no list. The extractor supplies a record for each of the four needs, and one Implements edge from each. A configuration whose list is null, which is the same as no list, supplies the same four. |
Test Specification: A listed need identifier that names no need of the export is refused, naming it. SEG-TS-429
|
The implementation export holds I-ONE, I-TWO, I-THREE and I-OTHER. The list I-ONE, I-GONE is configured. Reading the export raises one error from the extractor. The error names I-GONE and does not name I-ONE. A control that lists I-ONE and I-TWO is read without an error. |
Test Specification: A listed need identifier whose need the configured types do not admit is refused. SEG-TS-430
|
The implementation export holds I-ONE and I-TWO of the type impl, and I-OTHER of the type other. The types {impl} and the list I-ONE, I-OTHER are configured. Reading the export raises one error from the extractor. The error names I-OTHER and does not name I-ONE. A control that configures the types {impl, other} with the same list is read without an error, and the extractor supplies I-ONE and I-OTHER. |
Test Specification: Every listed need identifier that names no admitted need is named in one error. SEG-TS-431
|
The implementation export holds I-ONE, I-TWO and I-THREE of the type impl and I-OTHER of the type other. The types {impl} and the list I-ONE, I-GONE-A, I-OTHER, I-GONE-B are configured: two identifiers that name no need and one that names a need of another type. Reading the export raises one error from the extractor. The error names I-GONE-A, I-OTHER and I-GONE-B, and does not name I-ONE. It names each of the three once. |
Test Specification: A need that is not in the list of need identifiers is not refused, whatever its fault. SEG-TS-432
|
The implementation export holds I-ONE and I-TWO, which the Doxygen output locates, and needs of the type impl that the extractor cannot use. In the first export they are I-NO-TITLE, which has no title, and I-BAD-LINKS, whose links are a text and not a list. In the second export the need is I-NO-MACRO, whose macro is in no member of the output. Without a list, reading each export raises an error that names its faulty needs. With the list I-ONE, I-TWO the extractor supplies a record for the two needs and raises no error, for each export. With a list that holds I-ONE and one faulty need it raises an error that names that need, and does not name the other faulty need of the export: a need that is listed is still refused for its fault. |
tests/specification/test_content_extractor_no_body.py
Test Specification: A member whose body ends at -1 is an error for its node, and the node is not hashed. SEG-TS-361
|
In a copy of the Doxygen output of the implementations where the location of safe_data_init gives the end of the body as -1, extracting raises the extractor’s error. The message names IMP-safe_data_init, the need whose member records no body, and the stream gives no record for it. The same holds for a copy where both the start and the end of the body are -1. In a copy of the Doxygen output of the test specifications where the location of the test function of TC_SAFE_DATA_INIT_AND_VERIFY gives the end of the body as -1, extracting raises the error and the message names that need. The extraction over the fixture as frozen supplies all 12 Implementation records, so the rule does not refuse a member that records a body. |
tests/specification/test_content_extractor_path_root.py
Test Specification: A path root is put in front of the path the Doxygen output names, and the file is read there. SEG-TS-379
|
The Doxygen output names the macro QUEUE_MAKE in the file zephyr/queue.h. The repository holds the header at include/zephyr/queue.h and holds no file at zephyr/queue.h. No path prefix is configured. The header has a documentation comment with a satisfies tag, then a macro of five lines with continuation lines. With the path root include/ configured, the extractor supplies the record of the need I-QUEUE. Its apiHash equals the SHA-256 of the lines from the opener of the comment to the first line of the macro. Its bodyHash equals the SHA-256 of the five lines of the macro, to the last continuation line. |
Test Specification: With a prefix and a path root, the prefix is removed first and the root is put in front. SEG-TS-380
|
The Doxygen output names the macro QUEUE_MAKE in the file ext/zephyr/queue.h. The prefix ext/ and the path root include/ are configured. The repository holds the header at include/zephyr/queue.h. It also holds a decoy header, with other text, at each of three paths: zephyr/queue.h, ext/zephyr/queue.h and include/ext/zephyr/queue.h. The extractor supplies the record of I-QUEUE, and its apiHash and bodyHash equal the SHA-256 of the lines of the header at include/zephyr/queue.h, found as in the first specification. |
Test Specification: A path root with a trailing separator and one without it give the same record. SEG-TS-381
|
The Doxygen output names the macro QUEUE_MAKE in the file zephyr/queue.h, and the repository holds the header at include/zephyr/queue.h. The extractor is run twice, once with the path root include/ and once with the path root include. Each run supplies the record of I-QUEUE. The two records have the same digests and the same anchors, and the path of each anchor is include/zephyr/queue.h, with no doubled separator. |
Test Specification: An empty path root and a null path root are the same as no path root. SEG-TS-382
|
The Doxygen output names the macro QUEUE_MAKE in the file include/zephyr/queue.h, and the repository holds the header at that path. With no path root given, the extractor supplies the record of I-QUEUE. With the path root given as the empty text, or as null, it supplies a record with the same digests and the same anchors, and the path of each anchor is include/zephyr/queue.h. No separator is put in front of the path. |
Test Specification: A path root that is absolute or leads outside the repository is an error for the node. SEG-TS-383
|
The repository is a directory that holds a header at zephyr/queue.h. Next to it is a second directory, outside the repository, that holds a header at the same path. The Doxygen output names the macro QUEUE_MAKE in the file zephyr/queue.h. With no path root the extractor supplies the record of I-QUEUE. The path root then names the second directory in one of three ways: as a relative path that begins with .., as a relative path that begins inside the repository and climbs out with .., or as an absolute path. In each case taking the records raises a source error that names the need I-QUEUE. The header in the second directory is not opened. |
Test Specification: The directory of the test module is compared with the path after the root is put in front. SEG-TS-384
|
The test source of the repository is in three files: tests/mod_a/src/main.c, tests/mod_ab/src/main.c and tests/mod_b/src/main.c. Each has the test test_shared with its own comment. The Doxygen output names the test in the files mod_a/src/main.c, mod_ab/src/main.c and mod_b/src/main.c. The need T-SHARED names the test module tests/mod_a. With the path root tests/ the extractor supplies the record of T-SHARED, and its specHash and implHash equal the SHA-256 of the comment and of the test in tests/mod_a/src/main.c. With no path root the extractor raises a source error that names T-SHARED, because none of the three paths lies within tests/mod_a. |
Test Specification: A path root on the specifications block locates a test by the joined path. SEG-TS-385
|
The Doxygen output names the test test_shared in the file mod_a/src/main.c, and the repository holds the test source at tests/mod_a/src/main.c only. The need T-SHARED names no test module. With the path root tests/ configured on the specifications block, the extractor supplies the record of T-SHARED. Its specHash equals the SHA-256 of the comment of the test, from its opener to its closer, and its implHash equals the SHA-256 of the lines of the test, from the line that names it to its closing brace. |
With the path root include/ and the prefix ext/, the Doxygen output names the macro QUEUE_MAKE in ext/zephyr/queue.h, and the repository named lib holds the header at include/zephyr/queue.h. Both anchors of I-QUEUE, the one of the apiHash and the one of the bodyHash, name the repository lib and the path include/zephyr/queue.h. With the path root tests/, the test test_shared that the Doxygen output names in mod_a/src/main.c gives anchors for specHash and implHash that name the repository suite and the path tests/mod_a/src/main.c. |
The repository holds the header at include/zephyr/queue.h and a decoy at zephyr/queue.h. The path root include/ is configured. With the prefix ext/ and the Doxygen output naming the macro in zephyr/queue.h, which does not begin with the prefix, taking the records raises a source error that names I-QUEUE and the prefix. With the prefix ext and the path ext/zephyr/queue.h, whose remainder begins with a separator, the error names I-QUEUE and the path. With the whole path as the prefix, which leaves nothing, the error names I-QUEUE. In each case the root is not put in front of the unusable remainder. |
The Doxygen output names the macro QUEUE_MAKE in the file zephyr/queue.h, and the repository holds the header at include/zephyr/queue.h only. With the path root include/ configured, the extractor supplies the record of I-QUEUE. Asking the content extractor, and asking the composed producer that holds it, for the bytes behind apiHash gives the lines of the header from the opener of the comment to the first line of the macro. Asking for the bytes behind bodyHash gives the five lines of the macro. Each answer equals the lines that the test cuts from its own header, and its SHA-256 is the digest in the anchor of the record. |
tests/specification/test_content_extractor_prefix_and_module.py
Test Specification: A path whose remainder after the prefix is empty or begins with a separator is an error. SEG-TS-327
|
The Doxygen tree names test_alpha in the file inc/tests/mod_a/src/main.c. With the prefix inc/ configured, the extractor locates T-ALPHA. With the prefix inc configured, the remainder is /tests/mod_a/src/main.c. With the whole path inc/tests/mod_a/src/main.c as the prefix, the remainder is empty. In each of those two cases taking the records raises a source error that names T-ALPHA, the path inc/tests/mod_a/src/main.c and the prefix. The file tests/mod_a/src/main.c of the repository is not opened. |
Test Specification: case sync names every node whose path does not fit its prefix, with the path and the prefix. SEG-TS-328
|
The configuration gives the test stream the prefix inc and the implementation stream the prefix libsrc, each with no trailing separator. The paths of the Doxygen trees are inc/tests/mod_a/src/main.c, inc/tests/mod_b/src/main.c and libsrc/include/lib.h. Running case sync exits with status 2. Its output names the four needs T-ALPHA, T-GAMMA, I-LIB-MAX and I-LIB-MIN, each on a line of its own. The line of each holds the path of its node and the prefix of its stream. A control with the prefixes inc/ and libsrc/ exits with status 0. |
Test Specification: A test module that is absent, null or empty text names no test module. SEG-TS-329
|
The Doxygen tree names test_alpha once and test_shared in three directories. For each of the three forms, a need with no test_module key, a need whose test_module is null and a need whose test_module is the empty text, the extractor locates the need that names test_alpha, with no narrowing. It refuses the need that names test_shared with an error that names that need, and the error is the same for the three forms. |
Test Specification: A test module that is present and is neither null nor text is an error for that need. SEG-TS-330
|
The Doxygen tree names test_alpha in one file. The test-case export holds T-BAD, a need that names test_alpha and whose test_module is a number, a list, an object or a boolean, and T-GOOD, a need whose module is the text tests/mod_b. For each value, the extractor supplies the record of T-GOOD and then raises a source error that names T-BAD and does not name T-GOOD. A control whose test_module is the text tests/mod_a supplies a record for T-BAD. |
Test Specification: A shared symbol with a prefix that leaves no relative path gets the prefix error. SEG-TS-334
|
The Doxygen tree names test_shared in three files, one in each of the directories tests/mod_a, tests/mod_ab and tests/mod_b. The need T-SHARED names the test module tests/mod_a. With the prefix tests configured, the remainder of each path begins with a separator. With the whole path tests/mod_a/src/main.c as the prefix, the remainder of that path is empty. In each case taking the records raises a source error that names T-SHARED, a path of the tree and the prefix. The error does not say how many members lie within the test module. |
tests/specification/test_content_repository_reads.py
Test Specification: case sync performs no write in the content repository, not even to its index. SEG-TS-216
|
A content repository has an out-of-date index and a change that is not committed. Running case sync over it exits with status 0. Every file under the .git directory of the repository is the same after the command. The same holds for every file of the working tree. |
Test Specification: edge affirm performs no write in the content repository, not even to its index. SEG-TS-217
|
A content repository has an out-of-date index and a change that is not committed. The change is in a file that the edge does not anchor. Running edge affirm over it exits with status 0. Every file under the .git directory of the repository is the same after the command. The same holds for every file of the working tree. |
tests/specification/test_dangling_edge.py
Test Specification: The graph builder reports a never-affirmed edge its record reports as broken as broken. SEG-TS-104
|
The builder gets two requirements and a Refines edge between them. The record of the edge carries no hash and claims the state broken. The built graph reports the edge as broken, and it still carries no hash. |
Test Specification: The graph builder reports every other never-affirmed edge as pending. SEG-TS-105
|
The builder gets three requirements and three edges. A Refines edge carries no hash and claims the state directly outdated. A second Refines edge is pending. A third carries the hash it was affirmed against and the state active. The built graph reports the first two as pending, and the third as active with its hash. |
Test Specification: A never-affirmed edge to an absent node is broken in the graph built from the derivation. SEG-TS-106
|
The current records hold one requirement and a Refines edge from it to a requirement that the records lack. The recorded records are empty. The suspect detector derives the edge and the builder builds the derived records. The built graph reports the edge as broken. |
Test Specification: A never-affirmed strong edge to an absent node is a broken row and gives exit status 1. SEG-TS-107
|
The current stream is a store with a Verifies edge and an Implements edge between present nodes, and a second Implements edge from an implementation the store does not hold. Nothing is affirmed. Graph status lists the second Implements edge as broken, lists the other two edges as pending, and exits with status 1. The same store without the second Implements edge exits with status 0 and lists two pending edges. |
Test Specification: An affirmed strong edge whose endpoint leaves the stream is a broken row and gives exit 1. SEG-TS-108
|
One Verifies edge is affirmed over a store. The store is then changed so that it no longer holds the requirement the edge ends at. Graph status lists the Verifies edge as broken and exits with status 1. |
Test Specification: A Confirms edge to an absent specification gives exit status 1 and one dangling count. SEG-TS-109
|
The current stream is a store with one outcome recorded at the revision of the implementation repository, its Confirms and Witnesses edges, and a second Confirms edge to a specification the store does not hold. Graph status runs with that revision. It exits with status 1. Its evidence section counts one outcome at the current revision, no outcome at another revision and one dangling edge. |
Test Specification: Never-affirmed strong edges between present nodes are pending rows and give exit status 0. SEG-TS-110
|
The current stream is a store with an outcome and its evidence edges, one Verifies edge and one Implements edge, all endpoints present, nothing affirmed, and a clean implementation repository that the configuration names. Graph status lists both strong edges as pending and exits with status 0. |
Test Specification: The gate lists a broken strong edge as not ready, with the detail broken. SEG-TS-111
|
The built graph holds two requirements and a Refines edge between them that carries no hash and whose record reports the state broken. The package gate lists that edge among its unready edges, in the state broken, and gives its finding the detail broken. The report is blocked. |
Test Specification: Case sync stores a dangling edge as broken, and as pending once the node returns. SEG-TS-112
|
The current stream is a store whose Implements edge starts at an implementation the store does not hold. Case sync exits with status 0 and the stored edge document holds that edge in the state broken, with no hash. The store then gains that implementation. The next case sync exits with status 0 and the stored edge is pending, with no hash. |
tests/specification/test_drift.py
Deriving edge states from a current record stream whose declared source or target node is absent from that stream reports the edge as broken — for a strong edge whose recorded affirmation no longer has both endpoints present, and equally for an edge of a kind that carries no suspicion, such as an outcome’s confirms edge to a specification that is not in the current stream. Absence of an endpoint takes precedence over every other derived state. |
tests/specification/test_edge_affirm_unreadable_repository.py
Test Specification: edge affirm refuses, naming the repository and the reason, when it cannot read it. SEG-TS-345
|
The content repository of both endpoints cannot be read. It is made so in five ways, and each is a variant: its objects are removed, a stand-in git fails every call, the configuration maps it to a directory that holds no repository, the configuration maps it to a path that does not exist, and no git is on the path. No revision is given, so edge affirm has to discover one. Running edge affirm for the edge from REQ-C to REQ-A exits with status 2. A line of the output names the repository as the configuration names it, and gives a reason. For the path that does not exist, the reason says that it does not exist. The output holds no traceback. |
Test Specification: A refused edge affirm writes no review event, no edge record and no node record. SEG-TS-346
|
A case is empty, and the content repository cannot be read, in each of the five ways of the variants. Running edge affirm for the edge from REQ-C to REQ-A, with no revision given, exits with status 2. Every file of the case has the same bytes after the command as before it, and the case holds no review event, no edge record and no node record. |
Test Specification: When one endpoint is readable and one is not, edge affirm refuses and writes nothing. SEG-TS-347
|
An implementation is in one repository and the requirement that it implements is in another. A first edge of the same kind is affirmed, so the run shows that the two repositories can be read. Then the repository of the requirement is made unreadable, or the repository of the implementation is. The repository is made unreadable by the removal of its objects, or by a stand-in git that fails every call that runs in it and passes every other. Running edge affirm for the second edge, with no revision given, exits with status 2 and names the repository that cannot be read. Every file of the case has the same bytes after the command as before it. The other repository, the readable one, is not named as the one that cannot be read. |
Test Specification: A given revision is neither discovered nor checked, so edge affirm goes on. SEG-TS-348
|
The content repository cannot be read, in each of the five ways of the variants, and a case holds no extraction revision. A revision is given on the command line. Running edge affirm for the edge from REQ-C to REQ-A exits with status 0 and prints the affirmed line for the edge. It writes the node records of the two endpoints, and neither carries an extraction revision. The output has a line that names the repository and gives the number 2, the count of node records written without a revision. The output holds no traceback. |
A case sync records the revision of the repository for every node. Then the repository is made unreadable, in each of the five ways of the variants. The content of the endpoints does not change. A revision is given on the command line. Running edge affirm for the edge from REQ-C to REQ-A exits with status 0. The node record of each endpoint keeps the revision that case sync recorded. The output has no line that reports node records without a revision for the repository. |
tests/specification/test_edge_provenance_exit_and_writes.py
Test Specification: The exit status of edge show is the same for every history that the case can have. SEG-TS-283
|
The same affirmed edge is shown in eight cases. The first has no history, as a control. The others have a commit that holds the event, a commit with a bad signature, an event that no commit holds, a case copied with no history, a case inside another repository, a repository that cannot be read, and a shallow history. In every case, edge show gives the same exit status as in the control, in text and in JSON. The status of the control is 0. |
Test Specification: edge show performs no version-control write against the case, not even to its index. SEG-TS-284
|
A case is a git repository with one committed event. The recorded modification time of every file of the case is changed, so the index of the repository is out of date. A plain git status writes a new index in such a repository. edge show runs, in text and in JSON, and exits with status 0. Every file under the .git directory of the case is the same after the command. The same holds for every file of the working tree. The last step is a control: a plain git status in the same repository changes a file under .git. |
Test Specification: edge show performs no version-control write against a case that is a worktree. SEG-TS-285
|
A case is a worktree of another repository, on a branch of its own, with one committed event. The recorded modification time of every file of the case is changed, so its index is out of date. The index of a worktree is under the .git directory of the first repository. edge show runs, in text and in JSON, and exits with status 0. Every file under the .git directory of the first repository is the same after the command. The same holds for every file of the worktree. The last step is a control: a plain git status in the worktree changes a file under that .git directory. |
tests/specification/test_edge_provenance_identity.py
Test Specification: edge show reports the committer of the recording commit, with its date, as the identity. SEG-TS-260
|
A case is a git repository. One commit adds the review event of an edge. Its committer is Alice, with one commit date. Its author is Bob, with an earlier date. edge show exits with status 0, in text and in JSON. The JSON committer holds the name and the e-mail address of Alice, and a date that is the commit date as one instant. The text line “recorded in the case history as” holds the same name, the same e-mail address and the same instant. That line does not hold the e-mail address of Bob. |
Test Specification: edge show reports the identifier and the subject line of the recording commit. SEG-TS-261
|
A case is a git repository. One commit adds the review event of an edge. Its message has a subject line, an empty line and a body of two lines. edge show exits with status 0. The JSON commit is the identifier that git gives for the commit, and the JSON subject is the subject line alone. The text gives the first seven characters of the identifier at least. It gives the subject line in the same line as the identifier. It does not give the body. |
Test Specification: edge show reports who made the last affirmation of each affirmed edge in a selection. SEG-TS-262
|
Two edges are affirmed. Alice adds the event of the first edge in one commit. Bob adds the event of the second edge in a later commit. edge show runs with a selector of the edge kind and with no other option. It exits with status 0. Both edges are in the report. In text and in JSON, each edge names the commit that added its own event, and the committer of that commit, with the commit date. Neither edge names the commit or the committer of the other. |
Test Specification: edge show reports the author and the author date when the author is not the committer. SEG-TS-263
|
One commit adds the review event of an edge. Its committer is Alice, with one date. Its author is Bob, with an earlier date. edge show exits with status 0. The JSON author holds the name and the e-mail address of Bob and the author date as one instant. The JSON committer is Alice. The text has one line that starts with “author:”. That line holds the name, the e-mail address and the author date of Bob. The line “recorded in the case history as” still holds Alice. |
Test Specification: edge show reports no author when the author of the recording commit is its committer. SEG-TS-264
|
One commit adds the review event of an edge. The author and the committer are the same person, with the same date. edge show exits with status 0. The JSON has the author key, and its value is null. The JSON committer is that person. The text has no line that starts with “author:”. The line “recorded in the case history as” holds that person. |
Test Specification: edge show reports each Signed-off-by line of the recording commit as written, in order. SEG-TS-265
|
The message of the commit ends with two Signed-off-by lines. The first names Zed, and the second names Amy, so the order is not the order of the alphabet. edge show exits with status 0. The JSON list has two entries. They are the two values as written, with or without the word Signed-off-by, in the order of the message. The text has the two values in the same order, in lines that start with “signed-off-by:”. |
Test Specification: edge show reports no Signed-off-by line when the message of the recording commit has none. SEG-TS-266
|
The message of the commit has a subject line and a body, and no Signed-off-by line. edge show exits with status 0. The JSON list of sign-offs is empty. The text has no line that starts with “signed-off-by:”. |
Test Specification: edge show reports the committer as the commit records it and applies no mailmap. SEG-TS-286
|
The case holds a .mailmap file, in the commit that adds the event. The file maps the e-mail address of Alice to another name and another address. The committer of the commit is Alice. edge show exits with status 0. The JSON committer has the name and the e-mail address that the commit records. The mapped name and the mapped address are not in the text or in the JSON. |
Test Specification: edge show reports no author when the author is the committer, even if the dates differ. SEG-TS-291
|
One commit adds the review event of an edge. The author and the committer are the same person, by name and e-mail address. The author date is earlier than the commit date, as after an amend or a rebase. edge show exits with status 0. The JSON has the author key, and its value is null. The JSON committer is that person, with the commit date. The text has no line that starts with “author:”. |
tests/specification/test_edge_provenance_no_answer.py
Test Specification: edge show reports an event that no commit holds as not committed, with no identity or time. SEG-TS-276
|
A case is a git repository. Its only commit, by Carol, holds no review event. Then edge affirm records an event, and nobody commits it. edge show exits with status 0. The JSON status is notCommitted. The JSON commit, subject, committer and author are null. The text line “recorded in the case history” says not committed and holds no date. Neither the e-mail address of Carol nor her commit is anywhere in the output. |
Test Specification: edge show reports a last affirmation that no commit holds as not committed. SEG-TS-277
|
An edge is affirmed, and a commit by Alice adds its event. The text of the target requirement then changes, and the change is committed in the content repository. The edge is affirmed again, and nobody commits the second event. edge show exits with status 0. The JSON status is notCommitted, with no commit, no committer and no author. The text says not committed. The commit and the e-mail address of Alice are not in the output. |
Test Specification: edge show reports the history as not available for a case that has no repository. SEG-TS-278
|
A case with one committed event is copied to another directory with no .git directory. edge show for the copy exits with status 0. The JSON status is unavailable, with no commit, committer and author. The text line “recorded in the case history” says not available and holds no date. Alice, the committer of the original, is not in the output. A control run on the original case names her. |
Test Specification: edge show reports the history as not available for a case inside another repository. SEG-TS-279
|
The files of a case with one event are added, in one commit by Dan, to another repository. The case is a directory of that repository, and its root is not the top level of the repository. edge show for the case exits with status 0. The JSON status is unavailable, with no commit, committer and author. The text says not available. The commit of the enclosing repository and the e-mail address of Dan are not in the output. |
Test Specification: edge show reports the history as not available when git cannot read the history. SEG-TS-280
|
A case is a git repository, and a commit by Alice adds the event of an edge. The test deletes the object file of that commit from the repository. edge show exits with status 0, and it prints no traceback. The JSON status is unavailable, with no commit, committer and author. The text says not available. The e-mail address of Alice and the commit are not in the output. |
Test Specification: edge show reads the history of a case that is a worktree of another repository. SEG-TS-281
|
A repository has one commit by Dan. A worktree of it, on a branch of its own, is the case. A commit by Carol starts the case. A commit by Alice adds the event of an edge. The top level of the worktree is the root of the case. edge show exits with status 0. The JSON status is found, with the commit of the worktree and Alice as the committer. The commit of the first repository and Dan are not in the output. |
Test Specification: edge show reports that the history is shallow, beside the identity it reports. SEG-TS-282
|
A case has three commits. Carol starts it. Alice adds the event of the first edge. Bob adds the event of the second edge. A clone of depth one holds only the commit by Bob. edge show on the clone exits with status 0. For each edge, the JSON status is found, with the commit by Bob and Bob as the committer, and the JSON shallow is true. In the text, the block of each edge holds the word shallow. A control run on the full history gives the commit by Alice for the first edge, with shallow false, and no block holds the word shallow. |
Test Specification: edge show reports the provenance of the last affirmation of an edge that is not active. SEG-TS-288
|
An edge is affirmed, and one commit by Alice adds its event. The text of the target requirement then changes, so the edge is no longer active. edge show exits with status 0. The state of the edge in the report is not active. The JSON status is found, with the commit and Alice as the committer, and the text names the same commit and Alice. |
Test Specification: edge show reports an event as not committed when the case repository has no commit. SEG-TS-289
|
The case is a git repository with no commit. Then edge affirm records an event. edge show exits with status 0, and it prints no traceback. The JSON status is notCommitted, with no commit, subject, committer and author. The text line “recorded in the case history” says not committed and holds no date. |
Test Specification: edge show gives a null signature and a null shallow flag when no commit is reported. SEG-TS-290
|
Two cases are built. In the first, the event is in the working tree and in no commit. In the second, the case was copied with no history. For each, edge show exits with status 0. The JSON status is notCommitted in the first case and unavailable in the second. In both, the JSON signature is null, and the JSON shallow flag is null. Both keys are present. |
tests/specification/test_edge_provenance_recording_commit.py
Test Specification: edge show names the earliest commit that holds the event, not the one that made the file. SEG-TS-267
|
An early commit by Alice creates the file of review events, with the event of a first edge. A later commit by Bob adds the event of a second edge to the file. edge show for the second edge names the later commit and Bob, in text and in JSON. It does not name the early commit or Alice. edge show for the first edge names the early commit and Alice. |
Test Specification: edge show names one commit as the recording commit of each event that the commit adds. SEG-TS-268
|
A commit by Carol starts the case. One run of edge affirm then records two events, for two edges. One commit by Alice adds both. edge show for each edge names that commit and Alice, in text and in JSON. It does not name the commit by Carol. |
Test Specification: edge show matches the whole identifier of an event, not one that begins the same way. SEG-TS-269
|
The file of review events holds two events. The identifier of one ends with /event/1 and the identifier of the other ends with /event/10, so the first is the beginning of the second. The store gives each event a number of six digits, so the test writes both identifiers into the file as text. An early commit by Alice adds the event /event/10, of the first edge. A later commit by Bob adds the event /event/1, of the second edge. edge show for the second edge names the later commit and Bob. edge show for the first edge names the early commit and Alice. |
Test Specification: edge show does not name a commit only because its reason quotes the identifier of the event. SEG-TS-270
|
The reason of the first event is free text, and it ends with the identifier of the second event. The second event does not exist yet. An early commit by Alice adds the first event. A later commit by Bob adds the second event. edge show for the second edge names the later commit and Bob. In text and in JSON it does not name the early commit. Only an event holds the identifier of the event as its own identifier. A reason that quotes the identifier does not hold the event. |
Test Specification: edge show names the commit of the last affirmation of an edge that was affirmed twice. SEG-TS-271
|
An edge is affirmed, and one commit by Alice adds its event. The text of the target requirement then changes in the content repository, and the change is committed there. The edge is affirmed again, and a second commit by Bob adds the second event. edge show names the second commit and Bob, in text and in JSON. It does not name the first commit or Alice. |
Test Specification: edge show names the commit as it stands after an amend, with the new identifier. SEG-TS-272
|
One commit by Alice adds the event of an edge. edge show names that commit. Dan then amends the commit with a later commit date. The identifier of the commit changes. A second run of edge show names the new identifier and Dan as the committer, in text and in JSON. It does not name the old identifier. |
Test Specification: edge show names the earliest commit for an event that was removed and added again. SEG-TS-287
|
A commit by Alice adds the event of an edge. A later commit by Bob removes the event from the file. A third commit by Dan puts the event back, with the same text. The file is then the same as after the first commit. edge show names the first commit and Alice, in text and in JSON. It does not name the commit by Bob or the commit by Dan. |
tests/specification/test_edge_provenance_signature.py
Test Specification: edge show reports that the recording commit is not signed, with the status none. SEG-TS-273
|
One commit adds the review event of an edge, and it carries no signature. edge show exits with status 0. The JSON signature is the word none. The text has one line that starts with “signature:”, and it says none. |
Test Specification: edge show reports the status of a signature as git gives it, for each status. SEG-TS-274
|
A stand-in for the gpg program lets git make and check a signature of each kind. For each of seven letters of git, a case is built. One signed commit adds the review event of an edge. The letters are G, B, U, X, Y, R and E. edge show exits with status 0. The JSON signature and the text line that starts with “signature:” give one word. G is good. B is bad. U is unknownValidity. X and Y are expired. R is revoked. E is cannotCheck. The text gives that word, with or without spaces, and no other word of the set. |
Test Specification: edge show presents the identity as what the case history records, and never as verified. SEG-TS-275
|
Three cases are built. In the first, a commit with a good signature adds the event. In the second, the event is in the working tree and in no commit. In the third, the case has no history. For each, edge show exits with status 0. The text has one line with the words “recorded in the case history”. In the first case, that line has the words “recorded in the case history as”. The JSON has the key recordedInCaseHistory. Nothing that edge show prints, in text or in JSON, holds the words “affirmed by”, “verified” or “authenticated”. |
tests/specification/test_edge_selection_evidence_edges.py
Test Specification: Edge show with a subtree selection for a requirement lists no edge of an evidence kind. SEG-TS-366
|
A store holds the shape of the earlier specifications. It also holds an outcome, a Confirms edge from the outcome to a test specification, a Witnesses edge from it to an implementation, and a Calls edge between two implementations. It holds three more edges of those kinds that have a requirement of the subtree at one end: a Confirms edge to the leaf, a Witnesses edge to the middle requirement and a Calls edge to the leaf. Edge show with a subtree selection for the top, for the middle requirement and for the leaf each exits with status 0. The listed edges are the Refines, Verifies and Implements edges inside the subtree, as for the store without the additions, and no listed edge has the kind Confirms, Witnesses or Calls. |
Test Specification: Case remove with a subtree selection for a requirement leaves an edge of another kind. SEG-TS-367
|
The case holds the records of the store of the earlier specifications, written by case sync, and so holds the Calls edge that has the leaf at one end and the Calls edge between two implementations. Case remove with a subtree selection for the top exits with status 0. The edge records that the case holds afterwards are those held before, less the seven edges inside the subtree. Both Calls edges are still held. |
Test Specification: The selection function takes no Confirms, Witnesses, Calls or Excuses edge by subtree. SEG-TS-368
|
A graph holds a requirement, a requirement that refines it, a test specification, two implementations and an outcome. It holds one Refines edge, one Verifies edge and one Implements edge inside the subtree of the first requirement. It also holds, for each of the kinds Confirms, Witnesses, Calls and Excuses, one edge that has a requirement of the subtree as its source and one that has it as its target. Selecting by the subtree of the first requirement returns the three edges of the three kinds, and no other. Selecting by kind and subtree together for each of the four other kinds returns no edge. |
Test Specification: Edge show with a subtree selection for a node that is not a requirement lists no edge. SEG-TS-369
|
The store holds a test specification, an implementation and an outcome, each with edges of an evidence kind, and a requirement that is the far end of a refinement edge only, which no node of the store carries. Edge show with a subtree selection for the test specification, for the implementation, for the outcome, for a name that no node carries, and for the name that is the far end of the broken refinement edge each lists no edge and exits with status 2. |
Test Specification: Edge affirm with a subtree selection for a node that is not a requirement fails. SEG-TS-370
|
The same store, and an empty case. Edge affirm with a revision, a synthetic role and a subtree selection for the test specification, for the implementation, for the outcome and for the far end of the broken refinement edge each exits with status 2. The case holds no review event after any of them. |
Test Specification: Case remove with a subtree selection for a node that is not a requirement fails. SEG-TS-371
|
The case holds the records of the store, written by case sync. It holds a Calls edge between two implementations, and the broken refinement edge. Case remove with a subtree selection for the implementation, for the test specification, for the outcome and for the far end of the broken refinement edge each exits with status 2. The case holds the same edge records after each of them. |
Test Specification: The selection function takes no edge by the subtree of an outcome or any other node. SEG-TS-372
|
A graph holds a requirement and the nodes of the other kinds: a test specification, two implementations and an outcome. It holds a Confirms edge from the outcome to the test specification, a Witnesses edge from the outcome to an implementation, a Calls edge between the implementations, and the Verifies and Implements edges of the requirement. Selecting by the subtree of the outcome, of the test specification, of each implementation, and of a name that no node carries returns no edge. |
Test Specification: A subtree selection for a requirement that nothing refines still takes its two edges. SEG-TS-373
|
The store holds a requirement that no requirement refines and that refines no requirement, one test specification that verifies it and one implementation that implements it, beside the outcome and the edges of the evidence kinds. Edge show with a subtree selection for that requirement exits with status 0 and lists the Verifies edge and the Implements edge. Case remove with the same selection exits with status 0 and removes those two edges and no other. |
tests/specification/test_edge_selection_subtree.py
Test Specification: A subtree selection reaches the requirement and every requirement that refines it. SEG-TS-335
|
A store holds a chain of refinement, a requirement with a parent, and a requirement with two parents, one of them outside. Running edge show with a subtree selection for the top of the chain exits with status 0. The requirements that the listed edges name are the top, the requirement that refines it, the requirement that refines that one in turn, and the requirement with two parents. They are no others: not the parent of the top, not the second parent. The same holds for a subtree selection for the middle of the chain, which names the middle and the requirement below it. |
Test Specification: A sibling, and a requirement that refines only a requirement outside, add no edge. SEG-TS-336
|
A store holds a sibling of the top, which refines the parent of the top, and a requirement that refines only a requirement outside the subtree. A test specification and an implementation relate to that requirement alone. Running edge show with a subtree selection for the top exits with status 0. No listed edge has the sibling, the requirement that refines only a requirement outside, or the test specification or implementation that relate to that requirement alone, as an endpoint. |
Test Specification: Edge show lists a Refines edge in a subtree only when both of its ends are in it. SEG-TS-337
|
A store holds a top with a parent, a chain of refinement below the top, and a requirement that refines the top and a second requirement outside the subtree. Running edge show with a subtree selection for the top exits with status 0. The listed Refines edges are the three between two members: the middle refines the top, the leaf refines the middle, and the requirement with two parents refines the top. The edge from the top to its parent is not listed. The edge from the requirement with two parents to its second parent is not listed. |
Test Specification: Edge affirm with a subtree selection affirms only the edges inside the subtree. SEG-TS-338
|
A store holds the shape of the earlier specifications, and the case is empty. Running edge affirm with a subtree selection for the top, a revision and a role exits with status 0. The case then holds a review event for each of the seven edges inside the subtree, and for no other edge. It holds no review event for the edge from the top to its parent, nor for the edge from a member to a second parent outside. |
Test Specification: Case remove with a subtree selection removes only the edges inside the subtree. SEG-TS-339
|
A case holds the records of the shape of the earlier specifications, written by case sync. Running case remove with a subtree selection for the top exits with status 0. The edge records that the case holds afterwards are all the edges of the store, less the seven edges inside the subtree. The edge from the top to its parent is still held, and so is the edge from a member to a second parent outside. |
Test Specification: A Verifies or Implements edge is selected by the requirement that it names. SEG-TS-340
|
One test specification verifies a requirement inside the subtree and one outside, and one implementation implements a requirement inside and one outside. A selection by subtree for the top, with edge show, edge affirm and case remove in turn, takes the Verifies and Implements edges that name a requirement inside, and no other Verifies or Implements edge. The test specification and the implementation that relate to both sides give one selected edge and one edge that is not selected. A test specification and an implementation of the subtree that name a requirement outside are not selected either. |
Test Specification: A leaf requirement selects the Verifies and Implements edges it names, and no Refines edge. SEG-TS-341
|
A leaf requirement refines one requirement, has one test specification that verifies it and one implementation that implements it. Running edge show with a subtree selection for the leaf exits with status 0. The listed edges are the Verifies edge and the Implements edge of the leaf. The Refines edge from the leaf to its parent is not listed. |
Test Specification: A subtree selection for a requirement that has a parent leaves out its edge to the parent. SEG-TS-342
|
The middle requirement of a chain refines the top, and the leaf refines the middle. In turn, edge show, edge affirm and case remove run with a subtree selection for the middle requirement, each over its own store. Each exits with status 0. Each takes four edges: the edge from the leaf to the middle, the Verifies edge and the Implements edge of the leaf, and the Implements edge of the middle. None takes the edge from the middle requirement to the top. The edge from the middle to the top is the one the selection leaves out, whichever verb runs. |
Test Specification: A subtree selection for a requirement the store does not hold matches no edge. SEG-TS-343
|
The same store, and a requirement name that no node carries. Running edge show, edge affirm and case remove in turn with a subtree selection for that name each exit with status 2, a request that could not be judged. Edge affirm records no review event. Case remove removes no edge record. |
Test Specification: The edges of a subtree selection are the edges that a proof scope of that requirement holds. SEG-TS-344
|
The store holds only strong edges, and the nodes that they join. Edge show runs with a subtree selection for the top, and again for the middle of the chain. The proof generator collects the scope of the same requirement over the graph of the same store, and it holds the edges that join two members of the scope. For each of the two requirements, the edges that edge show lists are the edges of that scope, no more and no fewer. This is the reason a selection takes only the edges inside: it answers what a proof of the requirement would hold. |
tests/specification/test_edge_show_unreadable_repository.py
The edge from REQ-B to REQ-A is affirmed. Then the content repository cannot be read, in each of the five ways of the variants. Running edge show with the verbose rendering exits with status 0 and writes no traceback. For each endpoint, one line has the word before-content, the name of the endpoint, the words not available, the name of the repository as the configuration names it, and a reason. For the path that does not exist, the reason says that it does not exist. |
Test Specification: edge show shows the content of the readable endpoint, and says the other is not available. SEG-TS-351
|
An implementation is in one repository and the requirement that it implements is in another. The edge between them is affirmed. Then the repository of the requirement cannot be read, or the repository of the implementation cannot be. It is made unreadable by the removal of its objects, or by a stand-in git that fails every call that runs in it. Running edge show with the verbose rendering exits with status 0. The endpoint in the readable repository shows the content that it had at its affirmation. The other endpoint has a line that says that its before-content is not available and names its repository. |
Test Specification: edge show gives the same exit status whether or not it can read the before-content. SEG-TS-352
|
The edge from REQ-B to REQ-A is affirmed. Then the content of REQ-A changes in the working tree, so the edge is suspect. A first run of edge show with the verbose rendering reads the repository, and gives a status. Then the content repository cannot be read, in each of the five ways of the variants. Running edge show again with the verbose rendering gives the same status as the first run. So does running it with a subtree selection for REQ-A. |
Test Specification: The report of edge show has a null content and an error for an unreadable end. SEG-TS-353
|
The edge from REQ-B to REQ-A is affirmed. Then the content repository cannot be read, in each of the five ways of the variants. Running edge show with the verbose rendering and the machine-readable report exits with status 0. For each endpoint, the entry of the before-content keeps the revision that the affirmation recorded, has a null content, and has an error key. The error is a text that holds the name of the repository as the configuration names it and a reason. For the path that does not exist, the reason says that it does not exist. |
An implementation is in one repository and the requirement that it implements is in another, and the edge between them is affirmed. Then one of the two repositories cannot be read, in the two ways of the variants. Running edge show with the verbose rendering and the machine-readable report exits with status 0. The entry of the readable end holds its revision and its content as text, and it has no error, or an error that is null. The entry of the other end has a null content and an error that names its repository. |
Test Specification: The text of edge show prints one line of a fixed form for an endpoint it cannot read. SEG-TS-355
|
The edge from REQ-B to REQ-A is affirmed. Then the content repository cannot be read, in each of the five ways of the variants. Running edge show with the verbose rendering exits with status 0. For each endpoint, one line reads before-content, an at sign, the endpoint, the word revision with the revision of the affirmation in parentheses, a colon, the words not available, a colon, the repository, a colon and the reason. The repository is named as the configuration names it. The reason is not empty. |
The edge from REQ-B to REQ-A is affirmed, and a stand-in git logs each call. Running edge show without the verbose rendering exits with status 0, and the log holds no call of the subcommand show. The status and the text are kept. Then the content repository cannot be read, in each of the five ways of the variants. Running edge show without the verbose rendering again gives the same status and the same text, and no traceback. |
tests/specification/test_every_misshapen_need.py
Test Specification: The content extractor names every misshapen need of an export in one error. SEG-TS-389
|
An export of the content extractor holds five needs, in the stream of the implementations or in the stream of the test cases, one stream at a time. One need lacks a text field the extractor reads. One need declares an id other than its key. One need has a link field that is a text and not a list. The other two are good. Building the extractor raises one error. The error has one line for each of the three bad needs. Each line holds the key of the need and a word that tells why: the name of the missing field, the id that was declared, or the name of the link field. No line names a good need. A control export that holds only one of the three bad needs, with the two good ones, is refused with an error that names that need. |
Test Specification: The requirements reader names every misshapen need of the requirement export in one error. SEG-TS-390
|
The requirement export holds five needs of the configured type. One lacks a text field the reader reads. One declares an id other than its key. One has a parent-link field that is a text and not a list. The other two are good. Building the reader raises one error. The error has one line for each of the three bad needs. Each line holds the key of the need and a word that tells why: the name of the missing field, the id that was declared, or the name of the link field. No line names a good need. A control export that holds only one of the three bad needs, with the two good ones, is refused with an error that names that need. |
Test Specification: The outcome extractor names every misshapen need of an export in one error. SEG-TS-391
|
An export of the outcome extractor holds five needs, in the test-case export or in the implementation export, one export at a time, with a good other export and a run bundle that is accepted. One need lacks a text field the extractor reads. One need declares an id other than its key. One need has a link field that is a text and not a list. The other two are good. Building the extractor raises one error. The error has one line for each of the three bad needs. Each line holds the key of the need and a word that tells why: the name of the missing field, the id that was declared, or the name of the link field. No line names a good need. A control export that holds only one of the three bad needs, with the two good ones, is refused with an error that names that need. |
Test Specification: The error for misshapen needs of an export of the content extractor starts with a count. SEG-TS-392
|
An export of the content extractor, in the stream of the implementations or in the stream of the test cases, one at a time, holds three misshapen needs and two good ones. The first line of the error holds the number 3 and no other number, once the path of the export is cut out of it, and it names no need. Each of the lines after it names one bad need, so the error has four lines. With only one bad need, the first line holds the number 1 and one line follows. |
Test Specification: The error for misshapen needs of the requirement export starts with a count line. SEG-TS-393
|
The requirement export holds three misshapen needs and two good ones. The first line of the error holds the number 3 and no other number, once the path of the export is cut out of it, and it names no need. Each of the lines after it names one bad need, so the error has four lines. With only one bad need, the first line holds the number 1 and one line follows. |
Test Specification: The error for misshapen needs of an export of the outcome extractor starts with a count. SEG-TS-394
|
The test-case export, or the implementation export, one at a time, holds three misshapen needs and two good ones. The first line of the error holds the number 3 and no other number, once the path of the export is cut out of it, and it names no need. Each of the lines after it names one bad need, so the error has four lines. With only one bad need, the first line holds the number 1 and one line follows. |
Test Specification: The misshapen needs of an export of the content extractor are listed in export order. SEG-TS-395
|
An export of the content extractor, in the stream of the implementations or in the stream of the test cases, one at a time, holds three misshapen needs and two good ones. The keys of the bad needs are not in alphabetical order in the export. The lines of the error name the bad needs in the order of the export. Building the extractor a second time over the same export gives an error with the same text. |
Test Specification: The misshapen needs of the requirement export are listed in the order of the export. SEG-TS-396
|
The requirement export holds three misshapen needs and two good ones. The keys of the bad needs are not in alphabetical order in the export. The lines of the error name the bad needs in the order of the export. Building the reader a second time over the same export gives an error with the same text. |
Test Specification: The misshapen needs of an export of the outcome extractor are listed in export order. SEG-TS-397
|
The test-case export, or the implementation export, one at a time, holds three misshapen needs and two good ones. The keys of the bad needs are not in alphabetical order in the export. The lines of the error name the bad needs in the order of the export. Building the extractor a second time over the same export gives an error with the same text. |
Test Specification: Case sync prints one refusal that names every misshapen need and writes nothing. SEG-TS-398
|
The implementation export of the configured producer holds three misshapen needs and two good ones. Case sync over an initialized case exits with status 2. Its output names each of the three bad needs with a line of its own, and names no good need. The files of the case are the same after the command as before it. With the export mended, the same command exits with status 0. |
tests/specification/test_every_unmapped_result.py
Test Specification: Every unmapped or ambiguous result of a run artifact is named in one error. SEG-TS-399
|
A run artifact holds one board with five results: PUT_GET, which maps to one need, three results that map to no need, and one result of a test that two needs share. The extractor raises one error. It has one line for each of the four bad results. Each line holds the identifier of the result. The line of an unmapped result says that it maps to no test-case need. The line of the ambiguous result names both needs. The error does not name the result that maps to one need. A control artifact that holds only one unmapped result, with the good one, is refused with an error that names it. |
Test Specification: The error for unmapped or ambiguous results of a run starts with a count line. SEG-TS-400
|
A run artifact holds two boards. The first board holds 29 unmapped results and one ambiguous result. The second board holds the same 29 unmapped results and the same ambiguous result again, and each board also holds one good result. So the artifact holds 60 bad results, which are 58 unmapped results and two ambiguous ones. The first line of the error holds the number 60 and no other number, once the paths of the bundle and the artifact are cut out of it, and it names no result. The error has one more line for each bad result, so 61 lines. With a single bad result the first line holds the number 1 and one line follows. |
Test Specification: The bad results of a run are listed in the order of the run artifact, and the text is stable. SEG-TS-401
|
A run artifact holds two boards. The identifiers of the bad results are not in alphabetical order in the artifact: three unmapped results and one ambiguous result on the first board, then two unmapped results on the second board. The lines of the error name the six results in the order of the artifact. Building the extractor a second time over the same artifact gives an error with the same text. |
Test Specification: A result with the status not run is refused for its status, with no result left out. SEG-TS-402
|
A run artifact holds the result PUT_GET with the status not run, which maps to one need, and after it three results that map to no need. The extractor raises an error that names the result PUT_GET and says that its status has no counterpart in the closed set. This is a refusal of its own: it does not name the three unmapped results, which come after it in the artifact. An artifact whose only bad result has the status not run is refused the same way. |
Test Specification: Every result with the status not run is named in one refusal for its status. SEG-TS-412
|
A run artifact holds two boards. The first board holds, in this order, an unmapped result, a result with the status not run, a second unmapped result and a second result with the status not run. The second board holds a result with the status not run, then an unmapped result. The extractor raises one error. It has one line for each of the three results with the status not run, and each line holds the identifier of the result and the status. It names none of the unmapped results, even those that come before a result with the status not run. A second artifact holds one board with two unmapped results and then one result with the status not run. It is refused for the status, and its error names none of the unmapped results. |
Test Specification: Each line of the error for unmapped results holds the board and the scenario. SEG-TS-413
|
A run artifact holds two boards that run the scenario scn.alpha, on the platforms native_sim and qemu_x86, and a third board that runs the scenario scn.beta on native_sim. Each board holds the same unmapped result, whose identifier does not begin with the name of any scenario. The extractor raises one error with one line for each of the three results. The line of each result holds its platform and its scenario. The three lines are different from one another. The error has a count line first, and that line names no platform and no scenario. |
tests/specification/test_extraction_revision_affirm.py
Test Specification: edge affirm records the discovered revision in the node record of each endpoint. SEG-TS-211
|
A case is empty. A repository is configured and holds the committed content of both endpoints. Running edge affirm exits with status 0. The case then holds the node records of the two endpoints and no other. Each of the two records carries the revision of the repository, as git gives it, for that repository. |
Test Specification: edge affirm keeps a held revision while the content hashes are unchanged. SEG-TS-212
|
A case sync records the revision of the repository. Then a commit changes a file that no node anchors, so the repository is at a new revision and the content hashes are the same. Running edge affirm exits with status 0. The node record of each endpoint keeps the first revision. It does not carry the current revision of the repository, which is not the first one. |
Test Specification: edge affirm drops a held revision when the changed content is not committed. SEG-TS-213
|
A case sync records the revision of the repository. Then the content of one endpoint changes in the working tree and is not committed. A revision is given on the command line, so that edge affirm does not refuse. Running edge affirm exits with status 0. The node record of the changed endpoint holds the new content hash and carries no revision for the repository. The given revision is in no node record. |
Test Specification: edge affirm never records a revision that the operator gives as an extraction revision. SEG-TS-214
|
A revision that is not the revision of the repository is given on the command line. In a first case, the repository is configured and committed. Running edge affirm exits with status 0. The node records of the endpoints carry the revision of the repository, not the given one. In a second case, the configuration names no repository for the anchors. Running edge affirm exits with status 0, and the node records carry no revision at all. |
Test Specification: edge affirm reports each repository and the number of records written without a revision. SEG-TS-218
|
The content of both endpoints changes in the working tree and is not committed. A revision is given on the command line, so that edge affirm does not refuse. A case is empty. Running edge affirm exits with status 0. Its output has a line that names the repository and gives the number 2. |
tests/specification/test_extraction_revision_store.py
The store writes one node record of each kind that a case holds: a requirement, an implementation, a test specification and a waiver. Each record carries a map from a repository name to a revision. The map has one repository for one record and two repositories for the others. A new store over the same root reads each record back with the same map. The stored document of each record holds the map as a JSON object under one key, from repository name to revision. |
Test Specification: A node record without an extraction revision is read back as written. SEG-TS-196
|
The store writes one node record of each kind that a case holds, with no extraction revision. A new store over the same root reads each record back equal to the record written. The record carries no revision. The stored document of each record has no extraction revision field. Writing the same records again changes no byte of the case. |
Test Specification: The extraction revisions never enter a node hash, an edge hash or the design root. SEG-TS-197
|
Two cases hold the same nodes and edges. In the second case every node record also carries a map of extraction revisions. Each node hash, derived from the node kind and the content hashes, is the same in both cases. The design root over all node hashes and edge tuples is the same. An edge is affirmed in the first case. A current stream whose node records carry the map derives that edge as active, with the edge hash it was affirmed against. |
Test Specification: Every node schema declares the extraction revisions as an optional property. SEG-TS-198
|
Each of the five packaged node schemas, for a requirement, an implementation, a test specification, a test outcome and a waiver, declares the extraction revision key as a property. The property is an object. No schema lists it as required, so a record without it stays valid. |
Test Specification: The store refuses an extraction revision that is not 40 or 64 lowercase hex characters. SEG-TS-220
|
The store is given a node record whose map holds one of these values: the word XYZ, 40 uppercase hex characters, 39 lowercase hex characters, and 41 lowercase hex characters. Each write raises a store error. No file of the case changes. A value of 40 and a value of 64 lowercase hex characters are accepted. |
Test Specification: The store persists a node record with no extraction revision with no such field. SEG-TS-221
|
The store writes a node record with an empty map, and a node record with no map. The stored document of each has no extraction revision key. A record is written with a map and then written again with an empty map. The stored document of that record then has no extraction revision key, and not an empty object. |
tests/specification/test_extraction_revision_sync.py
Test Specification: case sync records the discovered revision for a node the case does not hold. SEG-TS-199
|
A case is empty. A repository is configured and holds the committed content of three requirements. Running case sync exits with status 0. Each node record in the case carries the revision of the repository, as git gives it, for that repository. |
Test Specification: case sync replaces a held revision with the discovered one when the hash changes. SEG-TS-200
|
A first case sync records the revision of the repository. Then the content of one requirement changes and the change is committed, so the repository is at a new revision. Running case sync again changes the content hash of that node record. It also changes the revision of the node record to the new revision of the repository. |
Test Specification: case sync adds the discovered revision to a node record that holds none. SEG-TS-201
|
The case holds three node records written with no extraction revision. The content has not changed, so running case sync writes the same content hashes. Each node record then carries the revision of the repository, as git gives it, for that repository. |
Test Specification: case sync keeps a held revision while the content hashes are unchanged. SEG-TS-202
|
A first case sync records the revision of the repository. Then a commit changes a file that no node anchors, so the repository is at a new revision and the content hashes are the same. Running case sync again keeps, in each node record, the first revision. It does not record the current revision of the repository, which is not the first one. |
Test Specification: case sync keeps a held revision when no repository is configured any more. SEG-TS-203
|
A first case sync records the revision of the repository. Then the configuration names no repository for the anchors, and the content is unchanged. Running case sync again exits with status 0. Each node record keeps the revision it held. |
Test Specification: case sync drops a held revision when the changed content is not committed. SEG-TS-204
|
A first case sync records the revision of the repository. Then the content of one requirement changes in the working tree and is not committed. Running case sync again exits with status 0. It writes the new content hash for that node record. The node record carries no revision for the repository. The first revision is not kept. |
Test Specification: case sync drops a held revision when the repository is not configured. SEG-TS-205
|
A first case sync records the revision of the repository. Then the content of one requirement changes and is committed, and the configuration names no repository for the anchors. Running case sync again exits with status 0, and does not refuse. It writes the new content hash for that node record. The node record carries no revision for the repository. |
Test Specification: case sync records no revision for a node whose anchored path the repository lacks. SEG-TS-206
|
Two repositories are configured and committed, and neither has a change that is not committed. The requirement reader anchors each requirement at a source file that the first repository does not hold at its revision. The implementation reader anchors at files that the second repository holds. Running case sync exits with status 0. Each requirement record carries no revision. Each implementation record carries the revision of the second repository. |
Test Specification: case sync reports each repository and the number of records written without a revision. SEG-TS-207
|
A first case sync, with every anchored file committed, prints no line that names the repository. Then the content of two of the three requirements changes in the working tree and is not committed. Running case sync again exits with status 0. Its output has a line that names the repository and gives the number 2, which is the number of node records written without a revision for it. |
Test Specification: case sync reports the count of records without a revision for each repository. SEG-TS-208
|
Two repositories are configured. The requirement reader anchors its three records at paths that the first repository does not hold. The implementation reader anchors at paths that the second repository holds. Running case sync exits with status 0. Its output has a line that names the first repository and gives the number 3. No line names the second repository. |
Test Specification: case sync records one revision for each repository that the anchors name. SEG-TS-209
|
Two repositories are configured, committed and unchanged. The two have different revisions. The requirement reader anchors at source files in the first repository. The implementation reader anchors at files in the second repository. Running case sync exits with status 0. Each requirement record carries the revision of the first repository for that repository only. Each implementation record carries the revision of the second repository for that repository only. |
Test Specification: case sync records a revision for each repository that one node's anchors name. SEG-TS-210
|
Two repositories are configured and committed. One implementation anchors its api hash in the first repository and its body hash in the second. Another implementation anchors the same way, but the file it names in the second repository has a change that is not committed. Running case sync exits with status 0. The first node record carries the revision of each repository. The second node record carries the revision of the first repository only. |
Test Specification: case sync writes nothing when the schema copy of the case predates the field. SEG-TS-215
|
The schema copy of a case has the extraction revision property removed from every node schema. Running case sync, which records revisions, exits with status 2 and changes no file of the case. After case refresh, the same case sync exits with status 0 and records the revision of the repository in each node record. |
Test Specification: case sync drops a held revision when the configured directory is not a repository. SEG-TS-219
|
A first case sync records the revision of the repository. Then the content of one requirement changes and is committed. The configuration now maps the repository name to a directory that is not a git repository. Running case sync again exits with status 0, and does not refuse. It writes the new content hash for that node record. The node record carries no revision for the repository. |
Test Specification: case sync keeps no held revision for a repository that the anchors no longer name. SEG-TS-222
|
Two repositories are configured and committed. A first case sync records, in each requirement record, the revision of the first repository. Then the configuration moves the requirement reader to a new repository name that maps to the same directory. The paths and the content hashes are the same. Running case sync again exits with status 0. Each requirement record carries the revision for the new name only. It carries none for the old name. |
tests/specification/test_extractor_comment_search.py
Test Specification: A test with no documentation comment above it is an error for its node. SEG-TS-172
|
In the test source, six tests have a documentation comment above them. One line of a stopping kind stands between the comment and the test. The kinds are a code line, an #include line and a #define line. They are also a line comment, a line that starts with three slashes, and a code line that ends in a block comment. A seventh test has code directly above it. An eighth test stands on the first line of its file. For each of the eight, taking the records raises a source error that names the test’s need. No hash is supplied. |
Test Specification: Plain comments, blank lines and conditional lines alone do not make a comment. SEG-TS-173
|
In the test source, one test has only a plain block comment above it. One has a banner comment that starts with three stars. One has a blank line and an #if line. Code lies above each of them. For each test, taking the records raises a source error that names the test’s need. No hash is supplied. |
Test Specification: A specHash steps over blank lines and conditional lines above the test. SEG-TS-190
|
In the test source, eight tests have a documentation comment above them. Lines of one kind stand between the comment and the test. The first test has one blank line, and the second has two. The third has a blank line and an #if line. The others have one line each: #ifdef, #ifndef, #elif, #else or #endif. For each test the specHash equals the SHA-256 of the comment, from its opening line to its closing line. The lines in between are not in the run. |
In the test source, four tests have a documentation comment above them. Lines of one kind stand between the comment and the test. The first has a plain block comment of one line. The second has one of three lines. The third has one of one line behind white space. The fourth has a plain comment, a blank line, an #if line and a blank line, in that order. For each test the specHash equals the SHA-256 of the documentation comment, from its opening line to its closing line. No byte of the plain comment is in the run. |
In a copy of the test source, the blank line below the comment of test_blank becomes an #ifndef line. The plain comment below the comment of test_plain reads another text. The specHash of both tests equals the digest of the comment, as before. In a second copy, the word Direct in the comment of test_direct reads DIRECT. Its specHash changes. It equals the SHA-256 of the changed comment. |
Test Specification: The search for the comment above an Implementation allows guard lines only. SEG-TS-193
|
In the header, the comment of IMP_DIRECT is directly above its define line. One #if line stands between the comment and the define line of IMP_GUARD. The apiHash of each equals the SHA-256 of the lines from the comment opening to the define line. Three macros have another kind of line between the comment and the define line. IMP_BLANK has a blank line. IMP_ELSE has an #else line. IMP_PLAIN has a plain comment. Each of the three is an error that names its need. |
tests/specification/test_extractor_error_report.py
Test Specification: Every node that cannot be supplied is reported in one error, each with its reason. SEG-TS-171
|
The test stream holds one good need, one need whose symbol no Doxygen member carries, and one whose test has no documentation comment. The implementation stream holds one good need and one whose macro has a blank line between its comment and its define line. Taking the records raises one source error. Its message names the three bad needs, each with its symbol and a reason, and the two reasons of the test stream differ. It does not name the two good needs. |
tests/specification/test_extractor_types_modules_and_prefix.py
The test-case export holds needs of the type test_case. It also holds T-OTHER, a need of the type test_other, whose symbol the Doxygen tree locates. The types {test_case} are configured. The extractor supplies records for T-ALPHA and T-GAMMA and for no other need. It supplies no Verifies edge from T-OTHER. |
No type is configured. The test-case export holds T-ALPHA of the type test_case and T-GAMMA of the type test_other, both with a symbol the Doxygen tree locates. The extractor supplies a record for each of them. |
The types {test_case} are configured. The test-case export holds a need of the type test_procedure that has no symbol field, and one of the type test_other with an empty symbol. Building the extractor and taking every record raises no error, and the records are those of the needs of the type test_case. |
The Doxygen tree holds three members named test_shared, in tests/mod_a, tests/mod_ab and tests/mod_b. The need T-SHARED-A names the test module tests/mod_a. The need T-SHARED-B names tests/mod_b. Each need is located through the member inside its module. Its specHash equals the SHA-256 of the comment above that member, and its anchor names that member’s file. The directory tests/mod_ab is not inside tests/mod_a. A second tree holds the name only in tests/mod_ab and tests/mod_b. There, a need that names tests/mod_a is an error, because no member lies inside it. |
The Doxygen tree for tests names the file suite/tests/mod_a/src/main.c, and the tree for implementations names lib-src/include/lib.h. The prefixes suite/ and lib-src/ are configured, one for each tree. The specHash of T-ALPHA equals the SHA-256 of the comment above test_alpha in tests/mod_a/src/main.c of the repository suite. The apiHash of I-LIB-MAX equals the digest of the comment and the define line of LIB_MAX in include/lib.h of the repository lib. |
Test Specification: A path that does not begin with the prefix is an error, and the file is not read. SEG-TS-169
|
The prefix suite/ is configured. In a copy of the Doxygen tree, the path of test_alpha begins with other/. That text has as many characters as the prefix. A readable file stands at other/tests/mod_a/src/main.c in the repository. Taking the records raises a source error that names T-ALPHA. The file under other/ is not opened. The file tests/mod_a/src/main.c is not opened either. Removing the first six characters reaches it. |
The readers name three repositories: docs, suite and lib, and no default repository is configured. Each anchor of T-ALPHA names the repository suite and the path tests/mod_a/src/main.c, with no prefix in it. Each anchor of I-LIB-MAX names the repository lib and the path include/lib.h. Each anchor of R-1 names the repository docs. |
Test Specification: After the choice by test module, anything but exactly one member is an error. SEG-TS-188
|
Three needs name the symbol test_shared, and each extraction is refused with an error that names the need. T-TWICE names the module tests/mod_a, where the Doxygen tree holds two members of that name. T-NO-MODULE names no module, and the tree holds three members. T-ELSEWHERE names the module tests/other, which holds none. |
Test Specification: A path outside the repository configured for the node's stream is an error. SEG-TS-189
|
The default repository is docs and the test stream names the repository suite. In a copy of the Doxygen tree the path of test_alpha is ../docs/reqs/alpha.sdoc, a readable file in the repository docs and outside the repository suite. Taking the records raises a source error that names T-ALPHA, and the file is not opened. |
Test Specification: The test module is compared with the file's path after the prefix is removed. SEG-TS-194
|
The Doxygen tree names three members test_shared, in the files suite/tests/mod_a/src/main.c, suite/tests/mod_ab/src/main.c and suite/tests/mod_b/src/main.c. The prefix suite/ is configured. The need T-SHARED-A names the test module tests/mod_a. It is located through the member in mod_a: its specHash equals the SHA-256 of the comment above that member, and its anchor names tests/mod_a/src/main.c. A need that names the module suite/tests/mod_a is an error, because no path inside the repository lies in it. |
tests/specification/test_gate_skip_rule.py
One leaf has one test specification. One outcome confirms the specification and witnesses the implementation. Its result is failed, and no waiver excuses it. The package gate reports one finding with the outcome as its subject. The severity of that finding blocks. The report is blocked. The same holds when the result is error. |
One leaf has one test specification. One outcome confirms the specification and witnesses the implementation. Its result is failed. A waiver that has not expired excuses the outcome. The package gate reports one finding with the outcome as its subject. The severity of that finding is information. The report is not blocked. The same holds when the result is error. |
Two graphs are the same leaf with one outcome that confirms the specification, witnesses the implementation and was skipped. In the second graph a waiver that has not expired excuses that outcome. The package gate gives an equal report for both graphs. The report holds no excused finding. It still lists the skipped outcome. The leaf has the same verdict in both graphs. |
One leaf has one test specification. Two outcomes confirm the specification and witness the implementation. One passed and one was skipped. The report lists the skipped outcome and not the passed one. The report holds one finding, with the skipped outcome as its subject and the skipped-outcome condition. The severity of that finding is information. No failing outcome is listed. The report is not blocked. |
One leaf carries an active verifies edge and an active implements edge. Its one test specification has two confirming outcomes. One passed and one was skipped. The satisfaction evaluator reports the leaf as satisfied. |
One leaf carries an active verifies edge and an active implements edge. Its one test specification has one confirming outcome, and that outcome was skipped. The satisfaction evaluator reports the leaf as not satisfied. The package gate reports the leaf as a coverage gap. The report is blocked, and that coverage gap is the only finding that blocks. |
One leaf carries an active verifies edge and an active implements edge. Its one test specification has one confirming outcome. That outcome failed, and a waiver that has not expired excuses it. The satisfaction evaluator reports the leaf as satisfied. |
One leaf has one test specification. One outcome passed at the current revision. Another outcome was skipped, and it was recorded at a different revision. The package gate reports the second outcome as stale, with one finding of information severity. The report does not list it among the skipped outcomes. The report is not blocked. |
tests/specification/test_gate_unreadable_repository.py
A configuration names the implementation repository, and the stream holds a test outcome. A control run of each of the three verbs, while the repository is healthy, ends with a status other than 2. Then the repository cannot be read, in each of the five ways of the variants. Running proof check, proof generate and graph status, with no revision given, each exits with status 2. A line of the output names the repository as the configuration names it, and gives a reason. For the path that does not exist, the reason says that it does not exist. The output holds no traceback. |
Test Specification: proof generate writes no evidence package when the implementation repository cannot be read. SEG-TS-358
|
A configuration names the implementation repository, and the case has no package. The repository cannot be read, in each of the five ways of the variants. Running proof generate with no revision given exits with status 2. The proofs directory of the case holds no file afterwards, and every file of the case has the same bytes as before the command. |
A stand-in git logs each call. Graph status over a stream with no test outcome exits with status 0, and the log holds no call. Graph status over a stream with an outcome, with a revision given, exits with a status other than 2, and the log holds no call. Proof verify over a package that the generator wrote makes no call either. The log is empty after all three. |
Test Specification: proof check, proof generate and graph status run git without the seven variables. SEG-TS-360
|
A configuration names the implementation repository, and the stream holds a test outcome. A second repository exists. All seven variables GIT_DIR, GIT_WORK_TREE, GIT_INDEX_FILE, GIT_OBJECT_DIRECTORY, GIT_ALTERNATE_OBJECT_DIRECTORIES, GIT_COMMON_DIR and GIT_NAMESPACE are set, and each names the second repository. A stand-in git logs the environment of each call. Running proof check, proof generate and graph status with no revision given leaves a log with calls for the revision and the status. In no call is one of the seven variables present. |
tests/specification/test_graph.py
Building a graph whose refines edges contain a self-loop, and separately one whose refines edges form a longer cycle, is refused with a graph-level error naming a cycle in both cases. Building a graph whose refines edges converge without looping — two children refining into one shared ancestor — succeeds; a diamond is not mistaken for a cycle. |
Building a graph from an edge record that carries no hash it was affirmed against, but whose recorded state claims otherwise, yields a built edge in the pending state — the state the record itself claims is disregarded in favour of the absence of an affirmed hash. |
Building a graph from a node record declaring a kind the taxonomy provider does not declare is refused, and building a graph from an edge record declaring such a kind is refused likewise — an undeclared kind stops the build whether it appears on a node or an edge. |
tests/specification/test_manual_configuration_examples.py
The manual shows its configuration file in a YAML code block at least once, in the installation tutorial. The scan reads every page of the manual and of the requirement specification and finds that block among the examples. A scan that finds none would let the next test pass for the wrong reason. |
Test Specification: Every YAML configuration example that a page shows is accepted by the loader. SEG-TS-443
|
A page of the manual or of the requirement specification shows a configuration in a YAML code block. The block is written to a file, as it stands, and the loader reads the file. Loading raises no configuration error, so that no example holds a key that the loader refuses. This is tried for each YAML block of each page, one at a time. |
tests/specification/test_need_ids_confirming_outcomes.py
Test Specification: With a list of need identifiers, an outcome with no listed implementation is set aside. SEG-TS-441
|
The implementation export of the frozen evidence fixture has one more need, a copy of the need that implements SD-REQ-005 under another identifier, so that SD-REQ-005 has two implementation needs. The list holds every need of the fixture except the copy and except the need that alone implements SD-REQ-004, SD-REQ-009 and SD-REQ-010. The producer reads the fixture and one run bundle. Running proof check for the golden scope with the strong edges affirmed gives these results. The outcomes of the tests that verify only those three requirements are listed as discarded outcomes, and each has one finding of the condition for a discarded outcome, with severity information and the outcome as its subject. No outcome of the test that verifies SD-REQ-005 is discarded, so that outcome confirms through the listed need. No outcome of the test that verifies SD-REQ-003 and SD-REQ-009 is discarded: it confirms through the listed need of SD-REQ-003. The three requirements that lost their only need are coverage gaps, and SD-REQ-005 is not. |
tests/specification/test_node_comparison.py
Test Specification: The suspect detector reports a hash as matching when both digests are equal. SEG-TS-227
|
The case holds a requirement record whose contentHash covers one text. The current stream holds a record of the same node whose contentHash covers the same text, but with an anchor that names another path. The comparison has one item, for contentHash. Its status is matching. It carries both anchors. |
Test Specification: The suspect detector reports a hash as differing when the two digests are not equal. SEG-TS-228
|
The case holds a requirement record whose contentHash covers one text. The current stream holds a record of the same node whose contentHash covers another text. The comparison has one item, for contentHash. Its status is differing. It carries both anchors, so the two digests can be read. |
Test Specification: The suspect detector reports a hash that only the case's record carries as recorded only. SEG-TS-229
|
The case holds a test specification record with the hashes specHash and implHash. The current stream holds a record of the same node with specHash alone, with the same digest. The comparison has two items. specHash is matching. implHash is recorded only, with the recorded anchor and no current anchor. |
Test Specification: The suspect detector reports a hash that only the current record carries as current only. SEG-TS-230
|
The case holds a test specification record with specHash alone. The current stream holds a record of the same node with specHash, with the same digest, and implHash. The comparison has two items. specHash is matching. implHash is current only, with the current anchor and no recorded anchor. |
Test Specification: The suspect detector gives one result for each hash name, each judged by itself. SEG-TS-231
|
The case holds an implementation record with the hashes apiHash and bodyHash. In the current record apiHash covers the same text and bodyHash covers another text. The comparison has exactly two items. apiHash is matching and bodyHash is differing. The change of one hash does not change the status of the other. |
Test Specification: The suspect detector reports every hash of a node that only one side holds as one-sided. SEG-TS-232
|
The case holds a test specification record with specHash and implHash, and the current stream holds no record of the node. The comparison has two items, and both are recorded only. In the other direction, the current stream holds the record and the case holds none. Both items are then current only. |
tests/specification/test_node_content_sources.py
Test Specification: The requirements reader supplies the bytes from which it computed each hash. SEG-TS-223
|
The reader reads the requirement export of the capture-shape fixture. It supplies three requirement records, each with the hash contentHash. For each record, asking the reader for the bytes behind contentHash gives bytes whose SHA-256 is the digest in the anchor of that record. The bytes are not empty. |
Test Specification: The content extractor supplies the bytes from which it computed each hash. SEG-TS-224
|
The extractor reads the test-case export and the implementation export of the capture-shape fixture, with their Doxygen output and their C sources. It supplies test specification records with specHash and implHash, and implementation records with apiHash and bodyHash. Take each record and each hash name. The bytes that the extractor gives for the hash have a SHA-256. That SHA-256 is the digest in the anchor of the record. |
Test Specification: The would-be store supplies the bytes from which it computed each hash. SEG-TS-225
|
The store loader reads the would-be store fixture. It supplies requirement, test specification and implementation records. Take each record and each hash name. The bytes that the loader gives for the hash have a SHA-256. That SHA-256 is the digest in the anchor of the record. |
Test Specification: The composed producer supplies the bytes from which any of its readers computed a hash. SEG-TS-226
|
The producer chains the requirements reader and the content extractor over the capture-shape fixture. It supplies records of three kinds. Take each record and each hash name. The bytes that the producer gives for the hash have a SHA-256. That SHA-256 is the digest in the anchor of the record. The reader of the record gives the same bytes. |
tests/specification/test_node_show_edge_cases.py
Test Specification: node show gives content that is valid UTF-8 as text in the JSON report. SEG-TS-255
|
The file of a requirement holds text with characters outside ASCII, and the case is synced. node show exits with status 0. The JSON content of the hash is the text of the file. The entry does not name the base64 encoding. The SHA-256 of the bytes that the content stands for is the current digest. |
Test Specification: node show gives content that is not valid UTF-8 as base64, with the encoding named. SEG-TS-256
|
The file of a requirement holds bytes that are not valid UTF-8, and the case is synced. node show exits with status 0. The JSON entry names the base64 encoding. Decoding the JSON content from base64 gives exactly the bytes of the file. The SHA-256 of those bytes is the current digest. |
Test Specification: node show exits with status 2 and names the identifier when the stream holds it twice. SEG-TS-257
|
The case holds a requirement record. A control run, over a current stream that holds the record once, exits with status 0. Then the current stream holds two records with that identifier and different content. node show exits with status 2. In the text and in the JSON, the message names the identifier, and the report has no hash. No file of the case changes. |
Test Specification: node show reports no current content and no checkout for a hash only the case records. SEG-TS-258
|
The case holds a test specification record with the hashes specHash and implHash. The current record of the node has specHash alone. For implHash, the text block says that there is no current content, and it has no checkout line and no worktree line. The JSON content and the JSON checkout of implHash are null. The block of specHash still has its checkout line and its content. |
Test Specification: node show reports a repository that cannot be read, with the reason, and keeps the status. SEG-TS-259
|
The case is synced. With the repository readable, node show exits with status 0 for a matching hash, and with status 1 after the file of the requirement changes. Then the configuration maps the repository name to a directory that is not a git repository. For the same two comparisons, node show exits with the same two statuses. The checkout line says that the repository cannot be read, and gives a reason after it. The JSON checkout has no revision, and has a reason that is text and not empty. Git does not look for a repository above the test’s directory, so a checkout that holds the temporary directory cannot make the plain directory readable. |
tests/specification/test_node_show_report.py
Test Specification: node show shows the node that has the identifier it is given, as its own verb. SEG-TS-233
|
The case holds three requirements. The help of the noun node lists the verb show. Running node show with the identifier REQ-B exits with status 0. Its text report names REQ-B and the kind Requirement. Its JSON report has the identifier REQ-B, the kind Requirement and one entry for contentHash. Running it with REQ-C names REQ-C and not REQ-B. |
Test Specification: node show reports the comparison of the current and the recorded digest of each hash. SEG-TS-234
|
The case holds a test specification with the hashes specHash and implHash. Then the file that implHash covers changes and is committed. The file of specHash does not change. The report has one block for each of the two hash names. specHash is matching and implHash is differing, in the text and in the JSON. In the JSON, each entry gives the recorded digest the case holds and the current digest of the file, in full. |
Test Specification: node show reports, for each named hash, the bytes that the current stream supplies. SEG-TS-235
|
The case holds a test specification and an implementation, each with two hashes. Then the file of specHash changes in the working tree and is not committed. For the test specification, the text of the specHash block shows the new text of the file. The text of the implHash block shows the text that the file still has. The JSON content of each hash is the text of its file, and the SHA-256 of that text is the current digest of the hash. The same holds for each hash of the implementation. No block says that no content is supplied. |
Test Specification: node show reports that none is supplied for a hash when the source supplies no content. SEG-TS-236
|
The case holds a waiver and a requirement. The current stream is a record source that reads no content and supplies the same two records. For each of the two nodes, node show exits with status 0, because the hash matches. The block of the hash says that no content is supplied. The JSON content is null. The report does not show any content. |
Test Specification: node show reports the extraction revision the case records for the anchor's repository. SEG-TS-237
|
A case is synced over two repositories that are at different revisions. A requirement anchors in the first and an implementation in the second. For the requirement, node show gives the revision of the first repository as the extraction revision, in the text and in the JSON. It does not give the revision of the second. For the implementation, in both of its hashes, it gives the revision of the second repository and not the first. |
Test Specification: node show reports that none is recorded for a node record that has no extraction revision. SEG-TS-238
|
The case holds three requirement records written with no extraction revision, as a case written by an older version holds them. The content has not changed. node show exits with status 0. The text says that none is recorded, and the JSON revision is null. After a case sync adds the revision, the text gives the revision and no longer says that none is recorded. |
Test Specification: node show reports the revision of the repository the current anchor names. SEG-TS-239
|
A case sync records the revision of the repository. Then a commit changes a file that no node anchors, so the repository is at a new revision. node show for a requirement gives the new revision as the revision of the checkout, in the text and in the JSON. It gives the first revision, and only that one, as the revision the node was extracted from. |
Test Specification: node show reports that no repository is configured for a current anchor that names none. SEG-TS-240
|
A case sync records the revision of the repository. Then the configuration maps no repository for the name that the anchors carry. node show exits with status 0 and the hash matches. The checkout line says that no repository is configured. It gives no revision, and the JSON checkout has no revision. The extraction revision is still the one the case records. |
Test Specification: node show reports whether the anchored paths match their commit, naming each that differs. SEG-TS-241
|
The case holds a requirement, a test specification and an implementation, in one repository. After the sync, the two files of the test specification and one file of the implementation change in the working tree and are not committed. For the test specification, the worktree line names its two paths and no other, and the JSON dirty paths are those two. For the implementation, they are its one changed path. For the requirement, the line says clean, names no path, and the JSON dirty paths are empty. |
tests/specification/test_node_show_user_case.py
Test Specification: node show gives the differing hash, the current bytes and the recorded extraction revision. SEG-TS-253
|
A case sync records the revision of the repository. Then the content of one requirement changes and the change is committed, so the repository is at a new revision. node show for the changed requirement exits with status 1. It names contentHash as differing. It shows the new content, in the text and in the JSON, and the SHA-256 of the JSON content is the current digest. It gives the first revision as the revision the case recorded, and the new revision as the revision of the checkout. node show for a requirement that did not change exits with status 0. |
Test Specification: node show says that none is recorded, and gives no other revision in its place. SEG-TS-254
|
The case holds a requirement record with no extraction revision. A review event of an edge of that requirement records another revision, given on the command line, for the same requirement. Then the content of the requirement changes and the change is committed. node show for the requirement exits with status 1. It names contentHash as differing and shows the new content. It says that none is recorded as the extraction revision. The revision of the review event appears nowhere in the text or in the JSON. The checkout line gives the revision of the repository. |
tests/specification/test_node_show_verdicts.py
Test Specification: node show exits with status 0 while every named hash of the node matches. SEG-TS-242
|
The case holds a requirement, a test specification and an implementation, synced from one repository. Nothing has changed. For each node, node show exits with status 0, and every hash is matching in the text and in the JSON. A file that no node anchors is then added to the repository and not committed. The repository differs from its commit, and node show still exits with status 0 for each node. |
Test Specification: node show exits with status 0, and names the dirty path, for a matching hash on it. SEG-TS-243
|
A file of a requirement changes in the working tree and is not committed. Then the case is synced, so the case holds the hash of the changed content. The case holds no extraction revision for the node, because the path is dirty. node show for that requirement exits with status 0. Its hash is matching. The worktree line names the path that differs, and the JSON dirty paths are that one path. |
Test Specification: node show exits with status 1 while a named hash of the node differs. SEG-TS-244
|
The case holds a test specification with the hashes specHash and implHash. A control run exits with status 0. Then the file of implHash changes in the working tree. The file of specHash does not change. node show exits with status 1, in the text and in the JSON, although specHash still matches. |
Test Specification: node show exits with status 1 while a named hash exists on one side only. SEG-TS-245
|
The case holds two test specification records, each with the hashes specHash and implHash. A control run, over a current stream that supplies the same two records, exits with status 0 for each. Then the current record of the first node loses implHash. node show for it exits with status 1, and implHash is recorded only. Then the current record of the second node gains the hash apiHash. node show for it exits with status 1, and apiHash is current only. |
Test Specification: node show exits with status 1 while the current stream holds no node with the identifier. SEG-TS-246
|
The case holds three requirements. A control run for REQ-C exits with status 0. Then REQ-C is removed from the current store. node show for REQ-C exits with status 1, and not with status 2. Its hash is recorded only. The other requirements are not affected: node show for REQ-B still exits with status 0. |
Test Specification: node show exits with status 2 and names the identifier when the case holds no such node. SEG-TS-247
|
The case holds three requirements. A control run for REQ-B exits with status 0. The current store gains a fourth requirement, REQ-NEW, that the case does not hold. node show for REQ-NEW exits with status 2, although the current stream holds it. node show for UNKNOWN-9, which no side holds, also exits with status 2. In the text and in the JSON, the message names the identifier, and the report has no hash. |
Test Specification: node show exits with status 2 when it cannot read the current stream it is given. SEG-TS-248
|
The case holds three requirements. A control run for REQ-B exits with status 0. Then node show is given, as the current stream, a directory that does not exist. It exits with status 2. It is then given a copy of the store whose manifest of requirements is not valid. It exits with status 2. In both cases the text and the JSON give a message and no hash. |
The case holds three requirements. node show works without any option for a bundle and exits with status 0. The help of node show does not list the option –bundle. Given –bundle and the directory of a run bundle, node show ends with an argument error and exit status 2. It changes no file of the case. |
Test Specification: node show exits with status 2 when no current stream is given and no producer is configured. SEG-TS-250
|
The case holds three requirements, and the configuration names no producer. A control run that is given a current stream exits with status 0. node show for REQ-B, given no current stream, exits with status 2 and gives a message. It changes no file of the case. |
tests/specification/test_node_show_writes_nothing.py
Test Specification: node show changes no file of the case, for each exit status it gives. SEG-TS-251
|
The case holds three requirements. The test takes the SHA-256 of every file of the case. Then node show runs for four nodes. A matching node exits with status 0. A differing node exits with status 1. A node that the current stream no longer holds exits with status 1. An identifier that the case does not hold exits with status 2. After each command, the files of the case are the same. No file is added or removed. |
Test Specification: node show performs no write in the content repository, not even to its index. SEG-TS-252
|
A content repository has an out-of-date index and a change that is not committed. The change is in a file that one node anchors. Running node show for that node and for a node that anchors another file exits with status 1 and with status 0. Every file under the .git directory of the repository is the same after the commands. The same holds for every file of the working tree. |
tests/specification/test_outcome_extractor.py
Test Specification: A run identifier joins the run's name, platform and scenario, in that order. SEG-TS-053
|
The bundle records the run name twister-run-2026-09-29. Its run artifact records four scenarios, all on the platform native_sim/native/64. Extracting supplies outcomes of exactly four run identifiers. Each is the name, the platform as native_sim-native-64 and one scenario name, joined by hyphens. Each run identifier starts the identities of 19 outcomes. The nested scenarios stay apart. When the name record of the bundle holds another-run, every run identifier starts with another-run. When one scenario records the platform qemu_x86, the run identifier of that scenario holds qemu_x86. |
Test Specification: A specification identifier is the identifier of the test-case need, verbatim. SEG-TS-054
|
Extracting from the fixture supplies 76 outcomes. Each identity ends with a slash and the identifier of one of the 19 test-case needs of the export. Each need identifier ends the identities of exactly four outcomes, one for each scenario. In a copy of the export, the need TC_SAFE_DATA_INIT_AND_VERIFY is renamed TC-renamed-1. Then the four identities that ended with the old identifier end with the new one. No other identity changes. |
Test Specification: A result maps to the need whose suite and test function join the result's scenario. SEG-TS-055
|
The fixture records the result safe_data.api.safe_data.init_and_verify. The need TC_SAFE_DATA_INIT_AND_VERIFY has the suite safe_data and the test function test_init_and_verify. Extracting gives that result the specification TC_SAFE_DATA_INIT_AND_VERIFY. The same holds in the nested scenario safe_data.api.plain. In the scenario safe_data.api, that result is passed and the result write_observes_overwritten_corruption is skipped. In a copy of the export, the test functions of these two needs are swapped. Then the passed result belongs to the other need, and the skipped result belongs to TC_SAFE_DATA_INIT_AND_VERIFY. In a copy of the artifact, the scenario safe_data.api.strict is renamed zz.api in its suite and its results. Then the results of zz.api map the same way. |
In a copy of the export, a second need has the suite and the test function of TC_SAFE_DATA_INIT_AND_VERIFY. The result safe_data.api.safe_data.init_and_verify now maps to two needs. Extracting raises an error that names that result. In a copy of the export, the need TC_SAFE_DATA_SELFTEST is dropped. The result safe_data.api.safe_data.selftest now maps to no need. Extracting raises an error that names that result. |
Test Specification: A content hash covers the specification identifier, the run identifier and the result. SEG-TS-057
|
The contentHash digest of the outcome of TC_SAFE_DATA_INIT_AND_VERIFY in the scenario safe_data.api equals a SHA-256. The SHA-256 is of this canonical record: {“result”:”passed”,”run”:”twister-run-2026-09-29-native_sim-native-64-safe_data.api”, “specification”:”TC_SAFE_DATA_INIT_AND_VERIFY”} In hex, the digest is b21f9c415e6b2de8ea131a18c709acdface0c91c976041b752ae382bf3128869. Each of the 76 digests equals the SHA-256 of its own canonical record. In a copy of the artifact, the execution time and the reason of every result are changed. Then no digest changes. In a copy, the status of that result is failed. Then only its digest changes, to the digest of the record with the result failed. |
Test Specification: A recorded status maps onto the member of the closed result set it corresponds to. SEG-TS-058
|
In the fixture, each result with the status passed gives an outcome with the result passed. Each result with the status skipped gives an outcome with the result skipped. In a copy of the artifact, the result init_and_verify in safe_data.api has the status failed and the result selftest has the status error. Then the two outcomes record the results failed and error. Every other outcome is unchanged. |
Test Specification: A status with no counterpart in the closed result set is an error for that result. SEG-TS-059
|
In a copy of the artifact, the result safe_data.api.safe_data.init_and_verify has the status blocked. Extracting raises an error that names that result. The same holds for the status no-such-status. |
The fixture records 76 results. 65 are passed and 11 are skipped. The skips fall 2, 5, 1 and 3 over the four scenarios. Extracting supplies 76 outcomes. The 11 outcomes with the result skipped are exactly those of the 11 skipped results. |
Test Specification: An outcome's revision is the revision the bundle records for the implementation checkout. SEG-TS-061
|
The record of the implementation checkout (toolbox) in the bundle holds 5847f3fdca777b8d62615d84b8926fdc8ce125ed and a line feed. Each of the 76 outcomes has that text, without the line feed, as its revision. When the record holds 77e25d8f3cb2e94adb5a44426b98e088f1bef3fe, every outcome has that revision. |
Test Specification: A run with no recorded full revision is refused, and no outcome is supplied. SEG-TS-062
|
Building the extractor raises an error when the bundle holds no revision record of the implementation checkout. It raises the same error when the record is empty. It raises the same error when the record holds only a line feed. |
Test Specification: A Confirms edge runs from each outcome to the specification its result maps to. SEG-TS-063
|
Extracting from the fixture supplies exactly 76 edges of kind Confirms. Their pairs are the 76 pairs of an outcome identity and a specification identifier, formed from the results. One pair is the outcome of safe_data.api.safe_data.init_and_verify and TC_SAFE_DATA_INIT_AND_VERIFY. No outcome has two such edges. |
Test Specification: A Witnesses edge runs from each outcome to each implementation of what its test verifies. SEG-TS-064
|
The need TC_SAFE_DATA_INIT_AND_VERIFY verifies SD-REQ-001 and SD-REQ-003. The implementation needs IMPL-safe_data_init and IMPL-safe_data_verify satisfy them. Each of the four outcomes of that specification has Witnesses edges to exactly those two implementations. For every outcome, the edges run to exactly the implementations whose need satisfies a requirement that its specification verifies. This holds for a skipped outcome too. The skipped outcome of TC_SAFE_DATA_WRITE_OBSERVES_OVERWRITTEN_CORRUPTION has one edge, to IMPL-safe_data_write. In a copy of the implementation export, IMPL-safe_data_commit also satisfies SD-REQ-001. Then the four outcomes have an edge to it as well. Without the implementation input, no Witnesses edge is supplied. |
Test Specification: An outcome's anchor names its bundle by digest, the artifact's path in it, and the result. SEG-TS-065
|
Each of the 76 outcomes has exactly one content hash, contentHash. Its anchor names as its repository the digest of the clean bundle, written as sha256: and 64 hex digits. Its path is the run artifact within the bundle, twister.json. Its locator is nodeid: followed by the identifier of the result, for example nodeid:safe_data.api.safe_data.init_and_verify. In a copy of the fixture, the bundle is moved to out/run1. Then every anchor still has the same repository member and the same path. |
tests/specification/test_outcome_extractor_boards.py
Test Specification: A leaf is satisfied when the test of its specification passed on every board. SEG-TS-331
|
One run artifact records one test on three platforms, native_sim/native/64, qemu_x86 and mps2/an385, and the test passed on each. One leaf requirement has an active Verifies edge from the specification of the test and an active Implements edge. The extractor supplies three outcomes, one for each platform, and each outcome has a Confirms edge to the specification. The satisfaction evaluator reports the leaf as satisfied. The same holds for the first two platforms alone. |
Test Specification: A leaf is not satisfied when the test failed on one board, though it passed on the others. SEG-TS-332
|
One run artifact records one test on three platforms. The test passed on two and failed on one, and the failing board is in turn the first, the second and the third. The extractor supplies three outcomes. For each order, the satisfaction evaluator reports the leaf as not satisfied. The package gate blocks, and the outcome of the failing board is the one outcome that no waiver excuses. A control with the test passed on every board is satisfied. |
Test Specification: A board that skipped the test adds no obligation: the others decide the leaf. SEG-TS-333
|
One run artifact records one test on three platforms. The test passed on two and was skipped on one, and the skipping board is in turn the first, the second and the third. The extractor supplies three outcomes. For each order, the satisfaction evaluator reports the leaf as satisfied. The package gate lists the skipped outcome and no other, and the gate does not block. The same holds for a run artifact with two platforms, where the test was skipped on one and passed on the other. |
tests/specification/test_outcome_extractor_need_ids.py
Test Specification: With a list and no need types, an outcome witnesses the listed needs only. SEG-TS-433
|
The implementation export holds IMPL-A and IMPL-B of the type impl and IMPL-C of the type design. Each satisfies the requirement that two test cases verify. A run bundle holds one passed result for each test case. The list IMPL-A, IMPL-C is configured and no need types are. Each of the two outcomes has a Witnesses edge to IMPL-A and to IMPL-C, and to no other need. A control without the list gives each outcome an edge to all three. |
Test Specification: With need types and no list, an outcome witnesses the needs of those types. SEG-TS-434
|
The implementation export holds IMPL-A and IMPL-B of the type impl and IMPL-C of the type design. Each satisfies the requirement that two test cases verify. A run bundle holds one passed result for each test case. The types {impl} are configured and no list is. Each of the two outcomes has a Witnesses edge to IMPL-A and to IMPL-B and to no other need. With the types {design} each has one edge, to IMPL-C. |
Test Specification: With need types and a list of need identifiers, a witnessed need is listed and typed. SEG-TS-435
|
The implementation export holds IMPL-A and IMPL-B of the type impl and IMPL-C of the type design, and each satisfies the requirement that two test cases verify. The types {impl} and the list IMPL-A are configured. Each of the two outcomes has one Witnesses edge, to IMPL-A. There is none to IMPL-B, which has the type and is not listed, and none to IMPL-C, which has neither. With the types {impl, design} and the list IMPL-B, IMPL-C each outcome has an edge to those two needs only. |
Test Specification: While neither need types nor a list is configured, an outcome witnesses every need. SEG-TS-436
|
The implementation export holds IMPL-A and IMPL-B of the type impl and IMPL-C of the type design, and each satisfies the requirement that two test cases verify. The configuration names no need types and no list. Each of the two outcomes has a Witnesses edge to each of the three needs. A list that is null, which is the same as no list, gives the same edges. |
Test Specification: A listed need identifier that names no need of the export is refused, naming it. SEG-TS-437
|
The implementation export holds IMPL-A, IMPL-B and IMPL-C. The list IMPL-A, IMPL-GONE is configured. Building the outcome extractor raises one error. The error names IMPL-GONE and does not name IMPL-A. A control that lists IMPL-A and IMPL-B builds the extractor without an error. |
Test Specification: A listed need identifier whose need the configured types do not admit is refused. SEG-TS-438
|
The implementation export holds IMPL-A and IMPL-B of the type impl and IMPL-C of the type design. The types {impl} and the list IMPL-A, IMPL-C are configured. Building the outcome extractor raises one error. The error names IMPL-C and does not name IMPL-A. A control that configures the types {impl, design} with the same list builds the extractor without an error. |
Test Specification: Every listed need identifier that names no admitted need is named in one error. SEG-TS-439
|
The implementation export holds IMPL-A and IMPL-B of the type impl and IMPL-C of the type design. The types {impl} and the list IMPL-A, IMPL-GONE-A, IMPL-C, IMPL-GONE-B are configured: two identifiers that name no need and one that names a need of another type. Building the outcome extractor raises one error. The error names IMPL-GONE-A, IMPL-C and IMPL-GONE-B, once each, and does not name IMPL-A. |
Test Specification: A need that is not in the list of need identifiers is not refused, whatever its fault. SEG-TS-440
|
The implementation export holds IMPL-A, IMPL-B and IMPL-C, and two needs that the outcome extractor cannot use: IMPL-RENAMED, whose id is another text than its key, and IMPL-BAD-LINKS, whose links are a text and not a list. Without a list, building the outcome extractor raises an error that names the two. With the list IMPL-A, IMPL-B the extractor is built without an error, and each outcome has a Witnesses edge to those two needs. With a list that holds IMPL-A and IMPL-BAD-LINKS it raises an error that names IMPL-BAD-LINKS and not IMPL-RENAMED: a need that is listed is still refused for its fault. |
tests/specification/test_outcome_extractor_need_types.py
The test-case export holds TC-A and TC-B of the type test_case. It also holds TC-OTHER of the type test_other, with a suite and a test function. A run bundle records a result for the test of each of the three needs. With the types {test_case, test_other} configured, the extractor supplies three outcomes, and one of them confirms TC-OTHER. With the types {test_case} configured, the extractor refuses the bundle with an error that names the result of TC-OTHER, because that result maps to no test-case need. |
Test Specification: While no type is configured, every need of the test-case export is a test-case need. SEG-TS-318
|
The test-case export holds TC-A of the type test_case and TC-OTHER of the type test_other, both with a suite and a test function. A run bundle records a result for the test of each. With no types configured, the extractor supplies two outcomes, and the outcomes confirm TC-A and TC-OTHER. When the export also holds a need of the type test_procedure whose suite is null, the extractor refuses the export with an error that names the need and says it has no text field ‘suite’. |
The test-case export holds two needs of the type test_case and three needs of the type test_procedure. The identifier of a procedure need has the form test-proc-<area>_api_procedures-<step>, and its suite and test function are null. The types {test_case} are configured. A run bundle records one result for the test of each test case. Building the extractor and taking every record raises no error. The extractor supplies two outcomes, and each Confirms edge runs to a test case. No edge runs to a procedure need. |
Test Specification: A bundle read over exports that hold needs of other types is not refused. SEG-TS-320
|
The test-case export of the toolbox fixture has a need of the type test_procedure added, with a suite and a test function that are null. The implementation export has a need of the type design added, whose links are not a list. The configuration names the types test_case and impl for the two exports. Running graph status with the clean bundle and a given revision exits with status 0. Its machine-readable report counts 76 outcomes at the current revision and none at another. |
Test Specification: With no types configured, a need of another type with no test function refuses the read. SEG-TS-321
|
The test-case export of the toolbox fixture has a need of the type test_procedure added, with a suite and a test function that are null. The configuration names no types. Running graph status with the clean bundle and a given revision exits with status 2 and prints no report. The output names the procedure need. A control, whose export lacks that need, gives exit status 0. |
The implementation export holds IMPL-1 of the type impl and NOTE-1 of the type design. The links of NOTE-1 are a text and not a list. A run bundle records one result for one test case. With the types {impl} configured for the implementation export, the extractor is built without an error, and one Witnesses edge runs from the outcome to IMPL-1. With no types configured, the extractor refuses the export with an error that names NOTE-1. |
Test Specification: Witnesses edges come only from the implementation needs of the configured types. SEG-TS-323
|
The implementation export holds IMPL-1 of the type impl and NOTE-1 of the type design. Both satisfy the requirement that the one test case verifies, and both have a valid list of links. A run bundle records one result for that test case. With the types {impl} configured, the extractor supplies one Witnesses edge from the outcome, and it runs to IMPL-1. With the types {design} configured, the one edge runs to NOTE-1. |
Test Specification: While no type is configured, every need of the implementation export is read. SEG-TS-324
|
The implementation export holds IMPL-1 of the type impl and NOTE-1 of the type design. Both satisfy the requirement that the one test case verifies. A run bundle records one result for that test case. With no types configured for the implementation export, the extractor supplies two Witnesses edges from the outcome, one to each need. |
tests/specification/test_proof_show.py
Test Specification: Proof show and proof verify accept an identifier, a unique prefix of it, or a directory path. SEG-TS-133
|
A case holds one generated package. For each of the two verbs, naming the package by its snapshot identifier, by the first twelve characters of the identifier, and by the path of a copy of its directory outside the case gives exit status 0. For proof show the three renderings are the same report, and its snapshot identifier is the identifier of the package. |
Test Specification: Proof show and proof verify exit with status 2 for a prefix that names two packages. SEG-TS-134
|
A case holds two packages generated one second apart, so that their identifiers share a long prefix. A prefix of both identifiers makes each verb exit with status 2. The output names both packages by identifier and holds no report. A prefix of the first identifier alone, longer than the shared one, names one package, and each verb exits with status 0. |
Test Specification: Proof show reports the snapshot, scopes, revision, totality, root and findings. SEG-TS-135
|
For a generated package, the machine-readable report of proof show holds the snapshot identifier, the requested scope, the member scope, the revision, the totality flag, the design root and the digests of the run bundles, each equal to what the documents of the package record, and the findings of the coverage report in the order of the report. The human-readable report holds the snapshot identifier, the revision, the design root, each digest and each requested requirement. |
Test Specification: Proof show reports, for each requirement of the scope, what the package records for it. SEG-TS-136
|
For a generated package, the machine-readable report of proof show holds one entry for each requirement of the package’s node manifest and no other entry. Each entry holds the requirements that refine it, the specifications that verify it, the implementations that implement it, and the outcomes (identifier and result) that confirm one of those specifications. The expected lists are read by hand from the design edges and the execution coverage record. At least one entry holds a skipped outcome, and at least one entry refines no requirement and holds no specification. |
Test Specification: Proof show says that no run bundle digest is recorded for a package that lists none. SEG-TS-137
|
The golden package was sealed before packages listed run bundles. For it, proof show exits with status 0, its human-readable report holds the words “not recorded” on the line about the run bundle digests, and its machine-readable report holds no digest for them. A generated package that lists a digest shows the digest and not those words. |
Test Specification: Proof show gives the same report whatever the readers of the configuration supply. SEG-TS-138
|
A control call of proof show names the package with a working configuration. Then the producer that reads the current stream is replaced by one that records each call and fails, and proof show gives the same report and exit status 0. The producer was not called. A second call names a configuration whose requirement export does not exist: the report is the same again. |
Test Specification: Proof show exits with status 0 for a package that records a blocked scope or a wrong root. SEG-TS-139
|
Four packages are read. A generated package that records no problem, a private copy whose coverage report records the scope as blocked with a finding of severity error, a private copy whose recorded root is not the root of its design, and the golden package. For each of them proof show exits with status 0 and reports the package. |
Test Specification: Proof show and proof verify exit with status 2 for a package that cannot be read. SEG-TS-140
|
A generated package is read by each verb with exit status 0. Six other names each give exit status 2 and a refusal in the output: an identifier that the case does not hold, a path that is no directory, an empty directory, a copy without its coverage report, a copy whose evidence manifest is not JSON, and a copy whose design consistency proof lacks its root. The output holds no report. |
Test Specification: Proof show reads a package named by its directory path from an empty directory. SEG-TS-158
|
A generated package is copied to a place outside its case. The working directory is empty: it holds no configuration file and no case, and the call names neither. Given only the path of the copy, proof show exits with status 0 and reports the snapshot identifier of the package. The directory is still empty afterwards. |
tests/specification/test_proof_verbs.py
Test Specification: The operator asks the gate about a scope and generates the package, each as its own verb. SEG-TS-149
|
Over the frozen evidence and a case with every strong edge affirmed, proof check reports the gate’s coverage report as machine-readable output and exits with status 0, and writes nothing. Proof generate, as a separate verb, writes the four documents of a package under the case and exits with status 0. |
Test Specification: The operator shows and verifies an evidence package, each as its own verb. SEG-TS-150
|
For a generated package, proof show exits with status 0 and its machine-readable report holds a list of requirements and no list of checks. Proof verify, as a separate verb, exits with status 0 and its machine-readable report holds a list of checks and no list of requirements. |
Test Specification: The root of a package is the root that the design consistency proof's own contents give. SEG-TS-151
|
Two packages are generated, one over the clean bundle and one over the clean bundle and a second bundle at another revision. For each, the recipe of the tutorial gives the recorded root from the node hashes, the design edges, the scope and the revision of the design consistency proof, and from nothing else. The golden package gives the root of the golden file. A copy of a package with one digit of a node hash changed gives another root than the recorded one. |
tests/specification/test_proof_verifier_bundles.py
Test Specification: The verifier fails the bundle digests check for a bundle the package does not list. SEG-TS-127
|
A package lists the digest of the clean bundle. Given that bundle, the check named bundle-digests is passed. Given a copy of the clean bundle with one file more, the check is failed and its detail holds the digest of the given copy. A package that lists no digest, the golden package, gives the same result for the clean bundle. |
Test Specification: The verifier reports the evidence as not judged when a listed bundle is not given. SEG-TS-128
|
A package lists the digests of two bundles. Given both, the checks named bundle-digests, rebuilt-evidence and snapshot-id are passed. Given only the first bundle, no check fails. The check named bundle-digests is not judged, its detail holds the digest of the bundle that is missing, and the checks named rebuilt-evidence and snapshot-id are not judged. |
Test Specification: The verifier reports the evidence as not judged when a design node hash differs. SEG-TS-129
|
Given the clean bundle and the readers of the configuration, the check named design-guard is passed for a generated package. In a private copy the node hash of one requirement is changed by one digit in the design consistency proof, and the root is sealed again over the changed hash. The root and identity checks of the copy are passed. The design-guard check is not judged, its detail names the requirement, and the checks named rebuilt-evidence and snapshot-id are not judged. No check fails. |
Test Specification: The verifier leaves the evidence unjudged for a design edge that no reader supplies. SEG-TS-130
|
In a private copy of a generated package one more design edge joins two requirements that the readers of the configuration do not join, and the root is sealed again over the longer edge list. Given the clean bundle, the check named design-guard is not judged, its detail names both endpoints of the edge, and the checks named rebuilt-evidence and snapshot-id are not judged. The root check is passed. No check fails. |
Test Specification: The verifier reports the rebuilt evidence check as failed when the record differs. SEG-TS-131
|
Given the clean bundle, the verifier rebuilds the outcomes and the findings at the revision the package records. For a generated package the check named rebuilt-evidence is passed. Two private copies each change the record. In the first, the result of one passed outcome in the execution coverage record is failed. In the second, the coverage report holds one more finding about an outcome of the record. For each copy the check named rebuilt-evidence is failed, and the root check is still passed. |
Test Specification: The verifier reports the snapshot identifier check as failed when the identifier differs. SEG-TS-132
|
A package generated at one timestamp and a package generated at another timestamp each pass the check named snapshot-id, given the clean bundle: the verifier mints the identifier with the timestamp the recorded identifier carries. A private copy changes the fingerprint part of the identifier in the design consistency proof and in the evidence manifest, so that the two documents agree, and the directory takes the new name. For the copy the check named snapshot-id is failed and the check named identity is passed. |
tests/specification/test_proof_verifier_package.py
Test Specification: The verifier recomputes the design root of a package and reports that it equals the record. SEG-TS-119
|
A package generated over the frozen evidence records a root. The recipe of the tutorial, written again in the test from the node hashes, the design edges, the scope and the revision of the design consistency proof, gives the same value. The verifier reports the check named root as passed. The golden package, which was sealed before packages listed run bundles, records the root in the golden file; the recipe gives that value too, and the verifier passes the root, the identity, the agreement and the unblocked checks of it. The verifier needs no configuration, no case and no run bundle for these checks. |
Test Specification: The verifier reports the root check as failed when one input of the root changed. SEG-TS-120
|
Four private copies of a generated package each change one input of the root in the design consistency proof, and nothing else: one hexadecimal digit of a node hash, a design edge removed, the revision, and the scope. The root recorded in each copy is the original. For each copy the check named root is failed. For the first two copies it is the only check that fails. An untouched copy passes the root check. |
Test Specification: The verifier reports the identity check as failed when two documents name different packages. SEG-TS-121
|
In a generated package the evidence manifest and the design consistency proof agree on the snapshot identifier, the requested scope and the revision: the check named identity is passed. Three private copies each change one of the three in the evidence manifest only: another snapshot identifier, one requested requirement removed, another revision. For each copy the identity check is failed, and the root check is still passed. |
Test Specification: The verifier reports the agreement check as failed for a name that is no member of the scope. SEG-TS-122
|
In a generated package every outcome and every finding that the execution coverage record and the coverage report name is a member of the member scope of the evidence manifest: the check named agreement is passed. Two private copies each break that. In the first, one outcome of the execution coverage record is removed from the member scope. In the second, the coverage report holds one more finding about a name that is no member. For each copy the agreement check is failed and the root check is still passed. |
Test Specification: The verifier reports the agreement check as failed when the record and the report differ. SEG-TS-123
|
In a generated package the execution coverage record and the coverage report agree on which outcomes are set aside, skipped and excused. Three private copies each break one of the three. In the first, an outcome that the record holds is also listed as stale in the report. In the second, an outcome that the report lists as skipped has the result passed in the record. In the third, the report lists as excused an outcome that carries no waiver in the record. For each copy the check named agreement is failed. |
Test Specification: The verifier reports the unblocked check as failed when the report says the scope is blocked. SEG-TS-124
|
The coverage report of a generated package records the scope as not blocked: the check named unblocked is passed. A private copy changes the one flag, as the tutorial does with a text editor, and nothing else. The unblocked check of the copy is failed. The root check is still passed, because the root does not cover the report, and the check named unblocked is the only check that fails. |
Test Specification: The verifier reports the affirmations check as passed when the case binds every design edge. SEG-TS-125
|
The case in which the package was generated holds a review event for every strong edge, made when the edges were affirmed. Given that case, the verifier reports the check named affirmations as passed for a generated package. Given no case, it does not make the check: the check is not made. |
Test Specification: The verifier reports the affirmations check as failed for an edge the case does not bind. SEG-TS-126
|
Two private copies of the case each change the review events of one design edge of the package. In the first, the one event of the edge is removed. In the second, the event is kept and the content hash of its requirement endpoint is changed by one hexadecimal digit, so that it binds another node hash than the package records. For each copy, given that case, the check named affirmations is failed and its detail names both endpoints of the edge. Checked against the original case, the same package passes. |
Test Specification: The verifier fails the identity check when the identifier is not the directory name. SEG-TS-152
|
A generated package, named by the path of its directory, passes the check named identity. A private copy of the same documents sits in a directory with another name. For the copy the identity check is failed, its detail holds both names, and the root check is still passed. |
Test Specification: The verifier fails the agreement check for an outcome that carries another revision. SEG-TS-153
|
In a generated package every outcome of the execution coverage record carries the revision of the package: the check named agreement is passed. A private copy gives one outcome of the record another revision, with the same form. For the copy the agreement check is failed and the root check is still passed. |
Test Specification: The verifier fails the agreement check when a recorded outcome is also listed as stale. SEG-TS-154
|
A private copy of a generated package lists in its coverage report, as stale, one outcome that its execution coverage record holds. For the copy the check named agreement is failed and the root check is still passed. The untouched package passes. |
Test Specification: The verifier fails the agreement check when the member scope has too much or too little. SEG-TS-155
|
The member scope of a generated package is the design nodes, the outcomes and nothing else: the check named agreement is passed. Two private copies change the evidence manifest only. In the first, the member scope holds one name more that no document names. In the second, one design node is missing from the member scope. For each copy the agreement check is failed and the root check is still passed. |
Test Specification: The verifier fails the unblocked check when the report lists an unready edge. SEG-TS-156
|
A private copy of a generated package lists one design edge as pending in the unready edges of its coverage report, and keeps the flag that says the scope is not blocked. For the copy the check named unblocked is failed and the root check is still passed. The untouched package passes. |
Test Specification: The verifier fails the unblocked check when the report holds a finding that blocks. SEG-TS-157
|
A private copy of a generated package holds one more finding of severity error in its coverage report, about a requirement of the scope, and keeps the flag that says the scope is not blocked. For the copy the check named unblocked is failed and the root check is still passed. |
tests/specification/test_proof_verify_cli.py
Test Specification: Proof verify names each check with its status, and names each check it did not make. SEG-TS-141
|
For a generated package named with no run bundle and no request for the affirmations, the machine-readable report holds ten checks by name: root, identity, agreement, unblocked, affirmations, bundle-digests, design-guard, rebuilt-evidence, snapshot-id and sibling-digests. The first four are passed, and the other six are not made. With the clean bundle and the request for the affirmations, the first nine are passed and the check named sibling-digests is still not made. In the human-readable report one line starts with each name and holds the status. For a copy whose root is wrong, the line of the root check holds the word failed. |
Test Specification: Proof verify judges the evidence by the run bundles named in the invocation and no others. SEG-TS-142
|
One package lists the digests of two bundles, and another lists the digest of the clean bundle alone. Naming both bundles for the first gives exit status 0. Naming only the clean bundle for the first gives exit status 2. Naming no bundle gives exit status 0, with the bundle checks not made. For the second package, naming the clean bundle gives exit status 0, and naming the clean bundle and the second bundle gives exit status 1, because the second bundle is a bundle that the package does not list. The configuration names no bundle in any call. |
Test Specification: Proof verify checks the affirmations only when asked, against the case that the call names. SEG-TS-143
|
The case that holds a package binds every design edge. With the request for the affirmations, the check named affirmations is passed and the exit status is 0. A private copy of the case lacks the review event of one design edge. Naming that copy as the case, with the request, gives exit status 1 and a failed affirmations check. Naming that copy without the request gives exit status 0 and the check not made. |
Test Specification: Proof verify exits with status 1 when a check fails, even if another is not judged. SEG-TS-144
|
Four private copies of a generated package fail one check each: a changed digit of a node hash (root), another requested scope in the evidence manifest (identity), a record that disagrees with the report (agreement), and a blocked scope (unblocked). Each gives exit status 1 and names the failed check. A copy of a package that lists two bundles, with a wrong root, named with only one bundle, has a failed root check and a check that is not judged. It gives exit status 1. |
Test Specification: Proof verify exits with status 2 when an asked check is not judged and no check failed. SEG-TS-145
|
A package lists two bundles and the call names one: the bundle checks are not judged, no check fails, and the exit status is 2. A copy of a package with one node hash changed and the root sealed again, named with the clean bundle, has a design guard that is not judged, no failed check, and exit status 2. The same two calls without any bundle give exit status 0. |
Test Specification: Proof verify exits with status 0 when every check made passed and every asked one was judged. SEG-TS-146
|
For a generated package the exit status is 0 in four calls: with the package alone, with the clean bundle, with the request for the affirmations, and with both. A package that lists two bundles gives exit status 0 when both are named. The golden package, which lists none, gives exit status 0 with the package alone. |
Test Specification: Proof verify takes no revision option and never asks for the revision of a repository. SEG-TS-147
|
Naming an option –revision for proof verify is a usage error with exit status 2. The function that resolves the revision for the other proof verbs is replaced by one that records each call and fails. Proof verify, named with the clean bundle, still gives exit status 0 and the function was not called. |
Test Specification: Proof show and proof verify leave every file of the case, bundles and configuration alone. SEG-TS-148
|
A case holds a generated package, and its bundles and configuration lie beside it. Every file under the directory has its bytes recorded. Proof show, and proof verify with the package alone, with the bundle, with the request for the affirmations, and for a package that fails, each run with the machine-readable and the human-readable rendering. Afterwards the directory holds the same files with the same bytes, and no other. |
Test Specification: Proof verify judges the package checks of a package named by path from an empty directory. SEG-TS-159
|
A generated package is copied to a place outside its case. The working directory is empty: it holds no configuration file and no case, and the call names neither. Given only the path of the copy, proof verify exits with status 0. The checks named root, identity, agreement and unblocked are passed, and the other six are not made. The directory is still empty afterwards. |
tests/specification/test_reader_parent_field_and_source_map.py
The configuration names the field trace. Reading the fixture export gives exactly three Refines edges: R-2 to R-1, R-3 to R-1 and R-3 to R-2. No edge goes to R-DECOY, the link in the field refines of R-2. |
The configuration names no parent field. Reading the fixture export gives exactly one Refines edge, R-2 to R-DECOY, the link in the field refines. The links in the field trace are not followed. |
The configuration holds a source map and no source directory. The content hash anchor of R-1 and R-2 names the repository docs, the path reqs/alpha.sdoc and the locator need:R-1 or need:R-2. That of R-3 names reqs/beta.sdoc. The digest of each equals the digest of the source directory form for the same need. So the map changes the anchor and never the hash. |
Test Specification: A docname the source map does not cover is refused, and every one is named. SEG-TS-163
|
In a copy of the export, two needs of the configured type req sit in the documents docs/delta and docs/epsilon. The map does not name them. Building the reader raises a source error that names both docnames. It names none of docs/alpha, docs/beta and docs/gamma. The first two are mapped. The third holds only a need of the type info, and that type is not configured. |
The configuration names the field trace. For each requirement, the contentHash digest equals a SHA-256 that the test computes. The test hashes the canonical JSON of the title, the content and the sorted parent links, under the key refines. The digest also equals the digest from a copy of the export whose parents sit in the field refines, read with the default. The decoy link of R-2 changes nothing. |
The configuration names the field trace. In a copy of the export, the links of R-3 are listed in the other order. The contentHash digest of R-3 is the digest the fixture gives. Both equal the SHA-256 of the canonical form of R-3 with its parents sorted. The test computes that digest. |
Test Specification: Refines edges come from the declared parent links, and from no back-link field. SEG-TS-186
|
The configuration names the field trace. R-1 holds the back-links R-2 and R-3 in the field trace_back. Reading the export gives one pending Refines edge per declared link, from the child to the parent: three edges, and none from R-1. |
Test Specification: A Requirement is anchored in the repository configured for the requirements reader. SEG-TS-187
|
The default repository is suite. The requirements reader names the repository docs and a source directory in it. The content hash anchor of R-1 names the repository docs and the path reqs/docs/alpha.rst. That path joins the source directory, the docname and the doctype, within docs. |
tests/specification/test_repository_path_refusal.py
Test Specification: A producer over three plain directories that hold the files is read without an error. SEG-TS-403
|
The three repositories of the fixtures are plain directories, with no version-control data, and each holds the files its stream reads. Building the producer and taking its nodes and edges raises no error. The producer supplies nine nodes. This is the control for the specifications that follow, so each of them fails for the repository path alone. |
Test Specification: A repository path that does not exist is reported once, by its name and with its path. SEG-TS-404
|
The configuration maps the repository of the test stream to a path that does not exist. Three needs read through it. The producer is built and its records are taken. One source error is raised. Exactly one of its lines holds the configured name of the repository. That line also holds the configured path and says that the path does not exist. No line holds the identifier or the symbol of a need of that stream, and the other two repositories are not named. |
Test Specification: A repository path that is a file is reported once, by its name and with its path. SEG-TS-405
|
The configuration maps the repository of the implementation stream to a path that is a file. Three needs read through it. The producer is built and its records are taken. One source error is raised. Exactly one of its lines holds the configured name of the repository. That line also holds the configured path and says that the path is not a directory. No line holds the identifier or the symbol of a need of that stream. |
The configuration gives the implementation stream and the test stream one repository name, and maps it to a path that does not exist. Six needs read through it. One source error is raised. Exactly one of its lines holds the configured name, and that line holds the path. No line holds the identifier or the symbol of a need. |
Test Specification: Two repositories whose paths cannot be used are both reported in one error. SEG-TS-407
|
The configuration maps the repository of the implementation stream to a path that does not exist, and the repository of the test stream to a path that is a file. The requirements repository is fine. One source error is raised. It has one line that holds the name of the first repository and its path, and one line that holds the name of the second repository and its path. No line holds the name of the requirements repository or the identifier or the symbol of any need. |
The three repositories are plain directories that hold the files the streams read and no version-control data. Case sync over an initialized case exits with status 0 and prints the sync line. It prints, for each of the three configured names, a line that says that node records were written without an extraction revision. The case holds nine nodes, three for each stream. |
Test Specification: A repository path that only the requirements reader reads through is not refused. SEG-TS-409
|
The configuration maps the repository of the requirements reader to a path that does not exist. The other two repositories are fine. Building the producer and taking its records raises no error, and the producer supplies the three requirements. Case sync over an initialized case exits with status 0 and its output says nothing about a path that does not exist. |
Test Specification: Case sync over a repository path that does not exist exits with status 2 and writes nothing. SEG-TS-410
|
The configuration maps the repository of the test stream to a path that does not exist. Case sync over an initialized case exits with status 2. Its output has exactly one line that holds the configured name of the repository, and that line holds the path. No line holds the identifier or the symbol of a need. The files of the case are the same after the command as before it. The output holds no traceback. |
The configuration maps the repository of the implementation stream to a path that does not exist. The test stream reads through a repository that is a directory but lacks the test source file its Doxygen output names, so each of its needs has a fault of its own. One source error is raised. It has a line that holds the configured name of the first repository, and every line that holds the identifier or the symbol of a need comes after that line. |
Test Specification: Several repositories whose paths cannot be used are listed sorted by configured name. SEG-TS-414
|
The configuration names the repository of the implementation stream zeta-name and the repository of the test stream alpha-name, and maps both to a path that does not exist. The implementation stream comes first in the order of the streams, but the error lists the line of alpha-name before the line of zeta-name. Building the producer a second time gives an error with the same lines. |
tests/specification/test_repository_reads_decoy_case.py
Test Specification: edge show names the commit of the case itself, whatever repository the environment names. SEG-TS-297
|
A case is a git repository. One commit by Alice adds the review event of an edge. A second repository holds a copy of the files of the case, in a commit by Dan. One variable of the environment names it: GIT_DIR, GIT_WORK_TREE, GIT_OBJECT_DIRECTORY or GIT_COMMON_DIR. edge show exits with status 0. In text and in JSON, the provenance of the edge is found, and it names the commit by Alice and her identity. It does not name the commit by Dan, or his e-mail address. A control, without the variable, gives the same. Git, called with the variable, answers differently, so the decoy works. |
Test Specification: edge show reports a case inside another repository as not available, whatever GIT_DIR names. SEG-TS-298
|
A case lies inside another repository, which holds it in a commit of its own. edge show for an edge of that case exits with status 0. It reports the history as not available: the JSON status is unavailable, and no commit, committer or author is named. The same holds when GIT_DIR names the git directory of the enclosing repository. Git, called with that variable, takes the case for the top level of that repository, so the variable changes the answer of git. |
tests/specification/test_repository_reads_decoy_content.py
Test Specification: case sync records the revision of the repository at the path, whatever the environment names. SEG-TS-292
|
A case is empty. A configuration maps the content repository, which holds the committed content of three requirements. A second repository has other commits. One variable of the environment names it: GIT_DIR, GIT_WORK_TREE, GIT_INDEX_FILE, GIT_OBJECT_DIRECTORY or GIT_COMMON_DIR. Running case sync exits with status 0 and prints no line about a missing extraction revision. Each node record carries the revision of the content repository, as git gives it with no such variable. It never carries a revision of the second repository. A control, without the variable, gives the same records. Git, called with the variable, answers differently, so the decoy works. |
Test Specification: case sync gives no revision for a repository without objects, whatever the environment names. SEG-TS-293
|
The content repository has lost every object file, so git cannot read a commit in it. A second repository holds a copy of those objects. A first case sync, without a variable, exits with status 0 and records no revision. It prints one line that names the repository and the count 3. Then GIT_ALTERNATE_OBJECT_DIRECTORIES names the object store of the second repository, and case sync runs again. It exits with status 0 and records no revision. It prints the same line. Git, called with the variable, can read the commit, so the variable changes the answer of git. |
Test Specification: edge affirm records the revision of the repository at the path, not an environment one. SEG-TS-294
|
A configuration maps the content repository, which holds the committed content of three requirements. A second repository has other commits. One variable of the environment names it: GIT_DIR, GIT_WORK_TREE, GIT_INDEX_FILE, GIT_OBJECT_DIRECTORY or GIT_COMMON_DIR. Running edge affirm for the edge from REQ-B to REQ-A, with no revision given, exits with status 0 and refuses nothing. The review event holds the revision of the content repository for both endpoints, and no other revision. Each of the two node records carries that revision. A control, without the variable, gives the same event revisions. Git, called with the variable, answers differently, so the decoy works. |
Test Specification: node show reports the revision and the cleanliness of the repository at the path. SEG-TS-295
|
A case holds three requirements, written by a case sync. The content repository is clean. A second repository has other commits. One variable of the environment names it: GIT_DIR, GIT_WORK_TREE, GIT_INDEX_FILE, GIT_OBJECT_DIRECTORY or GIT_COMMON_DIR. Running node show for REQ-B exits with status 0. The checkout of its hash names the revision of the content repository, as git gives it with no such variable. It lists no dirty path and reports no error. Git, called with the variable, answers differently, so the decoy works. |
Test Specification: edge show recovers the before-content from the repository at the path. SEG-TS-296
|
An edge from REQ-B to REQ-A is affirmed. Then the text of both requirements changes, and the change is committed in the content repository. A second repository has other commits. One variable of the environment names it: GIT_DIR, GIT_OBJECT_DIRECTORY or GIT_COMMON_DIR. Running edge show with the options for verbose JSON exits with status 0. The before-content of each endpoint is the text that the content repository held when the edge was affirmed. A control, without the variable, gives the same text. Git, called with the variable, answers differently, so the decoy works. |
Test Specification: edge affirm refuses a dirty content repository, whatever repository the environment names. SEG-TS-316
|
The content repository holds an uncommitted change in the file of REQ-B. A second repository is made so that it hides the change from a read of the wrong repository. One variable of the environment names it: GIT_DIR, GIT_WORK_TREE or GIT_INDEX_FILE. Running edge affirm for the edge from REQ-B to REQ-A, with no revision given, exits with status 2 and names the file of REQ-B. It writes no review event. A control, without the variable, gives the same. Git, called with the variable, reports no change in that file for GIT_DIR and GIT_WORK_TREE, so the decoy works. |
tests/specification/test_repository_reads_decoy_no_write.py
Test Specification: case sync writes nothing in the content repository or in the decoy, with a variable set. SEG-TS-299
|
A content repository has an out-of-date index and a change that is not committed. A second repository has an out-of-date index too. One variable of the environment names it: GIT_DIR, GIT_WORK_TREE or GIT_INDEX_FILE. Running case sync exits with status 0. Every file under the .git directory of each repository is the same after the command, and so is every file of each working tree. |
Test Specification: edge affirm and node show write nothing in the content repository or in the decoy. SEG-TS-300
|
A content repository has an out-of-date index and a change that is not committed, in a file that the edge does not anchor. A second repository has an out-of-date index too. One variable of the environment names it: GIT_DIR, GIT_WORK_TREE or GIT_INDEX_FILE. The test runs node show for REQ-B. Then it runs edge affirm for the edge from REQ-B to REQ-A. Every file under the .git directory of each repository is the same after both commands. So is every file of each working tree. |
Test Specification: edge show writes nothing under the git directory of the case or of the decoy. SEG-TS-301
|
A case is a git repository with an out-of-date index, and a commit holds the review event of an edge. A second repository holds a copy of the case, with an out-of-date index too. GIT_DIR or GIT_WORK_TREE names it. Running edge show exits with status 0. Every file under the .git directory of the case is the same after the command. So is every file under the .git directory of the second repository, and every file of both working trees. |
tests/specification/test_repository_reads_parts.py
Test Specification: A read of more paths than one call takes gives the answer that one call gives. SEG-TS-308
|
A repository holds nine requirements, each in a file of its own. The change of two files is not committed, and a third file was never committed. One call of git takes at most two paths. A stand-in git logs the calls. Running case sync exits with status 0. Git status is called more than once. The six requirements with clean, committed files carry the revision of the repository. The three others carry none. One line names the repository and the count 3. A control makes the same store with no limit, and gives the same records and the same line. |
Test Specification: A read in parts names every path in exactly one call, and no call names too many. SEG-TS-309
|
A repository holds nine requirements, each in a file of its own. One call of git takes at most two paths. A stand-in git logs each call. Running case sync exits with status 0. The calls of git status are more than one, and so are the calls of git ls-tree. In each call, the paths number at most two. Taken together, the calls of each subcommand name each of the nine paths once and name no other path. |
Test Specification: node show reads the paths of a node in parts and reports the dirty path one call reports. SEG-TS-310
|
A node, TS-1, hashes two files in one repository. The change of the second file in the order of the names is not committed. One call of git takes at most one path. Running node show for TS-1 exits with status 0. The checkout lists the second file as its one dirty path, and names the revision of the repository. A control, with no limit, gives the same checkout. |
Test Specification: A read of so many paths that the system refuses one call gives the answer of one call. SEG-TS-311
|
A repository holds a committed file for each of several hundred requirements. Each file lies in directories deep in the tree, and each path is about 3.5 KB long, with no one name longer than 250 bytes. The paths together are larger than the limit of the operating system for the arguments of one program, so that the number of bytes and not the number of paths decides where a read is cut in parts. Running case sync exits with status 0. Each node record carries the revision of the repository. No line reports a missing extraction revision. |
Test Specification: A call of git that fails makes the repository one that cannot be read. SEG-TS-312
|
A repository holds six requirements. In one run, a stand-in git fails the first call of git status. In a second run, it fails the first call of git ls-tree. In both runs, case sync exits with status 0. No node record carries a revision, and one line names the repository and the count 6. The same run without a failure gives all six records the revision. |
Test Specification: case sync gives no revision for any node of a repository when a later part fails. SEG-TS-313
|
A repository holds six requirements, all clean and committed. One call of git takes at most two paths. A stand-in git fails the second call of git status in one run, and the second call of git ls-tree in the other. Running case sync exits with status 0. No node record carries a revision, not even the records of the paths in the parts that were read. One line names the repository and the count 6. |
Test Specification: node show reports a repository that cannot be read when a later part fails. SEG-TS-314
|
A node, TS-1, hashes two files in one repository. One call of git takes at most one path. A stand-in git fails the second call of git status. Running node show for TS-1 exits with status 0. The checkout names no revision, and it gives an error. |
tests/specification/test_repository_reads_stand_in.py
Test Specification: case sync runs every call of git without the seven variables that name a repository. SEG-TS-302
|
A configuration maps a content repository. A second repository exists. All seven variables GIT_DIR, GIT_WORK_TREE, GIT_INDEX_FILE, GIT_OBJECT_DIRECTORY, GIT_ALTERNATE_OBJECT_DIRECTORIES, GIT_COMMON_DIR and GIT_NAMESPACE are set, and each names the second repository. A stand-in git logs the environment of each call. Running case sync exits with status 0. The log holds calls for the revision, the status and the tree. In no call is one of the seven variables present. |
Test Specification: edge affirm runs every call of git without the seven variables that name a repository. SEG-TS-303
|
A configuration maps a content repository. A second repository exists. All seven variables are set, and each names the second repository. A stand-in git logs the environment of each call. Running edge affirm for the edge from REQ-B to REQ-A, with no revision given, exits with status 0. The log holds calls for the revision, the status and the tree. In no call is one of the seven variables present. |
Test Specification: node show runs every call of git without the seven variables that name a repository. SEG-TS-304
|
A case holds three requirements. A second repository exists. All seven variables are set, and each names the second repository. A stand-in git logs the environment of each call. Running node show for REQ-B exits with status 0. The log holds calls for the revision, the status and the tree. In no call is one of the seven variables present. |
Test Specification: edge show runs the before-content read of git without the seven variables. SEG-TS-305
|
An edge from REQ-B to REQ-A is affirmed, and then the text of both requirements changes and is committed. A second repository exists. All seven variables are set, and each names the second repository. A stand-in git logs the environment of each call. Running edge show with the options for verbose JSON exits with status 0. The log holds a call of the subcommand show. In no call is one of the seven variables present. |
Test Specification: edge show runs every read of the history of the case without the seven variables. SEG-TS-306
|
A case is a git repository, and one commit adds the review event of an edge. A second repository exists. All seven variables are set, and each names the second repository. A stand-in git logs the environment of each call. Running edge show exits with status 0, and the provenance of the edge is found. The log holds calls of the subcommands rev-parse, log and show. In no call is one of the seven variables present. |
Test Specification: A repository read keeps GIT_CEILING_DIRECTORIES and the GIT_CONFIG_COUNT settings. SEG-TS-307
|
GIT_CEILING_DIRECTORIES names a directory, and GIT_CONFIG_COUNT with its key and value variables sets a git option. A stand-in git logs the environment of each call. Running case sync exits with status 0. The log holds calls. In each call, GIT_CEILING_DIRECTORIES and GIT_CONFIG_COUNT are still present. |
Test Specification: proof check reads the revision of the implementation repository without the seven variables. SEG-TS-315
|
A configuration maps the implementation repository, which is clean. A second repository exists. All seven variables are set, and each names the second repository. A stand-in git logs the environment of each call. Running proof check for the scope SREQ-1, with no revision given, does not refuse the run. The log holds calls of the subcommands rev-parse and status. In no call is one of the seven variables present. |
tests/specification/test_requirements_reader.py
Reading the frozen requirement export with the configured types {top_requirement, requirement} supplies Requirement records for exactly the 29 need identifiers the export holds; reading it with {requirement} alone supplies exactly the 22 identifiers of needs of that type, and no identifier of a top_requirement need appears among them. |
Reading the frozen requirement export with both requirement types configured supplies records whose local identifiers equal, byte for byte, the ids of the export’s needs, among them SD-REQ-002 and SD-TOP-001; no identifier is normalised, prefixed or re-cased. |
Test Specification: A Requirement's content hash covers its authored fields and no others. SEG-TS-013
|
The contentHash digest supplied for SD-REQ-002 equals the SHA-256 of the UTF-8 canonical JSON (sorted keys, no insignificant whitespace) of an object holding exactly its title, its content and its sorted refines, computed in the test. In a copy of the export where only its status is changed, the digest is the same; in a copy where one character of its content is changed, the digest differs. |
Test Specification: The order of a need's refines links does not change its content hash. SEG-TS-014
|
In two copies of the export where SD-REQ-002 declares the same two parents, SD-TOP-006 and SD-TOP-001, in opposite orders, the digest supplied for SD-REQ-002 is the same in both, and equals the digest computed in the test from the sorted parents. |
Reading the frozen export supplies exactly the 22 (child, parent) pairs its needs declare in refines, each edge of kind Refines in the pending state, running from the child to the parent. In a copy where a need’s refines_back lists a need that does not declare the link, the edge set is unchanged. |
Constructing the reader over a copy of the export that adds a created stamp to its version entry, and separately over one that adds it at the top level, raises the reader’s error before any record is supplied; constructing it over the export as frozen, whose every timestamp field is null, does not. |
Reading the frozen export with the repository name “toolbox” and the source directory “doc” supplies, for every Requirement, a contentHash anchor whose repository is “toolbox” (a name, not a path), whose path is the need’s docname and doctype under “doc” (doc/detailed.rst for SD-REQ-002, doc/top-level.rst for SD-TOP-001) and whose locator is need: followed by the need’s identifier. |
Test Specification: The producer's repository name is loaded from the configuration file. SEG-TS-018
|
Loading a configuration file whose producer block names the repository “sample-repo” yields a producer whose repository is “sample-repo”. |
Test Specification: The requirement export's location is loaded, resolved against the file. SEG-TS-019
|
Loading a configuration file in a subdirectory whose producer requirements block names the export “needs/needs.json” yields a requirement export path equal to that subdirectory joined with the relative path, independent of the working directory. |
Loading a configuration file whose producer requirements block lists the types sreq and sys, the first listed twice, yields the frozenset {“sreq”, “sys”}. |
Test Specification: The requirement source directory is loaded, resolved against the file. SEG-TS-021
|
Loading a configuration file in a subdirectory whose producer requirements block names the source directory “doc” yields a source directory path equal to that subdirectory joined with “doc”. |
tests/specification/test_run_bundle_cli.py
Test Specification: A run bundle that the extractor refuses gives exit status 2 and no verdict. SEG-TS-078
|
Graph status, proof check and proof generate each name the clean bundle with a revision given, and each gives a verdict: graph status prints its edges, proof check prints its coverage report, and proof generate prints a refusal of the gate or a snapshot. Five spoiled copies replace the bundle in turn: a dirty implementation checkout, no run name, no run artifact, no recorded revision, and a path that is a file and no directory. For each copy and each verb the exit status is 2. The output holds a refusal and no edge rows, no coverage report, no snapshot and no written document. |
Test Specification: Case sync, case check, graph check, edge show and edge affirm take no run bundle. SEG-TS-079
|
The three verbs that judge evidence list |
Test Specification: Graph status and proof check include the test evidence of exactly the bundles named. SEG-TS-080
|
With no bundle named, graph status counts no outcome and proof check lists no skipped and no stale outcome. Naming the clean bundle, proof check lists three skipped outcomes of that bundle’s run and no stale outcome. Naming it and a second bundle, recorded at another revision under another run name, proof check lists the same three skipped outcomes and 24 outcomes of the second run as stale, and graph status counts the outcomes of both runs. A third bundle that lies beside the others and is not named supplies no outcome to any report. |
Test Specification: Graph status reports outcomes at the current revision and at another, and dangling edges. SEG-TS-081
|
Graph status names the clean bundle and a second bundle recorded at another revision. Graph status runs with the revision of the first. Its machine-readable report holds an evidence section. The section counts 76 outcomes at the current revision, 76 at another revision, and no edge that touches an absent node. The rows of the report hold no edge of kind Confirms, Witnesses or Excuses. |
Test Specification: A Confirms, Witnesses or Excuses edge that touches an absent node gives exit status 1. SEG-TS-082
|
The current stream is a store that holds two outcomes, one recorded at the revision of the implementation repository and one at another, and one Confirms edge to a test specification that the store does not hold. Graph status runs with the revision of the repository. It exits with status 1, its negative verdict. The same store without that edge gives exit status 0. |
Test Specification: The evidence section counts each evidence edge that touches an absent node. SEG-TS-083
|
The current stream is the store of the previous test: two outcomes, one at the revision of the repository and one at another, and one Confirms edge to an absent test specification. Graph status runs with the revision of the repository. The evidence section counts one outcome at the current revision, one at another revision and one dangling edge. |
Test Specification: Graph status gives a state for every strong edge and for no evidence edge. SEG-TS-084
|
The current stream is a store with two outcomes, each with a Confirms edge and a Witnesses edge, and one Verifies and one Implements edge. Graph status runs with the revision of the repository. Its rows are the two strong edges, both pending. No row has the kind Confirms or Witnesses. |
Test Specification: When the only edges that are not active are pending, graph status exits with status 0. SEG-TS-085
|
The current stream is a store with two outcomes, one at the revision of the implementation repository and one at another, and a clean repository that the configuration names. Its two strong edges are pending and nothing is affirmed. Graph status runs and exits with status 0. |
Test Specification: Graph status refuses a discovered revision when the repository holds an untracked file. SEG-TS-086
|
The current stream holds an outcome. The implementation repository holds one untracked file. Graph status runs with no revision given. It exits with status 2 and its report names the untracked path. With a revision given, graph status exits with status 0. |
Test Specification: Proof check and proof generate refuse a discovered revision when the repository is dirty. SEG-TS-087
|
The implementation repository holds one untracked file. Proof check and proof generate run with no revision given. Each exits with status 2 and its report names the untracked path. Run with a revision given, neither exits with status 2. |
Test Specification: With an outcome in the stream and no obtainable revision, the verbs exit with status 2. SEG-TS-088
|
The current stream holds an outcome. No revision is given and no implementation repository is configured. Graph status, proof check and proof generate each exit with status 2. |
Test Specification: Graph status asks for no revision when the current stream holds no outcome. SEG-TS-089
|
The current stream holds a requirement, a specification, an implementation and two strong edges, and no outcome. No revision is given and no configuration is read. Graph status exits with status 0. |
Test Specification: A verb that reads a case whose record fails its schema exits with status 2. SEG-TS-090
|
One edge record in the case holds a link state that the case’s schema copy does not allow. Graph status, edge show, graph check on the case itself, and proof check each exit with status 2 and print the refusal with text. The machine-readable form of graph status holds an error entry. |
Test Specification: Graph check counts the pending strong edges and counts evidence edges by kind only. SEG-TS-091
|
The legacy case holds 32 edges: four strong edges are pending, six are active, and 22 evidence edges are pending. Graph check on the case reports a pending count of four, and counts of 10 Confirms and 12 Witnesses edges by kind. A store with two outcomes, each with a Confirms and a Witnesses edge, and two strong edges, none affirmed, gives a pending count of two when it is the current stream. The report holds the node counts, the edge counts and the pending count, and no count of dangling endpoints. |
Graph status and proof check name the clean bundle twice, once as a path and once as a path that goes through another directory and back. Each gives the result of naming it once: graph status counts 76 outcomes at the current revision, and proof check lists three skipped outcomes. Two copies of the bundle named together are refused, because they supply the same outcome identities twice. |
Test Specification: A run bundle and a current stream given in one invocation give exit status 2. SEG-TS-114
|
The current stream is a would-be store. Graph status, proof check and proof generate each run with the stream alone and are not refused. Each run with the stream and a named bundle exits with status 2, and the output holds a refusal and no verdict. |
Test Specification: A run bundle named with no test-case export in the configuration gives exit status 2. SEG-TS-116
|
A configuration that gives a test-case export lets graph status, proof check and proof generate judge the clean bundle (none exits with status 2). A configuration that gives none makes each of them exit with status 2 when the bundle is named, with a refusal and no verdict. |
tests/specification/test_run_bundle_digest.py
Test Specification: A run bundle's digest is the SHA-256 of its list of paths and file digests. SEG-TS-067
|
The clean bundle fixture holds 11 files. Its digest by the recipe of the
architecture page is the value named in the fixture’s README. The recipe
is run in plain Python, and in the shell with find, sort and sha256sum
where the shell has them. Both give that value. The tool gives that value
too, written as |
Test Specification: A changed byte, a renamed file or an added file changes the digest of a bundle. SEG-TS-068
|
Four copies of the clean bundle each differ from it in one way: one byte of the run artifact is changed, one file is renamed, one file is added, and one empty file is added. Each copy has a digest that differs from the clean bundle’s digest and from every other copy’s. Three more copies differ in no byte and no name: the files are created in the reverse order, the bundle lies in another directory under another name, and every file has another modification time. Each has the clean bundle’s digest. |
tests/specification/test_run_bundle_extractor.py
The bundle lies in a directory that also holds a revision record, a name record and a run artifact of the same names, with other content: another revision, another run name and an artifact whose every result failed. The configuration names the bundle. All 76 outcomes carry the revision and the run name of the bundle, and none carries a result of the other artifact. |
The clean bundle is accepted. With the dirty file of the implementation
checkout holding one line of |
The clean bundle is accepted. With the name record deleted, empty, or holding only a line feed, the extractor refuses the run and names the run name. |
The clean bundle is accepted. With the run artifact deleted, the extractor refuses the run, although the bundle still holds a test plan, two XML reports, the revisions and the name. With the run artifact replaced by text that is not JSON, the extractor refuses the run. |
The clean bundle with the frozen exports is accepted. A copy of the
test-specification export with a |
Test Specification: Each outcome's revision is the revision the bundle records for the implementation checkout. SEG-TS-075
|
The clean bundle records a different revision for each of its two checkouts. With the first as the implementation checkout, all 76 outcomes carry the first revision. With the second, all carry the second revision. A record of the implementation checkout that holds a short word is taken exactly as recorded. |
Test Specification: A bundle that records no revision for the implementation checkout is refused. SEG-TS-076
|
The clean bundle is accepted. With the revision record of the implementation checkout deleted, empty, or holding only a line feed, the extractor refuses the run and names the revision. It refuses the run too when the configuration names an implementation checkout of which the bundle holds no record. A missing record of another checkout does not refuse the run. |
Test Specification: A configuration that names a run is refused, whatever the entry holds. SEG-TS-115
|
A configuration with no run loads. A configuration whose producer holds
|
Test Specification: A path named as a run bundle that is not a directory with a readable artifact is refused. SEG-TS-117
|
The clean bundle is accepted. A path that does not exist, a path that is a plain file, and an empty directory each make the extractor refuse the run. Graph status exits with status 2 when it names the plain file. |
Test Specification: An outcome's anchor names its run bundle by the digest, wherever the bundle lies. SEG-TS-118
|
Each of the 76 outcomes of the clean bundle has an anchor whose repository
member is the bundle’s digest written as |
tests/specification/test_run_bundle_proof.py
Test Specification: A package's manifest holds the digest of every run bundle that supplied an in-scope outcome. SEG-TS-092
|
Three bundles are configured. The first is recorded at the revision given, and supplies outcomes in the scope. The second is recorded at another revision: its outcomes in the scope are set aside by the gate, and the package still records it. The third is recorded at the revision given, and holds results of one test function that lies outside the scope: it is not recorded. The evidence manifest of the generated package holds the digest of the first and of the second, and not the digest of the third. With only the first bundle configured, the manifest holds only that digest. |
Test Specification: A package's design root and design proof are those of the golden, with one run or two. SEG-TS-093
|
The golden design root was made before bundles existed. The package generated over the clean bundle has a design consistency proof that is byte for byte the golden’s. The package generated over the clean bundle and a second bundle at another revision has a design consistency proof that is byte for byte the golden’s for two runs. In both the design root is the root written in the golden. The scope of both packages holds test outcomes, and the root is the same with 24 or 48 of them in the scope. |
Test Specification: The gate leaves the outcomes of a run at another revision out of every coverage finding. SEG-TS-094
|
The gate’s report over the clean bundle equals the golden report. The report over the clean bundle and a second bundle at another revision equals the first report in every part except the list of stale outcomes and the diagnostics that name them: the blocked flag, the coverage gaps, the unready edges, the skipped, excused, unwaived and discarded outcomes and the empty-design flag are the same. The gate does not block. |
Test Specification: The gate reports each outcome of a run at another revision as an informational finding. SEG-TS-095
|
The gate’s report over the clean bundle and a second bundle at another revision equals the golden report for two runs. It lists 24 outcomes of the second run as stale. Each has one finding of severity information, and no outcome of the first run is listed as stale. |
Test Specification: Every requirement's satisfaction over bundle evidence equals the golden verdict. SEG-TS-096
|
The producer the configuration describes supplies the outcomes of the bundles. The graph built from the case and that producer gives the satisfaction evaluator the same verdicts as the golden for each of the 29 requirements, 18 of them satisfied, with the same outcomes set aside as incomplete. The verdicts are the same with a second run at another revision. |
Test Specification: The documents of a package equal the golden's, and the manifest gains one field. SEG-TS-097
|
For one run and for two runs, the coverage report and the execution coverage record are byte for byte the golden’s, and the package has the golden’s snapshot identifier. The evidence manifest has every field of the golden’s manifest with the same value, and exactly one more field. That field holds the digest of each bundle used: one for one run, two for two runs. |
tests/specification/test_taxonomy.py
Querying the taxonomy provider’s node-kind and edge-kind sets returns exactly the built-in vocabulary: the node kinds are Requirement, Implementation, TestSpecification, TestOutcome, and Waiver; the edge kinds are Refines, Verifies, Implements, Confirms, Witnesses, Excuses, and Calls. Neither set holds anything beyond this list, and neither omits an entry from it. |
Querying the taxonomy provider for the edge kinds that propagate suspicion returns exactly three: Refines, Verifies, and Implements. No other declared edge kind is included, and none of these three is missing. |
For each of the five built-in node kinds, querying the taxonomy
provider’s content-hash names returns exactly the names that kind
carries: |