20 lines
1012 B
TeX
20 lines
1012 B
TeX
%% SCRAP: archive/operations/refinement/annotations
|
|
%% SOURCE: docs/working/archive/operations/refinement/annotations.adoc
|
|
%% STATUS: OBSOLETE
|
|
%% FITS: none
|
|
%% EDITORIAL: lifted — prose rewritten to press voice; adoc syntax translated
|
|
|
|
\section*{C\,$\leftrightarrow$\,Isabelle Annotation Guide (Obsolete)}
|
|
|
|
This guide defined a \textsc{refinement} header standard for annotating
|
|
C source files with cross-references to their Isabelle/HOL counterparts.
|
|
The standard specified invariant documentation blocks, proof status markers
|
|
(\texttt{PROVEN}, \texttt{PENDING}, \texttt{UNVERIFIED}), and a tagging
|
|
convention linking each C function to the corresponding Isabelle theory.
|
|
|
|
The methodology was not adopted. Formal verification of StarForth proceeded
|
|
instead through standalone \texttt{.thy} files in \texttt{proof/}, organized
|
|
by feedback loop and word category, without inline C annotations. The 19
|
|
(subsequently 24, with ACL proofs) theory files provide the formal record.
|
|
This annotation guide is obsolete.
|