Files
TerminalBasic/openspec/changes/archive/2026-09-06-laufzeit-eingabe-und-systemstatus/verification.md

111 lines
7.6 KiB
Markdown
Raw Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
# Implementierungs- und Verifikationsnachweis
Change: `laufzeit-eingabe-und-systemstatus`, Stand 06.09.2026.
Grundlage: Arbeitsbaum auf `815825dde76eb8f4b48cb27d83f21732afe707c2`;
Proposal, Design, vier Delta-Specs und alle sechs Tasks abgeglichen.
## Ergebnis
| Dimension | Ergebnis |
|---|---|
| Vollständigkeit | 6/6 Tasks, 6/6 Requirements, 21/21 Szenarien abgeglichen |
| Korrektheit | Alle zugeordneten Regressionen und Workspace-Tests bestanden |
| Kohärenz | D1D4 umgesetzt; keine zusätzlichen Dependencies |
| Offene Befunde | 0 CRITICAL, 0 WARNING, 0 SUGGESTION im Change |
F14F17 und F19 sind umgesetzt. Die vier Hauptspecs wurden am 06.09.2026
synchronisiert und alle 15 Hauptspecs streng validiert. Der Change ist unter
`openspec/changes/archive/2026-09-06-laufzeit-eingabe-und-systemstatus` archiviert.
## Umsetzung und Design
- **D1:** `Datei` verwendet einen `BufReader<File>` für den gemeinsamen Cursor.
`feld_lesen`, `zeile_lesen`, `zeichen_lesen`, EOF und SEEK erhalten den
Lesefortschritt. INPUT # liest einzelne Felder statt vollständiger Zeilen;
fehlende Felder erzeugen Fehler 62. Dekodierte Strings werden in der VM
nicht erneut von Anführungszeichen oder Rand-Leerraum befreit.
- **D2:** INPUT$ zählt UTF-8-Codepoints. Beschädigte oder abgeschnittene
UTF-8-Sequenzen führen zu Fehler 57; EOF vor einem geforderten Zeichen
zu Fehler 62. Ein bereits angenommener Tastaturrest wird vor weiteren
Tasten geliefert und nicht nochmals als Trap-/Forms-Ereignis eingereiht.
Direkter Builtin-Dispatch und resumierbare VM-Eingabe verwenden dieselbe
Aufteilung. Alle fünf CV-Funktionen prüfen exakte Breite und Bytezeichen.
GET/PUT und UTF-32-Recorddarstellung bleiben eigenständige Binärpfade.
- **D3:** `fehler_am_pfad` unterscheidet fehlenden Dateieintrag (53) von
fehlendem Elternverzeichnis (76) bei OPEN, KILL, NAME und MKDIR.
Vorhandene Berechtigungs-/Existenzfehler bleiben erhalten; ein Pfadbestandteil,
der kein Verzeichnis ist, wird ebenfalls als Pfadfehler eingeordnet.
- **D4:** TIMEZONEKNOWN ist als parameterlose INTEGER-Funktion durch Semantik,
HIR, Codegenerator, stabile neue Builtin-ID 156 und Dispatch geführt.
`RtState::zeitpunkt` löst Zeit und Status gemeinsam auf. Die Systemquelle
bleibt nach Ausfällen aktiv, sodass spätere Erholung sichtbar wird.
Tests können die Zonenquelle ersetzen, ohne die Rechnerzone zu verändern.
Programmversatz, monotone Ereigniszeit und Betriebssystemuhr werden durch
die Statusabfrage nicht verändert. CLI-Startwarnung und Inventar sind angepasst.
## Szenarien und ausführbare Nachweise
Testnamen ohne Präfix stehen in `crates/tb-vm/tests/vm.rs`. `runtime` meint
`crates/tb-runtime/src/builtins.rs`, `frontend` die Semantik bzw. Inventartests.
Die Korpusprogramme liegen in `tests/compat`; der Harness führt jedes zweimal
gegen seine festgeschriebene Sollausgabe aus.
| Requirement / Szenario | Nachweis |
|---|---|
| Sequenzielle Datenübertragung: WRITE # und INPUT # sind gegenläufig | `input_datei_bewahrt_felder_und_unterscheidet_leer_von_fehlend`; `eingabefortschritt.bas` |
| Lesen über das Dateiende | Derselbe Test: leere Datei, fehlendes zweites Feld und EOF; `input_datei_alle_lesearten_teilen_utf8_cursor_und_seek` |
| Felder über zwei Aufrufe | `input_datei_bewahrt_felder_und_unterscheidet_leer_von_fehlend`: WRITE a/b, anschließende getrennte Reads |
| Zu wenige Felder | Derselbe Test: mit/ohne finales Zeilenende Fehler 62; explizit leere Felder bleiben lesbar |
| Record-Konvertierungen: MK und CV sind gegenläufig | `alle_mk_cv_paare_verlangen_exakte_bytezeichenbreite`: alle fünf Paare |
| Falsche Argumentlänge | Derselbe Test: jeweils Zielbreite minus ein Zeichen → Fehler 5 |
| Zu langes CVI-Argument | Derselbe Test: jeweils Zielbreite plus ein Zeichen → Fehler 5; zusätzlich Nicht-Bytezeichen |
| Dateisystem: Rückwärts-Schrägstrich auf Unix | `datei_und_elternpfadfehler_sind_am_sprachzugang_unterscheidbar`: OPEN über Backslash, anschließendes NAME/Lesen/Löschen |
| Verzeichnis durchlaufen | Derselbe Test: DIR$ mit Muster und Folgeaufruf; vorhandener Dateikorpus |
| Fehlender Pfad | Derselbe Test: MKDIR, NAME-Ziel, CHDIR, RMDIR, DIR$ → 76 |
| OPEN mit fehlendem Elternpfad | Derselbe Test: INPUT mit fehlender Datei → 53, fehlendem Elternpfad → 76; zusätzlich OUTPUT/APPEND/BINARY/RANDOM |
| Zonenermittlung: Zone nicht ermittelbar | runtime `zonenquelle_ausfall_und_erholung_gelten_fuer_alle_zeitfunktionen`; `timezonefallback.bas` |
| Rückfallebene ist erkennbar | `timezoneknown_hat_integer_signatur_und_zeigt_aktuellen_status`; `timezoneknown.bas` und `timezonefallback.bas` |
| Rückfall nach Programmstart | Derselbe VM-Test über STOP/Fortsetzung und runtime-Zonenquelle mit Ausfall und Erholung; bekannte UTC liefert -1 |
| Signaturen: Element ohne Laufzeitverhalten wird namentlich abgewiesen | Vorhandener frontend-Test `dokumentierte_elemente_werden_namentlich_abgewiesen`; Inventar hat derzeit 0 offene Elemente |
| Argumentprüfung ohne Laufzeitverhalten | frontend `builtins_typen`: MKL$() hat benannte Argumentanzahl-Diagnose |
| Signatur der Zonenzustandsabfrage | frontend `builtins_typen`: 0 Argumente, INTEGER; TIMEZONEKNOWN(1) benannt abgewiesen; runtime-Test prüft tatsächliches `Value::Int` |
| Tastatur: INKEY$ bei leerem Puffer | `inkey_ohne_taste_ist_leer` |
| Sondertaste als zwei Zeichen | `inkey_liefert_zeichen_und_sondertaste` |
| Sondertastenfolge in zwei Reads | `input_s_teilt_sondertasten_und_bewahrt_rest_fuer_inkey`; `eingabefortschritt.bas`; direkter runtime-Dispatch |
| Unicode aus Datei | `input_datei_alle_lesearten_teilen_utf8_cursor_und_seek`: ä/Emoji, INPUT und BINARY |
Zusätzliche Randfälle: CR/LF/CRLF, Leerzeilen, eingebettete Kommas,
verdoppelte Anführungszeichen und Zeilenumbrüche, Null-Länge, negative Länge,
ungültiges UTF-8, falscher Dateimodus, SEEK nach EOF und gemischte Lesearten.
`unicode_puffergrenzen_und_binaere_records_bleiben_getrennt` prüft UTF-8 an
8-KiB-Puffergrenzen sowie GET/PUT zwischen INPUT$-Aufrufen.
`sondertastenrest_wird_nicht_erneut_getrappt` prüft F1 unter KEY STOP/ON.
Die bestehenden Programmversatz- und Ereignistests bestehen weiterhin.
## Abnahme
- `cargo test --workspace --quiet`: **463 bestanden, 0 fehlgeschlagen,
1 ignoriert**. Der ignorierte Golden-Generator wurde nicht ausgeführt.
- `cargo clippy --workspace --all-targets --all-features -- -D warnings`: bestanden.
- `cargo fmt --all -- --check`: bestanden.
- `git diff --check`: bestanden vor dem Staging. Die abschließende
Prüfung des gestagten Changes mit `git diff --cached --check -- .
':(exclude)tests/compat/*.out'` besteht ebenfalls. Die neuen `.out`-Dateien
enthalten absichtlich signifikante PRINT-Leerzeichen am Zeilenende.
- `openspec validate laufzeit-eingabe-und-systemstatus --strict`: bestanden.
- Bestehende `tests/compat/*.out` unverändert; drei neue Programme mit
vorab festgelegten Sollausgaben ergänzt. Die Inventar-Abdeckungszahl
berücksichtigt die neue Erweiterung: 795 implementiert, 0 offen,
50 Non-Features, insgesamt 845 Einträge.
Die anfänglichen Testfehler (doppelte Quote-Auswertung, fehlende Korpus-
Rückfalldirektive, Test-Namensauflösung, Inventar-Gesamtzahl) sind behoben;
der abschließende Workspace-Lauf ist grün. Keine Tests oder vorhandenen
Sollausgaben wurden zum Übergehen dieser Fehler abgeschwächt.
Geprüft wurde headless auf macOS. Es erfolgte kein neuer interaktiver
Fremdprogrammvergleich und keine Windows-/Linux-Ausführung. Die ergänzenden
Korpusfälle belegen den erklärten TerminalBasic-Vertrag, keine historische
Bytekompatibilität. Der verbleibende Change
`spezifikationsabgleich-und-regressionsnachweise` bleibt eigenständig.